Class and Description |
---|
LocationVariable
This class represents proper program variables, which are not program
constants.
|
Class and Description |
---|
IProgramVariable |
Class and Description |
---|
Function
Objects of this class represent function and predicate symbols.
|
IProgramVariable |
QuantifiableVariable
This interface represents the variables that can be bound
(by quantifiers or other binding operators).
|
Class and Description |
---|
IObserverFunction |
LocationVariable
This class represents proper program variables, which are not program
constants.
|
Class and Description |
---|
LocationVariable
This class represents proper program variables, which are not program
constants.
|
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).
|
Class and Description |
---|
IProgramMethod |
LocationVariable
This class represents proper program variables, which are not program
constants.
|
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).
|
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).
|
Class and Description |
---|
IProgramMethod |
Class and Description |
---|
SchemaVariable
This interface represents the root of a schema variable hierarchy to be
express termstructures that match on logical terms.
|
Class and Description |
---|
IObserverFunction |
IProgramMethod |
IProgramVariable |
Operator
All symbols acting as members of a term e.g.
|
ProgramMethod
The program method represents a (pure) method in the logic.
|
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).
|
SchemaVariable
This interface represents the root of a schema variable hierarchy to be
express termstructures that match on logical terms.
|
SVSubstitute
JavaCardDL syntactical elements implement this interface if they can
occur as instantiations of schema variables.
|
Class and Description |
---|
IProgramVariable |
Class and Description |
---|
IProgramVariable |
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).
|
SVSubstitute
JavaCardDL syntactical elements implement this interface if they can
occur as instantiations of schema variables.
|
Class and Description |
---|
SVSubstitute
JavaCardDL syntactical elements implement this interface if they can
occur as instantiations of schema variables.
|
Class and Description |
---|
SVSubstitute
JavaCardDL syntactical elements implement this interface if they can
occur as instantiations of schema variables.
|
Class and Description |
---|
SVSubstitute
JavaCardDL syntactical elements implement this interface if they can
occur as instantiations of schema variables.
|
Class and Description |
---|
Function
Objects of this class represent function and predicate symbols.
|
LocationVariable
This class represents proper program variables, which are not program
constants.
|
SVSubstitute
JavaCardDL syntactical elements implement this interface if they can
occur as instantiations of schema variables.
|
Class and Description |
---|
SVSubstitute
JavaCardDL syntactical elements implement this interface if they can
occur as instantiations of schema variables.
|
Class and Description |
---|
ProgramSV
Objects of this class are schema variables matching program constructs within
modal operators.
|
SchemaVariable
This interface represents the root of a schema variable hierarchy to be
express termstructures that match on logical terms.
|
Class and Description |
---|
IProgramMethod |
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).
|
SchemaVariable
This interface represents the root of a schema variable hierarchy to be
express termstructures that match on logical terms.
|
SVSubstitute
JavaCardDL syntactical elements implement this interface if they can
occur as instantiations of schema variables.
|
Class and Description |
---|
IProgramMethod |
IProgramVariable |
LocationVariable
This class represents proper program variables, which are not program
constants.
|
SVSubstitute
JavaCardDL syntactical elements implement this interface if they can
occur as instantiations of schema variables.
|
Class and Description |
---|
IProgramMethod |
IProgramVariable |
LocationVariable
This class represents proper program variables, which are not program
constants.
|
ProgramConstant
This class represents currently only static final fields initialised with
a compile time constant.
|
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).
|
SchemaVariable
This interface represents the root of a schema variable hierarchy to be
express termstructures that match on logical terms.
|
Class and Description |
---|
Function
Objects of this class represent function and predicate symbols.
|
LocationVariable
This class represents proper program variables, which are not program
constants.
|
Operator
All symbols acting as members of a term e.g.
|
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.
|
Class and Description |
---|
Function
Objects of this class represent function and predicate symbols.
|
IObserverFunction |
IProgramMethod |
IProgramVariable |
LocationVariable
This class represents proper program variables, which are not program
constants.
|
LogicVariable
The objects of this class represent logical variables,
used e.g.
|
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).
|
Operator
All symbols acting as members of a term e.g.
|
ParsableVariable
This interface represents the variables that can be recognized
by one of the parsers.
|
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).
|
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.
|
SubstOp
Standard first-order substitution operator, resolving clashes but not
preventing (usually unsound) substitution of non-rigid terms across modal
operators.
|
SVSubstitute
JavaCardDL syntactical elements implement this interface if they can
occur as instantiations of schema variables.
|
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.
|
UpdateableOperator
Operators implementing this interface may stand for
locations as well.
|
Class and Description |
---|
Operator
All symbols acting as members of a term e.g.
|
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).
|
QuantifiableVariable
This interface represents the variables that can be bound
(by quantifiers or other binding operators).
|
Class and Description |
---|
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).
|
IObserverFunction |
IProgramMethod |
IProgramVariable |
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.
|
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.
|
Operator
All symbols acting as members of a term e.g.
|
ParsableVariable
This interface represents the variables that can be recognized
by one of the parsers.
|
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).
|
QuantifiableVariable
This interface represents the variables that can be bound
(by quantifiers or other binding operators).
|
Quantifier
The two objects of this class represent the universal and the existential
quantifier, respectively.
|
SchemaVariable
This interface represents the root of a schema variable hierarchy to be
express termstructures that match on logical terms.
|
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.
|
SortedOperator
Operator with well-defined argument and result sorts.
|
SubstOp
Standard first-order substitution operator, resolving clashes but not
preventing (usually unsound) substitution of non-rigid terms across modal
operators.
|
SVSubstitute
JavaCardDL syntactical elements implement this interface if they can
occur as instantiations of schema variables.
|
TermLabelSV
A schema variable which matches term labels
|
TermSV
A schema variable that is used as placeholder for terms.
|
TermTransformer
TermTransformer perform complex term transformation which cannot be
(efficiently or at all) described by taclets.
|
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.
|
UpdateableOperator
Operators implementing this interface may stand for
locations as well.
|
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.
|
Class and Description |
---|
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.
|
Class and Description |
---|
SchemaVariable
This interface represents the root of a schema variable hierarchy to be
express termstructures that match on logical terms.
|
Class and Description |
---|
Function
Objects of this class represent function and predicate symbols.
|
IProgramVariable |
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).
|
Operator
All symbols acting as members of a term e.g.
|
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.
|
Class and Description |
---|
Function
Objects of this class represent function and predicate symbols.
|
IProgramVariable |
QuantifiableVariable
This interface represents the variables that can be bound
(by quantifiers or other binding operators).
|
Class and Description |
---|
Function
Objects of this class represent function and predicate symbols.
|
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).
|
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.
|
Class and Description |
---|
Function
Objects of this class represent function and predicate symbols.
|
IObserverFunction |
IProgramVariable |
LocationVariable
This class represents proper program variables, which are not program
constants.
|
Operator
All symbols acting as members of a term e.g.
|
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).
|
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.
|
SVSubstitute
JavaCardDL syntactical elements implement this interface if they can
occur as instantiations of schema variables.
|
Class and Description |
---|
Function
Objects of this class represent function and predicate symbols.
|
IObserverFunction |
IProgramMethod |
IProgramVariable |
LocationVariable
This class represents proper program variables, which are not program
constants.
|
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).
|
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).
|
QuantifiableVariable
This interface represents the variables that can be bound
(by quantifiers or other binding operators).
|
Class and Description |
---|
Function
Objects of this class represent function and predicate symbols.
|
IProgramVariable |
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.
|
Class and Description |
---|
IObserverFunction |
IProgramMethod |
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).
|
Class and Description |
---|
IProgramMethod |
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).
|
Class and Description |
---|
Function
Objects of this class represent function and predicate symbols.
|
IObserverFunction |
IProgramMethod |
LocationVariable
This class represents proper program variables, which are not program
constants.
|
LogicVariable
The objects of this class represent logical variables,
used e.g.
|
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).
|
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).
|
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.
|
SVSubstitute
JavaCardDL syntactical elements implement this interface if they can
occur as instantiations of schema variables.
|
Class and Description |
---|
AbstractSortedOperator
Abstract sorted operator class offering some common functionality.
|
FormulaSV
A schema variable that is used as placeholder for formulas.
|
ParsableVariable
This interface represents the variables that can be recognized
by one of the parsers.
|
ProgramSV
Objects of this class are schema variables matching program constructs within
modal operators.
|
SchemaVariable
This interface represents the root of a schema variable hierarchy to be
express termstructures that match on logical terms.
|
SVSubstitute
JavaCardDL syntactical elements implement this interface if they can
occur as instantiations of schema variables.
|
TermLabelSV
A schema variable which matches term labels
|
TermSV
A schema variable that is used as placeholder for terms.
|
UpdateSV
A schema variable that is used as placeholder for updates.
|
Class and Description |
---|
SchemaVariable
This interface represents the root of a schema variable hierarchy to be
express termstructures that match on logical terms.
|
Class and Description |
---|
ModalOperatorSV
Schema variable matching modal operators.
|
Operator
All symbols acting as members of a term e.g.
|
SchemaVariable
This interface represents the root of a schema variable hierarchy to be
express termstructures that match on logical terms.
|
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.
|
SVSubstitute
JavaCardDL syntactical elements implement this interface if they can
occur as instantiations of schema variables.
|
Class and Description |
---|
Operator
All symbols acting as members of a term e.g.
|
QuantifiableVariable
This interface represents the variables that can be bound
(by quantifiers or other binding operators).
|
Class and Description |
---|
Operator
All symbols acting as members of a term e.g.
|
SchemaVariable
This interface represents the root of a schema variable hierarchy to be
express termstructures that match on logical terms.
|
SVSubstitute
JavaCardDL syntactical elements implement this interface if they can
occur as instantiations of schema variables.
|
Class and Description |
---|
SchemaVariable
This interface represents the root of a schema variable hierarchy to be
express termstructures that match on logical terms.
|
SVSubstitute
JavaCardDL syntactical elements implement this interface if they can
occur as instantiations of schema variables.
|
Class and Description |
---|
ElementaryUpdate
Class of operators for elementary updates, i.e., updates of the form
"x := t".
|
FormulaSV
A schema variable that is used as placeholder for formulas.
|
ModalOperatorSV
Schema variable matching modal operators.
|
Operator
All symbols acting as members of a term e.g.
|
ProgramSV
Objects of this class are schema variables matching program constructs within
modal operators.
|
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.
|
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.
|
TermSV
A schema variable that is used as placeholder for terms.
|
UpdateSV
A schema variable that is used as placeholder for updates.
|
VariableSV
Schema variable that is instantiated with logical variables.
|
Class and Description |
---|
LocationVariable
This class represents proper program variables, which are not program
constants.
|
Class and Description |
---|
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).
|
Class and Description |
---|
AbstractSortedOperator
Abstract sorted operator class offering some common functionality.
|
AbstractTermTransformer
Abstract class factoring out commonalities of typical term transformer implementations.
|
IProgramMethod |
LocationVariable
This class represents proper program variables, which are not program
constants.
|
Operator
All symbols acting as members of a term e.g.
|
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).
|
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.
|
Class and Description |
---|
AbstractSortedOperator
Abstract sorted operator class offering some common functionality.
|
AbstractTermTransformer
Abstract class factoring out commonalities of typical term transformer implementations.
|
Operator
All symbols acting as members of a term e.g.
|
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.
|
Class and Description |
---|
IObserverFunction |
LocationVariable
This class represents proper program variables, which are not program
constants.
|
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).
|
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.
|
Class and Description |
---|
Function
Objects of this class represent function and predicate symbols.
|
Operator
All symbols acting as members of a term e.g.
|
QuantifiableVariable
This interface represents the variables that can be bound
(by quantifiers or other binding operators).
|
Class and Description |
---|
Operator
All symbols acting as members of a term e.g.
|
SortedOperator
Operator with well-defined argument and result sorts.
|
Class and Description |
---|
Function
Objects of this class represent function and predicate symbols.
|
IObserverFunction |
IProgramMethod |
LocationVariable
This class represents proper program variables, which are not program
constants.
|
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).
|
ParsableVariable
This interface represents the variables that can be recognized
by one of the parsers.
|
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).
|
Class and Description |
---|
ParsableVariable
This interface represents the variables that can be recognized
by one of the parsers.
|
Class and Description |
---|
IProgramMethod |
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).
|
Class and Description |
---|
IProgramMethod |
LocationVariable
This class represents proper program variables, which are not program
constants.
|
ParsableVariable
This interface represents the variables that can be recognized
by one of the parsers.
|
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).
|
Class and Description |
---|
IObserverFunction |
LocationVariable
This class represents proper program variables, which are not program
constants.
|
LogicVariable
The objects of this class represent logical variables,
used e.g.
|
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).
|
QuantifiableVariable
This interface represents the variables that can be bound
(by quantifiers or other binding operators).
|
Class and Description |
---|
LogicVariable
The objects of this class represent logical variables,
used e.g.
|
ParsableVariable
This interface represents the variables that can be recognized
by one of the parsers.
|
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).
|
Class and Description |
---|
Operator
All symbols acting as members of a term e.g.
|
Class and Description |
---|
Operator
All symbols acting as members of a term e.g.
|
Class and Description |
---|
AbstractSortedOperator
Abstract sorted operator class offering some common functionality.
|
Operator
All symbols acting as members of a term e.g.
|
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).
|
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.
|
Class and Description |
---|
Operator
All symbols acting as members of a term e.g.
|
Class and Description |
---|
Operator
All symbols acting as members of a term e.g.
|
Class and Description |
---|
IProgramMethod |
IProgramVariable |
LocationVariable
This class represents proper program variables, which are not program
constants.
|
Operator
All symbols acting as members of a term e.g.
|
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).
|
Class and Description |
---|
IProgramMethod |
IProgramVariable |
Class and Description |
---|
IProgramMethod |
IProgramVariable |
LocationVariable
This class represents proper program variables, which are not program
constants.
|
Operator
All symbols acting as members of a term e.g.
|
Class and Description |
---|
IProgramVariable |
Class and Description |
---|
IProgramVariable |
Class and Description |
---|
IProgramMethod |
LocationVariable
This class represents proper program variables, which are not program
constants.
|
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).
|
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).
|
Class and Description |
---|
Function
Objects of this class represent function and predicate symbols.
|
Class and Description |
---|
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).
|
Class and Description |
---|
IProgramMethod |
LocationVariable
This class represents proper program variables, which are not program
constants.
|
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).
|
SVSubstitute
JavaCardDL syntactical elements implement this interface if they can
occur as instantiations of schema variables.
|
Class and Description |
---|
IProgramMethod |
IProgramVariable |
Operator
All symbols acting as members of a term e.g.
|
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).
|
Class and Description |
---|
LogicVariable
The objects of this class represent logical variables,
used e.g.
|
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.
|
Class and Description |
---|
Function
Objects of this class represent function and predicate symbols.
|
Operator
All symbols acting as members of a term e.g.
|
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.
|
Class and Description |
---|
IProgramMethod |
Class and Description |
---|
IObserverFunction |
IProgramMethod |
LocationVariable
This class represents proper program variables, which are not program
constants.
|
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).
|
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).
|
Class and Description |
---|
Function
Objects of this class represent function and predicate symbols.
|
LocationVariable
This class represents proper program variables, which are not program
constants.
|
LogicVariable
The objects of this class represent logical variables,
used e.g.
|
Copyright © 2003-2019 The KeY-Project.