| java.lang.Object de.uka.ilkd.key.logic.op.TermSymbol de.uka.ilkd.key.logic.op.Function de.uka.ilkd.key.logic.op.NonRigidFunction de.uka.ilkd.key.logic.op.NonRigidHeapDependentFunction
NonRigidHeapDependentFunction | public class NonRigidHeapDependentFunction extends NonRigidFunction (Code) | | Instances of this classes represent non-rigid functions, which dependent only on the
state of the heap and not of any local variables. This means their interpretation coincides
on all states that describe the same heap.
A famous representant of this kind of function is the inReachableState predicate.
|
NonRigidHeapDependentFunction | public NonRigidHeapDependentFunction(Name name, Sort sort, ArrayOfSort argSorts)(Code) | | creates a non rigid function with given signature
Parameters: name - the Name of the non-rigid function symbol Parameters: sort - the Sort of the symbol Parameters: argSorts - the array of Sort defining the argument sorts |
NonRigidHeapDependentFunction | public NonRigidHeapDependentFunction(Name name, Sort sort, Sort[] argSorts)(Code) | | creates a non rigid function with given signature
Parameters: name - the Name of the non-rigid function symbol Parameters: sort - the Sort of the symbol Parameters: argSorts - the array of Sort defining the argument sorts |
|
|