de.uka.ilkd.key.logic.op

Class ObserverFunction

java.lang.Object

de.uka.ilkd.key.logic.op.AbstractOperator

de.uka.ilkd.key.logic.op.AbstractSortedOperator

de.uka.ilkd.key.logic.op.Function

de.uka.ilkd.key.logic.op.ObserverFunction

All Implemented Interfaces:

Named, IObserverFunction, Operator, SortedOperator, SVSubstitute, Sorted

Direct Known Subclasses:

ProgramMethod

public class ObserverFunction
extends Function
implements IObserverFunction

Objects of this class represent "observer" function or predicate symbols. An observer symbol is a symbol taking a heap array as its first argument, and an object as its second argument (unless it is static). Observer symbols are used to represent JML model fields as well as occurrences of pure methods in specifications (via the subclass ProgramMethod). As they come from the Java program, both their parameter sorts and their result sorts always have an associated KeYJavaType. Observer symbols serve as the targets of contracts (i.e., as the subjects that the contracts are about).

Field Summary

Fields

Modifier and Type	Field and Description
private KeYJavaType	container
private int	heapCount
private boolean	isStatic
private ImmutableArray<KeYJavaType>	paramTypes
private int	stateCount
private KeYJavaType	type

Constructor Summary

Constructors

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)

Method Summary

Modifier and Type	Method and Description
static ProgramElementName	createName(java.lang.String baseName, KeYJavaType container)
private static Sort[]	getArgSorts(Sort heapSort, KeYJavaType container, boolean isStatic, ImmutableArray<KeYJavaType> paramTypes, int heapCount, int stateCount)
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. the base heap and extra heap.
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	isStatic() Tells whether the observer symbol is static.

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

isSkolemConstant, isUnique, proofToString, rename, 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

container

private final KeYJavaType container

isStatic

private final boolean isStatic

paramTypes

private final ImmutableArray<KeYJavaType> paramTypes

type

private final KeYJavaType type

heapCount

private final int heapCount

stateCount

private final int stateCount

Constructor Detail

ObserverFunction

public ObserverFunction(java.lang.String baseName,
                        Sort sort,
                        KeYJavaType type,
                        Sort heapSort,
                        KeYJavaType container,
                        boolean isStatic,
                        ImmutableArray<KeYJavaType> paramTypes,
                        int heapCount,
                        int stateCount)

Method Detail

createName

public static ProgramElementName createName(java.lang.String baseName,
                                            KeYJavaType container)

getArgSorts

private static Sort[] getArgSorts(Sort heapSort,
                                  KeYJavaType container,
                                  boolean isStatic,
                                  ImmutableArray<KeYJavaType> paramTypes,
                                  int heapCount,
                                  int stateCount)

getType

public final KeYJavaType getType()

Description copied from interface: IObserverFunction

Returns the result type of this symbol.

Specified by:

getType in interface IObserverFunction

getContainerType

public final 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

isStatic

public final boolean isStatic()

Description copied from interface: IObserverFunction

Tells whether the observer symbol is static.

Specified by:

isStatic in interface IObserverFunction

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

getNumParams

public final 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 final 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

getParamTypes

public final 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