public final class LocationVariable extends ProgramVariable implements UpdateableOperator
Constructor and Description |
---|
LocationVariable(ProgramElementName name,
KeYJavaType t) |
LocationVariable(ProgramElementName name,
KeYJavaType t,
boolean isFinal) |
LocationVariable(ProgramElementName name,
KeYJavaType t,
boolean isGhost,
boolean isFinal) |
LocationVariable(ProgramElementName name,
KeYJavaType t,
KeYJavaType containingType,
boolean isStatic,
boolean isModel) |
LocationVariable(ProgramElementName name,
KeYJavaType t,
KeYJavaType containingType,
boolean isStatic,
boolean isModel,
boolean isGhost,
boolean isFinal) |
LocationVariable(ProgramElementName name,
Sort s) |
Modifier and Type | Method and Description |
---|---|
int |
arity()
the arity of this operator
|
boolean |
bindVarsAt(int n)
Tells whether the operator binds variables at the n-th subterm.
|
boolean |
isRigid()
Tells whether the operator is rigid.
|
Name |
name()
returns the name of this element
|
UpdateableOperator |
rename(Name name)
Returns an equivalent variable with the new name.
|
java.lang.String |
toString() |
void |
validTopLevelException(Term term)
Checks whether the top level structure of the given @link Term
is syntactically valid, given the assumption that the top level
operator of the term is the same as this Operator.
|
void |
visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
protected ImmutableArray<java.lang.Boolean> |
whereToBind() |
convertToProgram, equalsModRenaming, getComments, getContainerType, getEndPosition, getFirstElement, getFirstElementIncludingBlocks, getKeYJavaType, getKeYJavaType, getKeYJavaType, getLastElement, getPositionInfo, getProgramElementName, getReferencePrefix, getRelativePosition, getStartPosition, isFinal, isGhost, isImplicit, isMember, isModel, isStatic, match, prettyPrint, proofToString
additionalValidTopLevel, argSort, argSorts, sort, sort
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
argSort, argSorts, sort
arity, bindVarsAt, isRigid, sort, validTopLevel, validTopLevelException
public LocationVariable(ProgramElementName name, KeYJavaType t, KeYJavaType containingType, boolean isStatic, boolean isModel, boolean isGhost, boolean isFinal)
public LocationVariable(ProgramElementName name, KeYJavaType t, KeYJavaType containingType, boolean isStatic, boolean isModel)
public LocationVariable(ProgramElementName name, KeYJavaType t)
public LocationVariable(ProgramElementName name, KeYJavaType t, boolean isFinal)
public LocationVariable(ProgramElementName name, KeYJavaType t, boolean isGhost, boolean isFinal)
public LocationVariable(ProgramElementName name, Sort s)
public void visit(Visitor v)
SourceElement
visit
in interface SourceElement
visit
in class ProgramVariable
v
- the Visitorpublic UpdateableOperator rename(Name name)
ProgramVariable
rename
in class ProgramVariable
name
- the new nameprotected final ImmutableArray<java.lang.Boolean> whereToBind()
public final Name name()
Named
public final int arity()
Operator
public final boolean bindVarsAt(int n)
Operator
bindVarsAt
in interface Operator
public final boolean isRigid()
Operator
public void validTopLevelException(Term term) throws TermCreationException
Operator
validTopLevelException
in interface Operator
TermCreationException
- if a construction error was recognisepublic java.lang.String toString()
toString
in class java.lang.Object
Copyright © 2003-2019 The KeY-Project.