public final class ProgramSV extends AbstractSV implements ProgramConstruct, UpdateableOperator
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.
|
ImmutableList<LocationVariable> |
collectParameters() |
boolean |
equalsModRenaming(SourceElement se,
NameAbstractionTable nat)
this method tests on object identity
|
StatementBlock |
getBody() |
ProgramElement |
getChildAt(int index)
Returns the child at the specified index in this node's "virtual"
child array.
|
int |
getChildCount()
Returns the number of children of this node.
|
Comment[] |
getComments()
Get comments.
|
KeYJavaType |
getContainerType()
Returns the container type of this symbol; for non-static observer
symbols, this corresponds to the sort of its second argument.
|
int |
getDimensions() |
Position |
getEndPosition()
Returns the end position of the primary token of this element.
|
Expression |
getExpressionAt(int index) |
int |
getExpressionCount()
Get the number of expressions in this container.
|
SourceElement |
getFirstElement()
Finds the source element that occurs first in the source.
|
SourceElement |
getFirstElementIncludingBlocks()
Finds the source element that occurs first in the source.
|
java.lang.String |
getFullName() |
int |
getHeapCount(Services services)
Check the heap count of the declaration, e.g.
|
ImmutableArray<LoopInitializer> |
getInits() |
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.
|
IProgramMethod |
getMethodContext()
returns the program method which is currently active
|
MethodDeclaration |
getMethodDeclaration() |
ImmutableArray<Modifier> |
getModifiers()
Get the modifiers.
|
java.lang.String |
getName()
Return the name of the model element.
|
int |
getNumParams()
Gives the number of parameters of the observer symbol.
|
PackageReference |
getPackageReference()
Get the package reference.
|
ParameterDeclaration |
getParameterDeclarationAt(int index) |
int |
getParameterDeclarationCount() |
ImmutableArray<ParameterDeclaration> |
getParameters() |
KeYJavaType |
getParameterType(int i)
returns the KeYJavaType of the i-th parameter declaration.
|
KeYJavaType |
getParamType(int i)
Gives the type of the i-th parameter of this observer symbol.
|
ImmutableArray<KeYJavaType> |
getParamTypes()
Returns the parameter types of this observer symbol.
|
PositionInfo |
getPositionInfo()
complete position information
|
ProgramElementName |
getProgramElementName()
Get identifier.
|
ReferencePrefix |
getReferencePrefix() |
Position |
getRelativePosition()
Returns the relative position (number of blank heading lines and
columns) of the primary token of this element.
|
KeYJavaType |
getReturnType() |
ReferencePrefix |
getRuntimeInstance()
returns the runtime instance object
|
Position |
getStartPosition()
Returns the start position of the primary token of this element.
|
int |
getStateCount()
Check the state count of the declaration (no_state = 0, two_state = 2, 1 otherwise).
|
Statement |
getStatementAt(int i) |
int |
getStatementCount()
Get the number of statements in this container.
|
Throws |
getThrown() |
KeYJavaType |
getType()
Returns the result type of this symbol.
|
TypeReference |
getTypeReference()
returns the type reference to the next enclosing class
|
TypeReference |
getTypeReferenceAt(int index) |
int |
getTypeReferenceCount()
Get the number of type references in this container.
|
java.lang.String |
getUniqueName() |
ImmutableArray<Expression> |
getUpdates() |
VariableSpecification |
getVariableSpecification(int index)
Returns the variablespecification of the i-th parameterdeclaration
|
boolean |
isAbstract() |
boolean |
isConstructor()
Test whether the declaration is a constructor.
|
boolean |
isFinal() |
boolean |
isImplicit() |
boolean |
isListSV() |
boolean |
isModel()
Test whether the declaration is model.
|
boolean |
isNative() |
boolean |
isPrivate()
Test whether the declaration is private.
|
boolean |
isProtected()
Test whether the declaration is protected.
|
boolean |
isPublic()
Test whether the declaration is public.
|
boolean |
isRigid()
Tells whether the operator is rigid.
|
boolean |
isStatic()
Tells whether the observer symbol is static.
|
boolean |
isStrictFp()
Test whether the declaration is strictfp.
|
boolean |
isSynchronized() |
boolean |
isVoid() |
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()
Creates a parseable string representation of the declaration of the
schema variable.
|
int |
size() |
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() |
isStrict, toString
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 boolean isListSV()
public boolean equalsModRenaming(SourceElement se, NameAbstractionTable nat)
equalsModRenaming
in interface SourceElement
public Comment[] getComments()
ProgramElement
getComments
in interface Label
getComments
in interface ProgramElement
public SourceElement getFirstElement()
SourceElement
getFirstElement
in interface Label
getFirstElement
in interface SourceElement
SourceElement.getStartPosition()
public SourceElement getFirstElementIncludingBlocks()
SourceElement
getFirstElementIncludingBlocks
in interface SourceElement
SourceElement.getStartPosition()
public SourceElement getLastElement()
SourceElement
getLastElement
in interface Label
getLastElement
in interface SourceElement
SourceElement.getEndPosition()
public Position getStartPosition()
SourceElement
getFirstElement()
.getStartPosition
in interface Label
getStartPosition
in interface SourceElement
public Position getEndPosition()
SourceElement
getLastElement()
.getEndPosition
in interface Label
getEndPosition
in interface SourceElement
public Position getRelativePosition()
SourceElement
getFirstElement()
.getRelativePosition
in interface Label
getRelativePosition
in interface SourceElement
public PositionInfo getPositionInfo()
SourceElement
getPositionInfo
in interface SourceElement
public ReferencePrefix getReferencePrefix()
getReferencePrefix
in interface ReferencePrefix
getReferencePrefix
in interface TypeReference
public int getDimensions()
getDimensions
in interface TypeReference
public int getTypeReferenceCount()
TypeReferenceContainer
getTypeReferenceCount
in interface TypeReferenceContainer
public TypeReference getTypeReferenceAt(int index)
getTypeReferenceAt
in interface TypeReferenceContainer
public PackageReference getPackageReference()
PackageReferenceContainer
getPackageReference
in interface PackageReferenceContainer
public int getExpressionCount()
ExpressionContainer
getExpressionCount
in interface ExpressionContainer
public Expression getExpressionAt(int index)
getExpressionAt
in interface ExpressionContainer
getExpressionAt
in interface IForUpdates
public int getChildCount()
NonTerminalProgramElement
getChildCount
in interface NonTerminalProgramElement
public ProgramElement getChildAt(int index)
NonTerminalProgramElement
getChildAt
in interface NonTerminalProgramElement
index
- an index into this node's "virtual" child arraypublic int getStatementCount()
StatementContainer
getStatementCount
in interface StatementContainer
public int size()
size
in interface IForUpdates
size
in interface ILoopInit
public ImmutableArray<Expression> getUpdates()
getUpdates
in interface IForUpdates
public ImmutableArray<LoopInitializer> getInits()
public Statement getStatementAt(int i)
getStatementAt
in interface StatementContainer
public ProgramElementName getProgramElementName()
NamedProgramElement
getProgramElementName
in interface NamedProgramElement
getProgramElementName
in interface TypeReference
getProgramElementName
in interface IProgramMethod
public java.lang.String getName()
NamedModelElement
getName
in interface NamedModelElement
getName
in interface TypeReference
getName
in interface IProgramMethod
public void visit(Visitor v)
SourceElement
visit
in interface Label
visit
in interface SourceElement
v
- the Visitorpublic void prettyPrint(PrettyPrinter w) throws java.io.IOException
SourceElement
prettyPrint
in interface Label
prettyPrint
in interface SourceElement
w
- a pretty printer.java.io.IOException
- occasionally thrown.public KeYJavaType getKeYJavaType()
getKeYJavaType
in interface TypeReference
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 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 java.lang.String toString()
public java.lang.String proofToString()
SchemaVariable
proofToString
in interface SchemaVariable
public MethodDeclaration getMethodDeclaration()
getMethodDeclaration
in interface IProgramMethod
public KeYJavaType getParameterType(int i)
IProgramMethod
getParameterType
in interface IProgramMethod
i
- the int specifying the parameter positionpublic StatementBlock getBody()
getBody
in interface IProgramMethod
public boolean isConstructor()
IProgramMethod
isConstructor
in interface IProgramMethod
public boolean isModel()
IProgramMethod
isModel
in interface IProgramMethod
public int getStateCount()
IObserverFunction
getStateCount
in interface IObserverFunction
public int getHeapCount(Services services)
IObserverFunction
getHeapCount
in interface IObserverFunction
public boolean isVoid()
isVoid
in interface IProgramMethod
public KeYJavaType getReturnType()
getReturnType
in interface IProgramMethod
public java.lang.String getUniqueName()
getUniqueName
in interface IProgramMethod
public java.lang.String getFullName()
getFullName
in interface IProgramMethod
public boolean isAbstract()
isAbstract
in interface IProgramMethod
public boolean isImplicit()
isImplicit
in interface IProgramMethod
public boolean isNative()
isNative
in interface IProgramMethod
public boolean isFinal()
isFinal
in interface IProgramMethod
public boolean isSynchronized()
isSynchronized
in interface IProgramMethod
public Throws getThrown()
getThrown
in interface IProgramMethod
public ParameterDeclaration getParameterDeclarationAt(int index)
getParameterDeclarationAt
in interface IProgramMethod
public VariableSpecification getVariableSpecification(int index)
IProgramMethod
getVariableSpecification
in interface IProgramMethod
public int getParameterDeclarationCount()
getParameterDeclarationCount
in interface IProgramMethod
public ImmutableArray<ParameterDeclaration> getParameters()
getParameters
in interface IProgramMethod
public ImmutableList<LocationVariable> collectParameters()
collectParameters
in interface IProgramMethod
LocationVariable
s passed as parameters to
this IProgramMethod
.public boolean isPrivate()
MemberDeclaration
isPrivate
in interface MemberDeclaration
public boolean isProtected()
MemberDeclaration
isProtected
in interface MemberDeclaration
public boolean isPublic()
MemberDeclaration
isPublic
in interface MemberDeclaration
public boolean isStatic()
IObserverFunction
isStatic
in interface MemberDeclaration
isStatic
in interface IObserverFunction
public boolean isStrictFp()
MemberDeclaration
isStrictFp
in interface MemberDeclaration
public ImmutableArray<Modifier> getModifiers()
Declaration
getModifiers
in interface Declaration
public ImmutableArray<KeYJavaType> getParamTypes()
IObserverFunction
getParamTypes
in interface IObserverFunction
getParamTypes
in interface IProgramMethod
public KeYJavaType getType()
IObserverFunction
getType
in interface IObserverFunction
public KeYJavaType getContainerType()
IObserverFunction
getContainerType
in interface IObserverFunction
public int getNumParams()
IObserverFunction
getNumParams
in interface IObserverFunction
public KeYJavaType getParamType(int i)
IObserverFunction
getParamType
in interface IObserverFunction
public TypeReference getTypeReference()
IExecutionContext
getTypeReference
in interface IExecutionContext
public IProgramMethod getMethodContext()
IExecutionContext
getMethodContext
in interface IExecutionContext
public ReferencePrefix getRuntimeInstance()
IExecutionContext
getRuntimeInstance
in interface IExecutionContext
protected 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 recogniseCopyright © 2003-2019 The KeY-Project.