de.uka.ilkd.key.logic

Class InnerVariableNamer

java.lang.Object

de.uka.ilkd.key.logic.VariableNamer

de.uka.ilkd.key.logic.InnerVariableNamer

All Implemented Interfaces:

InstantiationProposer

public class InnerVariableNamer
extends VariableNamer

Implements "inner renaming", i.e. renaming - if a new variable entering the globals causes a name clash - this "inner" variable, and leaving the clashing "outer" one untouched.

Nested Class Summary

Nested classes/interfaces inherited from class de.uka.ilkd.key.logic.VariableNamer

VariableNamer.BasenameAndIndex, VariableNamer.IndProgramElementName

Field Summary

Fields inherited from class de.uka.ilkd.key.logic.VariableNamer

map, renamingHistory, services

Constructor Summary

Constructors

Constructor and Description
InnerVariableNamer(Services services)

Method Summary

Modifier and Type	Method and Description
private int	getMaxCounterInGlobalsAndProgram(java.lang.String basename, java.lang.Iterable<ProgramElementName> globals, ProgramElement program, PosInProgram posOfDeclaration) returns the maximum counter for the passed basename in the passed globals and the passed program
ProgramVariable	rename(ProgramVariable var, Goal goal, PosInOccurrence posOfFind) intended to be called when symbolically executing a variable declaration; resolves any naming conflicts between the new variable and other global variables by renaming the new variable and / or other variables

Methods inherited from class de.uka.ilkd.key.logic.VariableNamer

createName, getBasename, getBasenameAndIndex, getMaxCounterInGlobals, getMaxCounterInProgram, getNameProposalForSchemaVariable, getProgramFromPIO, getProposal, getRenamingMap, getSuggestiveNameProposalForProgramVariable, getSuggestiveNameProposalForSchemaVariable, getTemporaryNameProposal, isUniqueInGlobals, isUniqueInProgram, isUniqueNameForSchemaVariable, parseName, parseName, parseName, parseName, setSuggestiveEnabled, wrapGlobals, wrapGlobals

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

InnerVariableNamer

public InnerVariableNamer(Services services)

Method Detail

getMaxCounterInGlobalsAndProgram

private int getMaxCounterInGlobalsAndProgram(java.lang.String basename,
                                             java.lang.Iterable<ProgramElementName> globals,
                                             ProgramElement program,
                                             PosInProgram posOfDeclaration)

returns the maximum counter for the passed basename in the passed globals and the passed program

rename

public ProgramVariable rename(ProgramVariable var,
                              Goal goal,
                              PosInOccurrence posOfFind)

Description copied from class: VariableNamer

intended to be called when symbolically executing a variable declaration; resolves any naming conflicts between the new variable and other global variables by renaming the new variable and / or other variables

Specified by:

rename in class VariableNamer

Parameters:

var - the new program variable

goal - the goal

posOfFind - the PosInOccurrence of the currently executed program

Returns:

the renamed version of the var parameter