| java.lang.Object
 de.uka.ilkd.key.logic.VariableNamer
All known Subclasses: de.uka.ilkd.key.logic.InnerVariableNamer,
| VariableNamer | | abstract public class VariableNamer implements InstantiationProposer(Code) | | Responsible for program variable naming issues.
|
| Inner Class :protected static interface Globals | |
| Inner Class :protected static class BasenameAndIndex | |
| Method Summary | |
| protected ProgramElementName | createName(String basename, int index, NameCreationInfo creationInfo)
| | protected BasenameAndIndex | getBasenameAndIndex(ProgramElementName name)
| | protected int | getMaxCounterInGlobals(String basename, Globals globals)
| | protected int | getMaxCounterInProgram(String basename, ProgramElement program, PosInProgram posOfDeclaration)
| | protected NameCreationInfo | getMethodStack(PosInOccurrence posOfFind)
| | protected ProgramElementName | getNameProposalForSchemaVariable(String basename, SortedSchemaVariable sv, PosInOccurrence posOfFind, PosInProgram posOfDeclaration, ListOfString previousProposals)
| | protected ProgramElement | getProgramFromPIO(PosInOccurrence pio)
| | public String | getProposal(TacletApp app, SchemaVariable var, Services services, Node undoAnchor, ListOfString previousProposals)
| | public HashMap | getRenamingMap()
| | public String | getSuggestiveNameProposalForProgramVariable(SortedSchemaVariable sv, TacletApp app, Goal goal, Services services, ListOfString previousProposals)
| | public String | getSuggestiveNameProposalForSchemaVariable(Expression e)
| | public ProgramElementName | getTemporaryNameProposal(String basename)
| | protected boolean | isUniqueInGlobals(String name, Globals globals)
| | protected boolean | isUniqueInProgram(String name, ProgramElement program, PosInProgram posOfDeclaration)
| | public boolean | isUniqueNameForSchemaVariable(String name, SortedSchemaVariable sv, PosInOccurrence posOfFind, PosInProgram posOfDeclaration)
| | public static ProgramElementName | parseName(String name, NameCreationInfo creationInfo, Comment[] comments)
| | public static ProgramElementName | parseName(String name, NameCreationInfo creationInfo)
| | public static ProgramElementName | parseName(String name, Comment[] comments)
| | public static ProgramElementName | parseName(String name)
| | abstract public ProgramVariable | rename(ProgramVariable var, Goal goal, PosInOccurrence posOfFind)
| | public static void | setSuggestiveEnabled(boolean enabled)
| | protected Globals | wrapGlobals(ListOfNamed globals)
| | protected Globals | wrapGlobals(SetOfProgramVariable globals)
|
| VariableNamer | | public VariableNamer(Services services)(Code) | |
Parameters:
services - pointer to services object |
| getBasenameAndIndex | | protected BasenameAndIndex getBasenameAndIndex(ProgramElementName name)(Code) | | determines the passed ProgramElementName's basename and index (ignoring
temporary indices)
|
| getMaxCounterInGlobals | | protected int getMaxCounterInGlobals(String basename, Globals globals)(Code) | | returns the maximum counter value already associated with the passed
basename in the passed list of global variables, or -1
|
| getMaxCounterInProgram | | protected int getMaxCounterInProgram(String basename, ProgramElement program, PosInProgram posOfDeclaration)(Code) | | returns the maximum counter value already associated with the passed
basename in the passed program (ignoring temporary counters), or -1
|
| getNameProposalForSchemaVariable | | protected ProgramElementName getNameProposalForSchemaVariable(String basename, SortedSchemaVariable sv, PosInOccurrence posOfFind, PosInProgram posOfDeclaration, ListOfString previousProposals)(Code) | | proposes a unique name for the instantiation of a schema variable
(like getProposal(), but somewhat less nicely)
Parameters:
basename - desired base name, or null to use default
Parameters:
sv - the schema variable
Parameters:
posOfFind - the PosInOccurrence containing the name's target program
Parameters:
posOfDeclaration - the PosInProgram where the name will be declared(or null to just be pessimistic about the scope)
Parameters:
previousProposals - list of names which should be considered taken,or null the name proposal, or null if no proposal is available |
| getProposal | | public String getProposal(TacletApp app, SchemaVariable var, Services services, Node undoAnchor, ListOfString previousProposals)(Code) | | proposes a unique name for the instantiation of a schema variable
Parameters:
app - the taclet app
Parameters:
var - the schema variable to be instantiated
Parameters:
services - not used
Parameters:
undoAnchor - not used
Parameters:
previousProposals - list of names which should be considered taken,or null the name proposal, or null if no proposal is available |
| getSuggestiveNameProposalForSchemaVariable | | public String getSuggestiveNameProposalForSchemaVariable(Expression e)(Code) | | |
| getTemporaryNameProposal | | public ProgramElementName getTemporaryNameProposal(String basename)(Code) | | proposes a unique name; intended for use in places where the information
required by getProposal() is not available
Parameters:
basename - desired base name, or null to use default the name proposal |
| isUniqueInGlobals | | protected boolean isUniqueInGlobals(String name, Globals globals)(Code) | | tells whether a name is unique in the passed list of global variables
|
| isUniqueNameForSchemaVariable | | public boolean isUniqueNameForSchemaVariable(String name, SortedSchemaVariable sv, PosInOccurrence posOfFind, PosInProgram posOfDeclaration)(Code) | | tells whether a name for instantiating a schema variable is unique
within its scope
Parameters:
name - the name to be checked
Parameters:
sv - the schema variable
Parameters:
posOfFind - the PosInOccurrence of the name's target program
Parameters:
posOfDeclaration - the PosInProgram where the name will be declared true if the name is unique or if its uniqueness cannot bechecked, else false |
| parseName | | public static ProgramElementName parseName(String name, NameCreationInfo creationInfo, Comment[] comments)(Code) | | parses the passed string and creates a suitable program element name
(this does *not* make the name unique - if that is necessary, use either
getTemporaryNameProposal() or getProposal())
Parameters:
name - the name as a string
Parameters:
creationInfo - optional name creation info the name should carry
Parameters:
comments - any comments the name should carry the name as a ProgramElementName |
| rename | | abstract public ProgramVariable rename(ProgramVariable var, Goal goal, PosInOccurrence posOfFind)(Code) | | 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
Parameters:
var - the new program variable
Parameters:
goal - the goal
Parameters:
posOfFind - the PosInOccurrence of the currently executed program the renamed version of the var parameter |
| setSuggestiveEnabled | | public static void setSuggestiveEnabled(boolean enabled)(Code) | | |
| wrapGlobals | | protected Globals wrapGlobals(ListOfNamed globals)(Code) | | creates a Globals object for use with other internal methods
|
| wrapGlobals | | protected Globals wrapGlobals(SetOfProgramVariable globals)(Code) | | creates a Globals object for use with other internal methods
|
|
|