| Interface | Description |
|---|---|
| IObserverFunction | |
| IProgramMethod | |
| IProgramVariable | |
| Operator |
All symbols acting as members of a term e.g. logical operators, predicates,
functions, variables etc. have to implement this interface.
|
| ParsableVariable |
This interface represents the variables that can be recognized
by one of the parsers.
|
| QuantifiableVariable |
This interface represents the variables that can be bound
(by quantifiers or other binding operators).
|
| SchemaVariable |
This interface represents the root of a schema variable hierarchy to be
express termstructures that match on logical terms.
|
| SortedOperator |
Operator with well-defined argument and result sorts.
|
| SVSubstitute |
JavaCardDL syntactical elements implement this interface if they can
occur as instantiations of schema variables.
|
| TermTransformer |
TermTransformer perform complex term transformation which cannot be
(efficiently or at all) described by taclets.
|
| UpdateableOperator |
Operators implementing this interface may stand for
locations as well.
|
| Class | Description |
|---|---|
| AbstractOperator |
Abstract operator class offering some common functionality.
|
| AbstractSortedOperator |
Abstract sorted operator class offering some common functionality.
|
| AbstractSV |
Abstract base class for schema variables.
|
| AbstractTermTransformer |
Abstract class factoring out commonalities of typical term transformer implementations.
|
| ElementaryUpdate |
Class of operators for elementary updates, i.e., updates of the form
"x := t".
|
| Equality |
This class defines the equality operator "=".
|
| FormulaSV |
A schema variable that is used as placeholder for formulas.
|
| Function |
Objects of this class represent function and predicate symbols.
|
| IfExThenElse |
This singleton class implements a conditional operator
"\ifEx iv; (phi) \then (t1) \else (t2)", where iv is an integer logic
variable, phi is a formula, and where t1 and t2 are terms with the same sort.
|
| IfThenElse |
This singleton class implements a general conditional operator
\if (phi) \then (t1) \else (t2).
|
| Junctor |
Class of junctor operators, i.e., operators connecting
a given number of formula to create another formula.
|
| LocationVariable |
This class represents proper program variables, which are not program
constants.
|
| LogicVariable |
The objects of this class represent logical variables,
used e.g. for quantification.
|
| Modality |
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 |
Schema variable matching modal operators.
|
| ObserverFunction |
Objects of this class represent "observer" function or predicate symbols.
|
| ProgramConstant |
This class represents currently only static final fields initialised with
a compile time constant.
|
| ProgramMethod |
The program method represents a (pure) method in the logic.
|
| ProgramSV |
Objects of this class are schema variables matching program constructs within
modal operators.
|
| ProgramVariable |
The objects of this class represent program variables and program
constants (resulting from static final declarations in programs; TODO: it is
weird that constants are a special case of variables).
|
| Quantifier |
The two objects of this class represent the universal and the existential
quantifier, respectively.
|
| SchemaVariableFactory |
A factory class for different Schema Variables
|
| SkolemTermSV |
Schema variable that is instantiated with fresh Skolem constants.
|
| SortDependingFunction |
The objects of this class represent families of function symbols, where
each family contains an instantiation of a template symbol for a particular
sort.
|
| SortDependingFunction.SortDependingFunctionTemplate | |
| SubstOp |
Standard first-order substitution operator, resolving clashes but not
preventing (usually unsound) substitution of non-rigid terms across modal
operators.
|
| TermLabelSV |
A schema variable which matches term labels
|
| TermSV |
A schema variable that is used as placeholder for terms.
|
| Transformer |
Functions with a restricted/special rule set only applicable for the top level
of the term transformer and not directly for its arguments, prohibiting any rule
applications to sub arguments as well as applications from outside such as update applications.
|
| UpdateApplication |
Singleton class defining a binary operator {u}t that applies updates u to
terms, formulas, or other updates t.
|
| UpdateJunctor |
Class of update junctor operators, i.e., operators connecting
a given number of updates to create another update.
|
| UpdateSV |
A schema variable that is used as placeholder for updates.
|
| VariableSV |
Schema variable that is instantiated with logical variables.
|
| WarySubstOp |
Terms. Operators may be Quantifiers or SubstOps that bind variables for
subterms, but also Modalitys, or
de.uka.ilkd.key.logic.op.QuanUpdateOperators. Many of the operators
are constantly defined in de.uka.ilkd.key.logic.op.Ops.
An operator can be a de.uka.ilkd.key.logic.op.TermSymbols,
such as a Function or a
variable. There are several kind of variables: LogicVariables (variables that must be
bound but do not occur in programs), ProgramVariables (allowed both in
programs and in logic, but not boundable), de.uka.ilkd.key.logic.op.Metavariables, and SchemaVariables for Taclets.
Last modified: Mon Apr 18 09:42:36 MEST 2005