ProgramSV (KeY API Documentation)

java.lang.Object
- de.uka.ilkd.key.logic.op.AbstractOperator
- - de.uka.ilkd.key.logic.op.AbstractSortedOperator
  - - de.uka.ilkd.key.logic.op.AbstractSV
    - - de.uka.ilkd.key.logic.op.ProgramSV

All Implemented Interfaces:

Declaration, MemberDeclaration, Expression, ExpressionStatement, ExpressionContainer, Label, LoopInitializer, ModelElement, NamedModelElement, NamedProgramElement, NonTerminalProgramElement, ProgramElement, Reference, IExecutionContext, MemberReference, MethodName, NameReference, PackageReferenceContainer, ReferencePrefix, ReferenceSuffix, TypeReference, TypeReferenceContainer, TypeReferenceInfix, SourceElement, Statement, Branch, IForUpdates, IGuard, ILoopInit, StatementContainer, TerminalProgramElement, Named, IObserverFunction, IProgramMethod, IProgramVariable, Operator, ParsableVariable, SchemaVariable, SortedOperator, SVSubstitute, UpdateableOperator, ProgramConstruct, Sorted
```
public final class ProgramSV
extends AbstractSV
implements ProgramConstruct, UpdateableOperator
```
Objects of this class are schema variables matching program constructs within modal operators. The particular construct being matched is determined by the ProgramSVSort of the schema variable.

Field Summary

Fields
Modifier and Type Field and Description

private static ProgramList EMPTY_LIST_INSTANTIATION

private boolean isListSV

Fields
Modifier and Type	Field and Description
`private static ProgramList`	`EMPTY_LIST_INSTANTIATION`
`private boolean`	`isListSV`

Constructor Summary

Constructors
Constructor and Description

ProgramSV(Name name, ProgramSVSort s, boolean isListSV)
creates a new SchemaVariable used as a placeholder for program constructs

Constructors
Constructor and Description
`ProgramSV(Name name, ProgramSVSort s, boolean isListSV)` creates a new SchemaVariable used as a placeholder for program constructs

Method Summary

All Methods Instance Methods Concrete Methods
Modifier and Type	Method and Description
`private MatchConditions`	`addProgramInstantiation(ProgramElement pe, MatchConditions matchCond, Services services)` adds a found mapping from schema variable `var` to program element `pe` and returns the updated match conditions or null if mapping is not possible because of violating some variable condition
`private MatchConditions`	`addProgramInstantiation(ProgramList list, MatchConditions matchCond, Services services)` adds a found mapping from schema variable `var` to the list of program elements `list` and returns the updated match conditions or null if mapping is not possible because of violating some variable condition
`private boolean`	`check(ProgramElement match, ExecutionContext ec, Services services)` returns true, if the given SchemaVariable can stand for the ProgramElement
`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. the base heap and extra heap.
`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`	`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.
`private MatchConditions`	`matchListSV(SourceData source, MatchConditions matchCond)`
`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`	`visit(Visitor v)` calls the corresponding method of a visitor in order to perform some action/transformation on this element

Methods inherited from class de.uka.ilkd.key.logic.op.AbstractSV
isStrict, toString

Methods inherited from class de.uka.ilkd.key.logic.op.AbstractSortedOperator
additionalValidTopLevel, additionalValidTopLevel2, argSort, argSorts, sort, sort

Methods inherited from class de.uka.ilkd.key.logic.op.AbstractOperator
arity, bindVarsAt, isRigid, name, validTopLevel, whereToBind

Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Methods inherited from interface de.uka.ilkd.key.logic.op.SortedOperator
argSort, argSorts, sort

Methods inherited from interface de.uka.ilkd.key.logic.op.Operator
arity, bindVarsAt, isRigid, sort, validTopLevel

Methods inherited from interface de.uka.ilkd.key.logic.Named
name

- Field Detail
  - EMPTY_LIST_INSTANTIATION
```
private static final ProgramList EMPTY_LIST_INSTANTIATION
```
  - isListSV
```
private final boolean isListSV
```
- Constructor Detail
  - ProgramSV
```
ProgramSV(Name name,
          ProgramSVSort s,
          boolean isListSV)
```
    creates a new SchemaVariable used as a placeholder for program constructs
    
    Parameters:
    
    name - the Name of the SchemaVariable allowed to match a list of program constructs
- Method Detail
  - isListSV
```
public boolean isListSV()
```
  - equalsModRenaming
```
public boolean equalsModRenaming(SourceElement se,
                                 NameAbstractionTable nat)
```
    this method tests on object identity
    
    Specified by:
    
    equalsModRenaming in interface SourceElement
  - getComments
```
public Comment[] getComments()
```
    Description copied from interface: ProgramElement
    
    Get comments.
    
    Specified by:
    
    getComments in interface Label
    
    Specified by:
    
    getComments in interface ProgramElement
    
    Returns:
    
    comments if the schemavariable stands for programm construct and has comments attached to it (not supported yet)
  - getFirstElement
```
public SourceElement getFirstElement()
```
    Description copied from interface: SourceElement
    
    Finds the source element that occurs first in the source.
    
    Specified by:
    
    getFirstElement in interface Label
    
    Specified by:
    
    getFirstElement in interface SourceElement
    
    Returns:
    
    the first source element in the syntactical representation of this element, may be equals to this element.
    
    See Also:
    
    SourceElement.getStartPosition()
  - getFirstElementIncludingBlocks
```
public SourceElement getFirstElementIncludingBlocks()
```
    Description copied from interface: SourceElement
    
    Finds the source element that occurs first in the source.
    
    Specified by:
    
    getFirstElementIncludingBlocks in interface SourceElement
    
    Returns:
    
    the first source element in the syntactical representation of this element, may be equals to this element.
    
    See Also:
    
    SourceElement.getStartPosition()
  - getLastElement
```
public SourceElement getLastElement()
```
    Description copied from interface: SourceElement
    
    Finds the source element that occurs last in the source.
    
    Specified by:
    
    getLastElement in interface Label
    
    Specified by:
    
    getLastElement in interface SourceElement
    
    Returns:
    
    the last source element in the syntactical representation of this element, may be equals to this element.
    
    See Also:
    
    SourceElement.getEndPosition()
  - getStartPosition
```
public Position getStartPosition()
```
    Description copied from interface: SourceElement
    
    Returns the start position of the primary token of this element. To get the start position of the syntactical first token, call the corresponding method of getFirstElement().
    
    Specified by:
    
    getStartPosition in interface Label
    
    Specified by:
    
    getStartPosition in interface SourceElement
    
    Returns:
    
    the start position of the primary token.
  - getEndPosition
```
public Position getEndPosition()
```
    Description copied from interface: SourceElement
    
    Returns the end position of the primary token of this element. To get the end position of the syntactical first token, call the corresponding method of getLastElement().
    
    Specified by:
    
    getEndPosition in interface Label
    
    Specified by:
    
    getEndPosition in interface SourceElement
    
    Returns:
    
    the end position of the primary token.
  - getRelativePosition
```
public Position getRelativePosition()
```
    Description copied from interface: SourceElement
    
    Returns the relative position (number of blank heading lines and columns) of the primary token of this element. To get the relative position of the syntactical first token, call the corresponding method of getFirstElement().
    
    Specified by:
    
    getRelativePosition in interface Label
    
    Specified by:
    
    getRelativePosition in interface SourceElement
    
    Returns:
    
    the relative position of the primary token.
  - getPositionInfo
```
public PositionInfo getPositionInfo()
```
    Description copied from interface: SourceElement
    
    complete position information
    
    Specified by:
    
    getPositionInfo in interface SourceElement
  - getReferencePrefix
```
public ReferencePrefix getReferencePrefix()
```
    Specified by:
    
    getReferencePrefix in interface ReferencePrefix
    
    Specified by:
    
    getReferencePrefix in interface TypeReference
  - getDimensions
```
public int getDimensions()
```
    Specified by:
    
    getDimensions in interface TypeReference
  - getTypeReferenceCount
```
public int getTypeReferenceCount()
```
    Description copied from interface: TypeReferenceContainer
    
    Get the number of type references in this container.
    
    Specified by:
    
    getTypeReferenceCount in interface TypeReferenceContainer
    
    Returns:
    
    the number of type references.
  - getTypeReferenceAt
```
public TypeReference getTypeReferenceAt(int index)
```
    Specified by:
    
    getTypeReferenceAt in interface TypeReferenceContainer
  - getPackageReference
```
public PackageReference getPackageReference()
```
    Description copied from interface: PackageReferenceContainer
    
    Get the package reference.
    
    Specified by:
    
    getPackageReference in interface PackageReferenceContainer
    
    Returns:
    
    the package reference.
  - getExpressionCount
```
public int getExpressionCount()
```
    Description copied from interface: ExpressionContainer
    
    Get the number of expressions in this container.
    
    Specified by:
    
    getExpressionCount in interface ExpressionContainer
    
    Returns:
    
    the number of expressions.
  - getExpressionAt
```
public Expression getExpressionAt(int index)
```
    Specified by:
    
    getExpressionAt in interface ExpressionContainer
    
    Specified by:
    
    getExpressionAt in interface IForUpdates
  - getChildCount
```
public int getChildCount()
```
    Description copied from interface: NonTerminalProgramElement
    
    Returns the number of children of this node.
    
    Specified by:
    
    getChildCount in interface NonTerminalProgramElement
    
    Returns:
    
    an int giving the number of children of this node
  - getChildAt
```
public ProgramElement getChildAt(int index)
```
    Description copied from interface: NonTerminalProgramElement
    
    Returns the child at the specified index in this node's "virtual" child array.
    
    Specified by:
    
    getChildAt in interface NonTerminalProgramElement
    
    Parameters:
    
    index - an index into this node's "virtual" child array
    
    Returns:
    
    the program element at the given position
  - getStatementCount
```
public int getStatementCount()
```
    Description copied from interface: StatementContainer
    
    Get the number of statements in this container.
    
    Specified by:
    
    getStatementCount in interface StatementContainer
    
    Returns:
    
    the number of statements.
  - size
```
public int size()
```
    Specified by:
    
    size in interface IForUpdates
    
    Specified by:
    
    size in interface ILoopInit
  - getUpdates
```
public ImmutableArray<Expression> getUpdates()
```
    Specified by:
    
    getUpdates in interface IForUpdates
  - getInits
```
public ImmutableArray<LoopInitializer> getInits()
```
    Specified by:
    
    getInits in interface ILoopInit
  - getStatementAt
```
public Statement getStatementAt(int i)
```
    Specified by:
    
    getStatementAt in interface StatementContainer
  - getProgramElementName
```
public ProgramElementName getProgramElementName()
```
    Description copied from interface: NamedProgramElement
    
    Get identifier.
    
    Specified by:
    
    getProgramElementName in interface NamedProgramElement
    
    Specified by:
    
    getProgramElementName in interface TypeReference
    
    Specified by:
    
    getProgramElementName in interface IProgramMethod
    
    Returns:
    
    the identifier.
  - getName
```
public java.lang.String getName()
```
    Description copied from interface: NamedModelElement
    
    Return the name of the model element.
    
    Specified by:
    
    getName in interface NamedModelElement
    
    Specified by:
    
    getName in interface TypeReference
    
    Specified by:
    
    getName in interface IProgramMethod
    
    Returns:
    
    the name of the model element.
  - visit
```
public void visit(Visitor v)
```
    Description copied from interface: SourceElement
    
    calls the corresponding method of a visitor in order to perform some action/transformation on this element
    
    Specified by:
    
    visit in interface Label
    
    Specified by:
    
    visit in interface SourceElement
    
    Parameters:
    
    v - the Visitor
  - prettyPrint
```
public void prettyPrint(PrettyPrinter w)
                 throws java.io.IOException
```
    Description copied from interface: SourceElement
    
    Pretty print.
    
    Specified by:
    
    prettyPrint in interface Label
    
    Specified by:
    
    prettyPrint in interface SourceElement
    
    Parameters:
    
    w - a pretty printer.
    
    Throws:
    
    java.io.IOException - occasionally thrown.
  - getKeYJavaType
```
public KeYJavaType getKeYJavaType()
```
    Specified by:
    
    getKeYJavaType in interface TypeReference
    
    Specified by:
    
    getKeYJavaType in interface IProgramVariable
  - getKeYJavaType
```
public KeYJavaType getKeYJavaType(Services javaServ)
```
    Specified by:
    
    getKeYJavaType in interface IProgramVariable
  - getKeYJavaType
```
public KeYJavaType getKeYJavaType(Services javaServ,
                                  ExecutionContext ec)
```
    Description copied from interface: Expression
    
    returns the KeYJavaType of an expression
    
    Specified by:
    
    getKeYJavaType in interface Expression
    
    Specified by:
    
    getKeYJavaType in interface IProgramVariable
  - addProgramInstantiation
```
private MatchConditions addProgramInstantiation(ProgramElement pe,
                                                MatchConditions matchCond,
                                                Services services)
```
    adds a found mapping from schema variable var to program element pe and returns the updated match conditions or null if mapping is not possible because of violating some variable condition
    
    Parameters:
    
    pe - the ProgramElement var is mapped to
    
    matchCond - the MatchConditions to be updated
    
    services - the Services provide access to the Java model
    
    Returns:
    
    the updated match conditions including mapping var to pe or null if some variable condition would be hurt by the mapping
  - addProgramInstantiation
```
private MatchConditions addProgramInstantiation(ProgramList list,
                                                MatchConditions matchCond,
                                                Services services)
```
    adds a found mapping from schema variable var to the list of program elements list and returns the updated match conditions or null if mapping is not possible because of violating some variable condition
    
    Parameters:
    
    list - the ProgramList var is mapped to
    
    matchCond - the MatchConditions to be updated
    
    services - the Services provide access to the Java model
    
    Returns:
    
    the updated match conditions including mapping var to list or null if some variable condition would be hurt by the mapping
  - matchListSV
```
private MatchConditions matchListSV(SourceData source,
                                    MatchConditions matchCond)
```
  - check
```
private boolean check(ProgramElement match,
                      ExecutionContext ec,
                      Services services)
```
    returns true, if the given SchemaVariable can stand for the ProgramElement
    
    Parameters:
    
    match - the ProgramElement to be matched
    
    services - the Services object encapsulating information about the java datastructures like (static)types etc.
    
    Returns:
    
    true if the SchemaVariable can stand for the given element
  - match
```
public MatchConditions match(SourceData source,
                             MatchConditions matchCond)
```
    Description copied from interface: ProgramElement
    
    matches the source "text" (@link SourceData#getSource()) against the pattern represented by this object. In case of a successful match the resulting MatchConditions with the found instantiations of the schemavariables. If the match failed, null is returned instead.
    
    Specified by:
    
    match in interface ProgramElement
    
    Parameters:
    
    source - the SourceData with the program element to match
    
    matchCond - the MatchConditions found up to this point
    
    Returns:
    
    the resulting match conditions or null if the match failed
  - toString
```
public java.lang.String toString()
```
    Overrides:
    
    toString in class AbstractOperator
  - proofToString
```
public java.lang.String proofToString()
```
    Description copied from interface: SchemaVariable
    
    Creates a parseable string representation of the declaration of the schema variable.
    
    Specified by:
    
    proofToString in interface SchemaVariable
  - getMethodDeclaration
```
public MethodDeclaration getMethodDeclaration()
```
    Specified by:
    
    getMethodDeclaration in interface IProgramMethod
  - getParameterType
```
public KeYJavaType getParameterType(int i)
```
    Description copied from interface: IProgramMethod
    
    returns the KeYJavaType of the i-th parameter declaration. This method does not care about the invoker as argSort does.
    
    Specified by:
    
    getParameterType in interface IProgramMethod
    
    Parameters:
    
    i - the int specifying the parameter position
    
    Returns:
    
    the KeYJavaType of the i-th parameter
  - getBody
```
public StatementBlock getBody()
```
    Specified by:
    
    getBody in interface IProgramMethod
  - isConstructor
```
public boolean isConstructor()
```
    Description copied from interface: IProgramMethod
    
    Test whether the declaration is a constructor.
    
    Specified by:
    
    isConstructor in interface IProgramMethod
  - isModel
```
public boolean isModel()
```
    Description copied from interface: IProgramMethod
    
    Test whether the declaration is model.
    
    Specified by:
    
    isModel in interface IProgramMethod
  - getStateCount
```
public int getStateCount()
```
    Description copied from interface: IObserverFunction
    
    Check the state count of the declaration (no_state = 0, two_state = 2, 1 otherwise).
    
    Specified by:
    
    getStateCount in interface IObserverFunction
  - getHeapCount
```
public int getHeapCount(Services services)
```
    Description copied from interface: IObserverFunction
    
    Check the heap count of the declaration, e.g. the base heap and extra heap.
    
    Specified by:
    
    getHeapCount in interface IObserverFunction
  - isVoid
```
public boolean isVoid()
```
    Specified by:
    
    isVoid in interface IProgramMethod
  - getReturnType
```
public KeYJavaType getReturnType()
```
    Specified by:
    
    getReturnType in interface IProgramMethod
    
    Returns:
    
    the return type
  - getUniqueName
```
public java.lang.String getUniqueName()
```
    Specified by:
    
    getUniqueName in interface IProgramMethod
  - getFullName
```
public java.lang.String getFullName()
```
    Specified by:
    
    getFullName in interface IProgramMethod
  - isAbstract
```
public boolean isAbstract()
```
    Specified by:
    
    isAbstract in interface IProgramMethod
  - isImplicit
```
public boolean isImplicit()
```
    Specified by:
    
    isImplicit in interface IProgramMethod
  - isNative
```
public boolean isNative()
```
    Specified by:
    
    isNative in interface IProgramMethod
  - isFinal
```
public boolean isFinal()
```
    Specified by:
    
    isFinal in interface IProgramMethod
  - isSynchronized
```
public boolean isSynchronized()
```
    Specified by:
    
    isSynchronized in interface IProgramMethod
  - getThrown
```
public Throws getThrown()
```
    Specified by:
    
    getThrown in interface IProgramMethod
  - getParameterDeclarationAt
```
public ParameterDeclaration getParameterDeclarationAt(int index)
```
    Specified by:
    
    getParameterDeclarationAt in interface IProgramMethod
  - getVariableSpecification
```
public VariableSpecification getVariableSpecification(int index)
```
    Description copied from interface: IProgramMethod
    
    Returns the variablespecification of the i-th parameterdeclaration
    
    Specified by:
    
    getVariableSpecification in interface IProgramMethod
  - getParameterDeclarationCount
```
public int getParameterDeclarationCount()
```
    Specified by:
    
    getParameterDeclarationCount in interface IProgramMethod
  - getParameters
```
public ImmutableArray<ParameterDeclaration> getParameters()
```
    Specified by:
    
    getParameters in interface IProgramMethod
  - collectParameters
```
public ImmutableList<LocationVariable> collectParameters()
```
    Specified by:
    
    collectParameters in interface IProgramMethod
    
    Returns:
    
    The list of LocationVariables passed as parameters to this IProgramMethod.
  - isPrivate
```
public boolean isPrivate()
```
    Description copied from interface: MemberDeclaration
    
    Test whether the declaration is private.
    
    Specified by:
    
    isPrivate in interface MemberDeclaration
  - isProtected
```
public boolean isProtected()
```
    Description copied from interface: MemberDeclaration
    
    Test whether the declaration is protected.
    
    Specified by:
    
    isProtected in interface MemberDeclaration
  - isPublic
```
public boolean isPublic()
```
    Description copied from interface: MemberDeclaration
    
    Test whether the declaration is public.
    
    Specified by:
    
    isPublic in interface MemberDeclaration
  - isStatic
```
public boolean isStatic()
```
    Description copied from interface: IObserverFunction
    
    Tells whether the observer symbol is static.
    
    Specified by:
    
    isStatic in interface MemberDeclaration
    
    Specified by:
    
    isStatic in interface IObserverFunction
  - isStrictFp
```
public boolean isStrictFp()
```
    Description copied from interface: MemberDeclaration
    
    Test whether the declaration is strictfp.
    
    Specified by:
    
    isStrictFp in interface MemberDeclaration
  - getModifiers
```
public ImmutableArray<Modifier> getModifiers()
```
    Description copied from interface: Declaration
    
    Get the modifiers.
    
    Specified by:
    
    getModifiers in interface Declaration
    
    Returns:
    
    the (original) list of modifiers wrapped .
  - getParamTypes
```
public ImmutableArray<KeYJavaType> getParamTypes()
```
    Description copied from interface: IObserverFunction
    
    Returns the parameter types of this observer symbol. "Parameters" here includes only the *explicit* parameters, not the heap and the receiver object.
    
    Specified by:
    
    getParamTypes in interface IObserverFunction
    
    Specified by:
    
    getParamTypes in interface IProgramMethod
  - getType
```
public KeYJavaType getType()
```
    Description copied from interface: IObserverFunction
    
    Returns the result type of this symbol.
    
    Specified by:
    
    getType in interface IObserverFunction
  - getContainerType
```
public KeYJavaType getContainerType()
```
    Description copied from interface: IObserverFunction
    
    Returns the container type of this symbol; for non-static observer symbols, this corresponds to the sort of its second argument.
    
    Specified by:
    
    getContainerType in interface IObserverFunction
  - getNumParams
```
public int getNumParams()
```
    Description copied from interface: IObserverFunction
    
    Gives the number of parameters of the observer symbol. "Parameters" here includes only the *explicit* parameters, not the heap and the receiver object. Thus, for observer symbols representing model fields, this will always return 0.
    
    Specified by:
    
    getNumParams in interface IObserverFunction
  - getParamType
```
public KeYJavaType getParamType(int i)
```
    Description copied from interface: IObserverFunction
    
    Gives the type of the i-th parameter of this observer symbol. "Parameters" here includes only the *explicit* parameters, not the heap and the receiver object.
    
    Specified by:
    
    getParamType in interface IObserverFunction
  - getTypeReference
```
public TypeReference getTypeReference()
```
    Description copied from interface: IExecutionContext
    
    returns the type reference to the next enclosing class
    
    Specified by:
    
    getTypeReference in interface IExecutionContext
    
    Returns:
    
    the type reference to the next enclosing class
  - getMethodContext
```
public IProgramMethod getMethodContext()
```
    Description copied from interface: IExecutionContext
    
    returns the program method which is currently active
    
    Specified by:
    
    getMethodContext in interface IExecutionContext
    
    Returns:
    
    the currently active method
  - getRuntimeInstance
```
public ReferencePrefix getRuntimeInstance()
```
    Description copied from interface: IExecutionContext
    
    returns the runtime instance object
    
    Specified by:
    
    getRuntimeInstance in interface IExecutionContext
    
    Returns:
    
    the runtime instance object

Class ProgramSV

Field Summary

Constructor Summary

Method Summary

Methods inherited from class de.uka.ilkd.key.logic.op.AbstractSV

Methods inherited from class de.uka.ilkd.key.logic.op.AbstractSortedOperator

Methods inherited from class de.uka.ilkd.key.logic.op.AbstractOperator

Methods inherited from class java.lang.Object

Methods inherited from interface de.uka.ilkd.key.logic.op.SortedOperator

Methods inherited from interface de.uka.ilkd.key.logic.op.Operator

Methods inherited from interface de.uka.ilkd.key.logic.Named

Field Detail

EMPTY_LIST_INSTANTIATION

isListSV

Constructor Detail

ProgramSV

Method Detail

isListSV

equalsModRenaming

getComments

getFirstElement

getFirstElementIncludingBlocks

getLastElement

getStartPosition

getEndPosition

getRelativePosition

getPositionInfo

getReferencePrefix

getDimensions

getTypeReferenceCount

getTypeReferenceAt

getPackageReference

getExpressionCount

getExpressionAt

getChildCount

getChildAt

getStatementCount

size

getUpdates

getInits

getStatementAt

getProgramElementName

getName

visit

prettyPrint

getKeYJavaType

getKeYJavaType

getKeYJavaType

addProgramInstantiation

addProgramInstantiation

matchListSV

check

match

toString

proofToString

getMethodDeclaration

getParameterType

getBody

isConstructor

isModel

getStateCount

getHeapCount

isVoid

getReturnType

getUniqueName

getFullName

isAbstract

isImplicit

isNative

isFinal

isSynchronized

getThrown

getParameterDeclarationAt

getVariableSpecification

getParameterDeclarationCount

getParameters

collectParameters

isPrivate

isProtected

isPublic