Package | Description |
---|---|
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. |
Modifier and Type | Class and Description |
---|---|
class |
AbstractTermTransformer
Abstract class factoring out commonalities of typical term transformer implementations.
|
Modifier and Type | Method and Description |
---|---|
static TermTransformer |
AbstractTermTransformer.name2metaop(java.lang.String s) |
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 |
Copyright © 2003-2019 The KeY-Project.