| de.uka.ilkd.key.logic.op |
|
contains the operators of {@link
de.uka.ilkd.key.logic.Term}s. Operators may be {@link
de.uka.ilkd.key.logic.op.Quantifier}s or {@link
de.uka.ilkd.key.logic.op.SubstOp}s that bind variables for
subterms, but also {@link de.uka.ilkd.key.logic.op.Modality}s, or
{@link de.uka.ilkd.key.logic.op.QuanUpdateOperator}s. Many of the operators
are constantly defined in {@link de.uka.ilkd.key.logic.op.Op}s.
An operator can be a {@link de.uka.ilkd.key.logic.op.TermSymbol}s,
such as a {@link de.uka.ilkd.key.logic.op.Function} or a
variable. There are several kind of variables: {@link
de.uka.ilkd.key.logic.op.LogicVariable}s (variables that must be
bound but do not occur in programs), {@link
de.uka.ilkd.key.logic.op.ProgramVariable}s (allowed both in
programs and in logic, but not boundable), {@link
de.uka.ilkd.key.logic.op.Metavariable}s, and {@link
de.uka.ilkd.key.logic.op.SchemaVariable}s for {@link
de.uka.ilkd.key.rule.Taclet}s.
Last modified: Mon Apr 18 09:42:36 MEST 2005
|
| Java Source File Name | Type | Comment |
| AbstractMetaOperator.java | Class | this class implements the interface for
MetaOperators. |
| AbstractTermSV.java | Class | |
| AccessOp.java | Class | |
| AnonymousUpdate.java | Class | |
| ArrayOp.java | Class | |
| AttributeOp.java | Class | |
| CastFunctionSymbol.java | Class | This function symbol is created for casts to the depending sort. |
| ComputeSpecOp.java | Class | This compute spec operator is used for computing spec. |
| ConstructorFunction.java | Class | A Constructor is a Function which belongs to a generated sort. |
| Equality.java | Class | This class represents an equality symbol for a given sort.
The system will generate automatically for each sort exactly one
equality symbol. |
| ExactInstanceSymbol.java | Class | |
| ExpressionOperator.java | Class | |
| FormulaSV.java | Class | |
| Function.java | Class | |
| IfExThenElse.java | Class | This implements an ifEx (x1, x2, ...) (phi) (t1) (t2) operator.
The meaning of this expression is given by
(ifEx (x1, x2, ...) (phi) (t1) (t2)) equiv (ifEx (x1) (ex x2. |
| IfThenElse.java | Class | |
| InstanceofSymbol.java | Class | |
| IProgramVariable.java | Interface | |
| IUpdateOperator.java | Interface | |
| Junctor.java | Class | |
| ListSV.java | Class | |
| Location.java | Interface | Operators implementing this interface may stand for
locations as well. |
| LocationVariable.java | Class | This class represents all kind of local and instance variables. |
| LogicVariable.java | Class | |
| MetaOperator.java | Interface | This is the interface for MetaOperators, which are used to do complex term
transformation when applying a taclet. |
| Metavariable.java | Class | |
| Modality.java | Class | this class is used to represent a dynamic logic modality like
diamond and box (but also extensions of DL like
preserves and throughout are possible in the future). |
| ModalOperatorSV.java | Class | |
| NameSV.java | Class | |
| NonRigid.java | Interface | |
| NonRigidFunction.java | Class | Non-rigid function or predicate symbols are realised as instances
of this class. |
| NonRigidFunctionLocation.java | Class | |
| NonRigidHeapDependentFunction.java | Class | Instances of this classes represent non-rigid functions, which dependent only on the
state of the heap and not of any local variables. |
| NRFunctionWithExplicitDependencies.java | Class | Non Rigid Fucntion with explicit dependencies. |
| Op.java | Class | This class contains logical connectives, most of them derive
from this class. |
| Operator.java | Interface | All symbols acting as members of a term e.g. |
| OperatorSV.java | Class | Creates an operator schemavariable that matches a given set of operators. |
| ParsableVariable.java | Interface | |
| ProgramConstant.java | Class | This class represents currently only static final fields initialised with
a compile time constant. |
| ProgramMethod.java | Class | The program method represents a concrete method in the logic.
In case of an instance method the first argument represents the
object on which the method is invoked. |
| ProgramSV.java | Class | |
| ProgramVariable.java | Class | |
| QuantifiableVariable.java | Interface | |
| Quantifier.java | Class | |
| QuanUpdateOperator.java | Class |
Operator for simultaneous, guarded and quantified updates. |
| RigidFunction.java | Class | |
| SchemaVariable.java | Interface | |
| SchemaVariableAdapter.java | Class | This class represents the root of a schema variable hierarchy to be
express termstructures that match on logical terms. |
| SchemaVariableFactory.java | Class | |
| ShadowArrayOp.java | Class | |
| ShadowAttributeOp.java | Class | |
| ShadowedOperator.java | Interface | |
| SkolemTermSV.java | Class | |
| SortDependingFunction.java | Class | A sort depending function is a function symbol. |
| SortDependingSymbol.java | Interface | Interface for a class (function, predicate) from which instances
exist for every sort (e.g. |
| SortedSchemaVariable.java | Class | This class represents the root of a schema variable hierarchy to be express
termstructures that match on logical terms. |
| SubstOp.java | Class | Standard first-order substitution operator, resolving clashes but not
preventing (usually unsound) substitution of non-rigid terms across modal
operators. |
| SVSubstitute.java | Interface | JavaCardDL syntactical elements implement this interface if they can
occur as instantiations of schema variabe. |
| TermSV.java | Class | |
| TermSymbol.java | Class | The abstract class term symbol implements common features of several
symbols occuring as part of a term (formula). |
| VariableSV.java | Class | |
| WarySubstOp.java | Class | |