| java.lang.Object de.uka.ilkd.key.logic.RenameTable
RenameTable | public class RenameTable (Code) | | |
Constructor Summary | |
public | RenameTable(RenameTable parent, MapFromQuantifiableVariableToInteger localTable, int newMax) |
RenameTable | public RenameTable(RenameTable parent, MapFromQuantifiableVariableToInteger localTable, int newMax)(Code) | | |
contains | public boolean contains(QuantifiableVariable n)(Code) | | returns true iff the given variable is mapped to an abstract name.
The test is performed in the local as well as in the parent
renaming table.
Parameters: n - the QuantifiableVariable object the existence of an abstract name is checked. true if n has been already assigned to anabstract name |
containsLocally | public boolean containsLocally(QuantifiableVariable n)(Code) | | does nearly the same as
RenameTable.contains(QuantifiableVariable) but performs
the test only on the local table
Parameters: n - the QuantifiableVariable object the existence of an abstract name is checked. true if n has been already locallyassigned to an abstract name |
extend | public RenameTable extend()(Code) | | creates a nested renaimg table with this
as parent
|
sameAbstractName | public boolean sameAbstractName(QuantifiableVariable n1, QuantifiableVariable n2)(Code) | | tests if both QuantifiableVariables are assigned to the same abstract
name (locally or by the parent)
Parameters: n1 - one of the QuantifiableVariables to be tested iff they havebeen assigned the same abstract name Parameters: n2 - one of the QuantifiableVariables to be tested true iff n1 and n2 are mappedto the same abstract name |
|
|