| java.lang.Object
 de.uka.ilkd.key.logic.op.TermSymbol
de.uka.ilkd.key.logic.op.Function
de.uka.ilkd.key.logic.op.NonRigidFunction
All known Subclasses: de.uka.ilkd.key.logic.op.ExpressionOperator, de.uka.ilkd.key.logic.op.ProgramMethod, de.uka.ilkd.key.rule.soundness.SVSkolemFunction, de.uka.ilkd.key.logic.op.NRFunctionWithExplicitDependencies, de.uka.ilkd.key.logic.op.ConstructorFunction, de.uka.ilkd.key.logic.op.NonRigidHeapDependentFunction,
| NonRigidFunction | | public class NonRigidFunction extends Function implements NonRigid(Code) | | Non-rigid function or predicate symbols are realised as instances
of this class. Some particular non-rigid functions
(namely attributes and arrays) are currently bypassing this class,
but should be integrated into this framework in the mid-future (this
was written 2005, may be you read this in the year 2035;-).
|
| NonRigidFunction | | public NonRigidFunction(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 |
| NonRigidFunction | | public NonRigidFunction(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 ArrayOfSort defining the argument sorts |
| isRigid | | public boolean isRigid(Term term)(Code) | | true if the value of "term" having this operator astop-level operator and may not be changed by modalities |
|
|