public abstract class ProgramVariable extends AbstractSortedOperator implements SourceElement, ProgramElement, Expression, ReferencePrefix, IProgramVariable, ParsableVariable, ReferenceSuffix, ProgramInLogic
Modifier | Constructor and Description |
---|---|
protected |
ProgramVariable(ProgramElementName name,
Sort s,
KeYJavaType t,
KeYJavaType containingType,
boolean isStatic,
boolean isModel,
boolean isGhost) |
protected |
ProgramVariable(ProgramElementName name,
Sort s,
KeYJavaType t,
KeYJavaType containingType,
boolean isStatic,
boolean isModel,
boolean isGhost,
boolean isFinal) |
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.
|
Expression |
convertToProgram(Term t,
ExtList l) |
boolean |
equalsModRenaming(SourceElement se,
NameAbstractionTable nat)
equals modulo renaming is described in the corresponding
comment in class SourceElement.
|
Comment[] |
getComments()
Get comments.
|
KeYJavaType |
getContainerType()
returns the KeYJavaType where the program variable is declared or
null if the program variable denotes not a field
|
Position |
getEndPosition()
Returns the end position of the primary token of this element.
|
SourceElement |
getFirstElement()
Finds the source element that occurs first in the source.
|
SourceElement |
getFirstElementIncludingBlocks()
Finds the source element that occurs first in the source.
|
KeYJavaType |
getKeYJavaType() |
KeYJavaType |
getKeYJavaType(Services javaServ) |
KeYJavaType |
getKeYJavaType(Services javaServ,
ExecutionContext ec)
returns the
KeYJavaType of an expression |
SourceElement |
getLastElement()
Finds the source element that occurs last in the source.
|
PositionInfo |
getPositionInfo()
complete position information
|
ProgramElementName |
getProgramElementName() |
ReferencePrefix |
getReferencePrefix()
We do not have a prefix, so fake it!
This way we implement ReferencePrefix
|
Position |
getRelativePosition()
Returns the relative position (number of blank heading lines and
columns) of the primary token of this element.
|
Position |
getStartPosition()
Returns the start position of the primary token of this element.
|
boolean |
isFinal()
returns true iff the program variable has been declared as final
|
boolean |
isGhost()
returns true if the program variable has been declared as ghost
|
boolean |
isImplicit() |
boolean |
isMember()
returns true iff the program variable is a member
|
boolean |
isModel()
returns true iff the program variable has been declared as model
|
boolean |
isRigid()
Tells whether the operator is rigid.
|
boolean |
isStatic()
returns true iff the program variable has been declared as static
|
MatchConditions |
match(SourceData source,
MatchConditions matchCond)
matches the source "text" (@link SourceData#getSource()) against the pattern represented
by this object.
|
Name |
name()
returns the name of this element
|
void |
prettyPrint(PrettyPrinter w)
Pretty print.
|
java.lang.String |
proofToString() |
abstract Operator |
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() |
additionalValidTopLevel, argSort, argSorts, sort, sort
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
argSort, argSorts, sort
arity, bindVarsAt, isRigid, sort, validTopLevel, validTopLevelException
protected ProgramVariable(ProgramElementName name, Sort s, KeYJavaType t, KeYJavaType containingType, boolean isStatic, boolean isModel, boolean isGhost, boolean isFinal)
protected ProgramVariable(ProgramElementName name, Sort s, KeYJavaType t, KeYJavaType containingType, boolean isStatic, boolean isModel, boolean isGhost)
public ProgramElementName getProgramElementName()
public boolean isStatic()
public boolean isModel()
public boolean isGhost()
public boolean isFinal()
public boolean isMember()
public KeYJavaType getContainerType()
public SourceElement getFirstElement()
SourceElement
getFirstElement
in interface SourceElement
SourceElement.getStartPosition()
public SourceElement getFirstElementIncludingBlocks()
SourceElement
getFirstElementIncludingBlocks
in interface SourceElement
SourceElement.getStartPosition()
public SourceElement getLastElement()
SourceElement
getLastElement
in interface SourceElement
SourceElement.getEndPosition()
public Comment[] getComments()
ProgramElement
getComments
in interface ProgramElement
public void visit(Visitor v)
SourceElement
visit
in interface SourceElement
v
- the Visitorpublic void prettyPrint(PrettyPrinter w) throws java.io.IOException
SourceElement
prettyPrint
in interface SourceElement
w
- a pretty printer.java.io.IOException
- occasionally thrown.public Position getStartPosition()
SourceElement
getFirstElement()
.getStartPosition
in interface SourceElement
public Position getEndPosition()
SourceElement
getLastElement()
.getEndPosition
in interface SourceElement
public Position getRelativePosition()
SourceElement
getFirstElement()
.getRelativePosition
in interface SourceElement
public PositionInfo getPositionInfo()
SourceElement
getPositionInfo
in interface SourceElement
public KeYJavaType getKeYJavaType()
getKeYJavaType
in interface IProgramVariable
public KeYJavaType getKeYJavaType(Services javaServ)
getKeYJavaType
in interface IProgramVariable
public KeYJavaType getKeYJavaType(Services javaServ, ExecutionContext ec)
Expression
KeYJavaType
of an expressiongetKeYJavaType
in interface Expression
getKeYJavaType
in interface IProgramVariable
public ReferencePrefix getReferencePrefix()
getReferencePrefix
in interface ReferencePrefix
public boolean equalsModRenaming(SourceElement se, NameAbstractionTable nat)
equalsModRenaming
in interface SourceElement
public Expression convertToProgram(Term t, ExtList l)
convertToProgram
in interface ProgramInLogic
public java.lang.String proofToString()
public boolean isImplicit()
public MatchConditions match(SourceData source, MatchConditions matchCond)
ProgramElement
MatchConditions
with
the found instantiations of the schemavariables. If the match
failed, null is returned instead.match
in interface ProgramElement
source
- the SourceData with the program element to matchmatchCond
- the MatchConditions found up to this pointpublic abstract Operator rename(Name name)
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.