Package | Description |
---|---|
de.uka.ilkd.key.logic |
provides a representation for the term and sequent
structure.
|
de.uka.ilkd.key.logic.op |
contains the operators of
Term s. |
de.uka.ilkd.key.rule.metaconstruct |
contains classes representing the meta constructs of
Taclet s. |
de.uka.ilkd.key.rule.metaconstruct.arith |
contains classes representing the special meta constructs of
Taclet s performing arithmetic operations. |
de.uka.ilkd.key.strategy.quantifierHeuristics | |
de.uka.ilkd.key.util |
This package is a grab bag of miscellaneous useful code fragments.
|
Modifier and Type | Interface and Description |
---|---|
interface |
Term
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
Modifier and Type | Class and Description |
---|---|
class |
TermImpl
The currently only class implementing the Term interface.
|
Modifier and Type | Class and Description |
---|---|
class |
AbstractSortedOperator
Abstract sorted operator class offering some common functionality.
|
class |
AbstractSV
Abstract base class for schema variables.
|
class |
AbstractTermTransformer
Abstract class factoring out commonalities of typical term transformer implementations.
|
class |
ElementaryUpdate
Class of operators for elementary updates, i.e., updates of the form
"x := t".
|
class |
Equality
This class defines the equality operator "=".
|
class |
FormulaSV
A schema variable that is used as placeholder for formulas.
|
class |
Function
Objects of this class represent function and predicate symbols.
|
class |
Junctor
Class of junctor operators, i.e., operators connecting
a given number of formula to create another formula.
|
class |
LocationVariable
This class represents proper program variables, which are not program
constants.
|
class |
LogicVariable
The objects of this class represent logical variables,
used e.g.
|
class |
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 |
ModalOperatorSV
Schema variable matching modal operators.
|
class |
ObserverFunction
Objects of this class represent "observer" function or predicate symbols.
|
class |
ProgramConstant
This class represents currently only static final fields initialised with
a compile time constant.
|
class |
ProgramMethod
The program method represents a (pure) method in the logic.
|
class |
ProgramSV
Objects of this class are schema variables matching program constructs within
modal operators.
|
class |
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 |
Quantifier
The two objects of this class represent the universal and the existential
quantifier, respectively.
|
class |
SkolemTermSV
Schema variable that is instantiated with fresh Skolem constants.
|
class |
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 |
TermLabelSV
A schema variable which matches term labels
|
class |
TermSV
A schema variable that is used as placeholder for terms.
|
class |
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.
|
class |
UpdateJunctor
Class of update junctor operators, i.e., operators connecting
a given number of updates to create another update.
|
class |
UpdateSV
A schema variable that is used as placeholder for updates.
|
class |
VariableSV
Schema variable that is instantiated with logical variables.
|
Modifier and Type | Class and Description |
---|---|
class |
AddCast |
class |
ArrayBaseInstanceOf
Creates an Type::instance(..) term for the component type of the
array.
|
class |
ConstantValue
Replace a program variable that is a compile-time constant with the
value of the initializer
|
class |
CreateBeforeLoopUpdate
Initializes the "before loop" update needed for the assignable clause.
|
class |
CreateFrameCond
Creates the frame condition (aka "assignable clause") for the given loop.
|
class |
CreateHeapAnonUpdate
Creates the anonymizing update for the heap.
|
class |
CreateLocalAnonUpdate
Expects a loop body and creates the anonymizing update
out_1:=anon_1||...||out_n:=anon_n , where anon_1, ..., anon_n are
the written variables in the loop body visible to the outside. |
class |
CreateWellformedCond
Creates the wellformedness condition for the given anonymizing heap terms if
they apply for the current profile and modality type.
|
class |
EnumConstantValue
resolve a program variable to an integer literal.
|
class |
ExpandQueriesMetaConstruct
Uses the class
QueryExpand in order to insert query expansions in the term that the
meta construct is applied on. |
class |
IntroAtPreDefsOp |
class |
MemberPVToField |
class |
ObserverEqualityMetaConstruct
This meta contruct allows one to prove equality (equivalence) of two
observer terms if they belong to the same observer function symbol.
|
Modifier and Type | Class and Description |
---|---|
class |
DivideLCRMonomials
Metaoperator for computing the result of dividing one monomial by another
|
class |
DivideMonomials
Metaoperator for computing the result of dividing one monomial by another
|
class |
MetaAdd |
class |
MetaArithBitMaskOp |
class |
MetaBinaryAnd |
class |
MetaBinaryOr |
class |
MetaBinaryXOr |
class |
MetaDiv |
class |
MetaEqual |
class |
MetaGeq |
class |
MetaGreater |
class |
MetaLeq |
class |
MetaLess |
class |
MetaMul |
class |
MetaPow
Computes the pow function for literals.
|
class |
MetaShift |
class |
MetaShiftLeft |
class |
MetaShiftRight |
class |
MetaSub |
Modifier and Type | Class and Description |
---|---|
class |
Metavariable
Deprecated.
|
Modifier and Type | Method and Description |
---|---|
static void |
Assert.assertEqualSort(Sorted t1,
Sorted t2)
Check whether two terms (or other sorted objects) are of the same sort.
|
static void |
Assert.assertSubSort(Sorted t1,
Sorted t2)
Check whether the sort of t1 is a subsort of the sort of t2.
|
Copyright © 2003-2019 The KeY-Project.