public class ObserverFunction extends Function implements IObserverFunction
Constructor and Description |
---|
ObserverFunction(java.lang.String baseName,
Sort sort,
KeYJavaType type,
Sort heapSort,
KeYJavaType container,
boolean isStatic,
ImmutableArray<KeYJavaType> paramTypes,
int heapCount,
int stateCount) |
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.
|
static ProgramElementName |
createName(java.lang.String baseName,
KeYJavaType container) |
KeYJavaType |
getContainerType()
Returns the container type of this symbol; for non-static observer
symbols, this corresponds to the sort of its second argument.
|
int |
getHeapCount(Services services)
Check the heap count of the declaration, e.g.
|
int |
getNumParams()
Gives the number of parameters of the observer symbol.
|
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.
|
int |
getStateCount()
Check the state count of the declaration (no_state = 0, two_state = 2, 1 otherwise).
|
KeYJavaType |
getType()
Returns the result type of this symbol.
|
boolean |
isRigid()
Tells whether the operator is rigid.
|
boolean |
isStatic()
Tells whether the observer symbol is static.
|
Name |
name()
returns the name of this element
|
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.
|
protected ImmutableArray<java.lang.Boolean> |
whereToBind() |
isSkolemConstant, isUnique, proofToString, rename, 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 ObserverFunction(java.lang.String baseName, Sort sort, KeYJavaType type, Sort heapSort, KeYJavaType container, boolean isStatic, ImmutableArray<KeYJavaType> paramTypes, int heapCount, int stateCount)
public static ProgramElementName createName(java.lang.String baseName, KeYJavaType container)
public final KeYJavaType getType()
IObserverFunction
getType
in interface IObserverFunction
public final KeYJavaType getContainerType()
IObserverFunction
getContainerType
in interface IObserverFunction
public final boolean isStatic()
IObserverFunction
isStatic
in interface IObserverFunction
public int getStateCount()
IObserverFunction
getStateCount
in interface IObserverFunction
public int getHeapCount(Services services)
IObserverFunction
getHeapCount
in interface IObserverFunction
public final int getNumParams()
IObserverFunction
getNumParams
in interface IObserverFunction
public final KeYJavaType getParamType(int i)
IObserverFunction
getParamType
in interface IObserverFunction
public final ImmutableArray<KeYJavaType> getParamTypes()
IObserverFunction
getParamTypes
in interface IObserverFunction
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.