Package | Description |
---|---|
de.uka.ilkd.key.nparser.varexp | |
de.uka.ilkd.key.pp |
This package contains pretty-printing functionality used by the GUI and for
saving proofs.
|
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.rule.conditions | |
de.uka.ilkd.key.rule.tacletbuilder |
Modifier and Type | Method and Description |
---|---|
VariableCondition |
ConstructorBasedBuilder.build(java.lang.Object[] arguments,
java.util.List<java.lang.String> parameters,
boolean negated) |
VariableCondition |
ConditionBuilder.build(java.lang.Object[] arguments,
java.util.List<java.lang.String> parameters,
boolean negated)
Should construct a variable condition for the given arguments and parameters.
|
Constructor and Description |
---|
ConstructorBasedBuilder(java.lang.String name,
boolean negationSupported,
java.lang.Class<? extends VariableCondition> clazz,
ArgumentType... types) |
ConstructorBasedBuilder(java.lang.String name,
java.lang.Class<? extends VariableCondition> clazz,
ArgumentType... types) |
Modifier and Type | Method and Description |
---|---|
protected void |
LogicPrinter.printVariableCondition(VariableCondition sv) |
Modifier and Type | Class and Description |
---|---|
class |
VariableConditionAdapter
The variable condition adapter can be used by variable conditions
which can either fail or be successful, but which do not create a
constraint.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<VariableCondition> |
Taclet.getVariableConditions() |
ImmutableList<VariableCondition> |
TacletApplPart.getVariableConditions()
returns the list of additional generic conditions on
instantiations of schema variables.
|
Constructor and Description |
---|
TacletApplPart(Sequent ifseq,
ImmutableList<NewVarcond> varsNew,
ImmutableList<NotFreeIn> varsNotFreeIn,
ImmutableList<NewDependingOn> varsNewDependingOn,
ImmutableList<VariableCondition> variableConditions)
constructs a new TacletApplPart object with the given Sequent,
a list of variables that are new, a list of variable pairs that
represent the NotFreeIn relation and a list of additional
generic variable conditions.
|
Modifier and Type | Class and Description |
---|---|
class |
AbstractOrInterfaceType
This variable condition checks if a given type denotes an abstract class or
interface type.
|
class |
AlternativeVariableCondition
disjoin two variable conditions
|
class |
ApplyUpdateOnRigidCondition |
class |
ArrayComponentTypeCondition
This variable condition checks if an array component is of reference type
|
class |
ArrayLengthCondition |
class |
ArrayTypeCondition
This variable condition checks if an instantiation is an array.
|
class |
ConstantCondition
This variable condition checks if an instantiation is a constant formula or term,
i.e.
|
class |
ContainsAssignmentCondition
This variable condition can be used to check whether an assignment expression
occurs as a subexpression of a schemavariable instantiation,
|
class |
DifferentFields
This variable condition checks if given two terms s, t both terms have a different
unique symbol as top level operator
|
class |
DifferentInstantiationCondition |
class |
DropEffectlessElementariesCondition |
class |
DropEffectlessStoresCondition |
class |
EnumConstantCondition
ensures that the given instantiation for the schemavariable denotes a
constant of an enum type.
|
class |
EnumTypeCondition
This variable condition checks if a type is an enum type.
|
class |
EqualUniqueCondition |
class |
FieldTypeToSortCondition
Variable condition that enforces a given generic sort to be instantiated with
the type of a field constant.
|
class |
FinalReferenceCondition
ensures that the given instantiation for the schema variable denotes a
final field
|
class |
FreeLabelInVariableCondition |
class |
HasLoopInvariantCondition
Checks whether a loop has an invariant (either normal or "free").
|
class |
IsLabeledCondition
Checks whether the given statement is labeled, i.e., actual a
LabeledStatement.
|
class |
IsThisReference
This variable condition checks if a given type denotes an abstract class or
interface type.
|
class |
JavaTypeToSortCondition
Variable condition that enforces a given generic sort to be instantiated with
the sort of a program expression a schema variable is instantiated with
|
class |
LocalVariableCondition
Ensures the given ProgramElement denotes a local variable
|
class |
LoopFreeInvariantCondition
Extracts the free loop invariants for the given loop term.
|
class |
LoopInvariantCondition
Extracts the loop invariants for a loop term (for all applicable heap
contexts).
|
class |
LoopVariantCondition
Extracts the variant for a loop term.
|
class |
MayExpandMethodCondition
ensures that the given instantiation for the schemavariable denotes
a method whose body may be expanded.
|
class |
MetaDisjointCondition |
class |
NewJumpLabelCondition
This variable condition ensures that no other label of the
same name exists in the context program or one of the schemavariable
instantiations.
|
class |
ObserverCondition |
class |
SameObserverCondition
A variable condition that is satisfied if the two arguments are
schema variables,
their instantiations are terms of observer functions,
with the same function,
which as exactly one heap argument
and has got a dependency contract
,
|
class |
SimplifyIfThenElseUpdateCondition |
class |
StaticFieldCondition
This variable condition checks if the instantiation of a schemavariable (of
type Field) refers to a Java field declared as "static".
|
class |
StaticMethodCondition
ensures that the given instantiation for the schemavariable denotes
a static method.
|
class |
StaticReferenceCondition
ensures that the given instantiation for the schemavariable denotes a
static field
|
class |
StoreStmtInCondition
Stores the given
Statement , after substitution of
SchemaVariable s, into the given ProgramSV for later use in
other conditions and transformers. |
class |
StoreTermInCondition
Stores the given
Term , after substitution of SchemaVariable s,
into the given SchemaVariable for later use in other conditions and
transformers. |
class |
SubFormulaCondition
This variable condition checks if an instantiation for a formula has sub formulas
which are formulas.
|
class |
TermLabelCondition
This variable condition checks if an instantiation for term labels contains a specific
term label.
|
class |
TypeComparisonCondition
General varcond for checking relationships between types of schema variables.
|
class |
TypeCondition
This variable condition checks if a schemavariable is instantiated
with a reference or primitive type
|
Modifier and Type | Field and Description |
---|---|
protected ImmutableList<VariableCondition> |
TacletBuilder.variableConditions
List of additional generic conditions on the instantiations of
schema variables.
|
Modifier and Type | Method and Description |
---|---|
void |
TacletBuilder.addVariableCondition(VariableCondition vc)
Add an additional generic condition on the instantiation of
schema variables.
|
Copyright © 2003-2019 The KeY-Project.