This variable condition can be used to check whether an update can be performed on a formula or term. That is the case if the top-level operator is rigid and of arity greater than 0.
\applyUpdateOnRigid(VARIABLE, VARIABLE, VARIABLE)
This variable condition can be used to check whether an assignment expression occurs as a subexpression of a schemavariable instantiation,
\containsAssignment(VARIABLE)\not\containsAssignment(VARIABLE)
\different(VARIABLE, VARIABLE)
This variable condition checks if given two terms s, t both terms have a different unique symbol as top level operator
\differentFields(VARIABLE, VARIABLE)
\dropEffectlessElementaries(VARIABLE, VARIABLE, VARIABLE)
\dropEffectlessStores(VARIABLE, VARIABLE, VARIABLE, VARIABLE, VARIABLE)
\equalUnique(VARIABLE, VARIABLE, VARIABLE)
Variable condition that enforces a given generic sort to be instantiated with the type of a field constant. The condition can only be fulfilled if the given field term is constant of which the referred type is known.
\fieldType(VARIABLE, SORT)
ensures that the given instantiation for the schema variable denotes a final field
\final(VARIABLE)\not\final(VARIABLE)
\freeLabelIn(VARIABLE, VARIABLE)\not\freeLabelIn(VARIABLE, VARIABLE)
Extracts the free loop invariants for the given loop term. Free invariants are only assumed, but not proven (like an axiom).
\getFreeInvariant(VARIABLE, VARIABLE, VARIABLE)
Extracts the loop invariants for a loop term (for all applicable heap contexts).
\getInvariant(VARIABLE, VARIABLE, VARIABLE)
Checks whether a loop has an invariant (either normal or "free").
\hasInvariant(VARIABLE, VARIABLE)
This variable condition checks if an instantiation for term labels contains a specific term label.
\hasLabel(VARIABLE, STRING)\not\hasLabel(VARIABLE, STRING)
This variable condition checks if an instantiation for a formula has sub formulas which are formulas. It returns false for an arity equal to zero or no sub formulas. This is needed to simplify distinguishing between different well-definedness operators in taclets, since the difference exists only for formulas.
\hasSubFormulas(VARIABLE)\not\hasSubFormulas(VARIABLE)
This variable condition checks if a given type denotes an abstract class or interface type.
\isAbstractOrInterface(tr TYPE_RESOLVER)\not\isAbstractOrInterface(tr TYPE_RESOLVER)
This variable condition checks if an instantiation is an array.
\isArray(VARIABLE)\not\isArray(VARIABLE)
\isArrayLength(VARIABLE)\not\isArrayLength(VARIABLE)
This variable condition checks if an instantiation is a constant formula or term, i.e. its arity is equal to zero.
\isConstant(VARIABLE)\not\isConstant(VARIABLE)
ensures that the given instantiation for the schemavariable denotes a constant of an enum type.
\isEnumConst(VARIABLE)
This variable condition checks if a given type denotes a final type. Final types are either primitive types or classes that are declared final or arrays of final types.
\isFinal(tr TYPE_RESOLVER)\not\isFinal(tr TYPE_RESOLVER)
This variable condition checks if a context is affected by the strictfp modifier
\isInStrictFp()\not\isInStrictFp()
Ensures the given ProgramElement denotes a local variable
\isLocalVariable(VARIABLE)\not\isLocalVariable(VARIABLE)
This variable condition checks if the instantiation of a schemavariable (of type Field) refers to a Java field declared as "model". The negated condition is true if the instantiation refers to an instance or static or ghost field.
\isModelField(VARIABLE)\not\isModelField(VARIABLE)
\isObserver(VARIABLE, VARIABLE)
This variable condition checks if the instantiation of a schemavariable (of type Field) refers to
a Java field declared as "static".
The negated condition is true if the instantiation refers to an instance (non-static) field.
Inspired by FieldTypeToSortCondition.
\isStaticField(VARIABLE)\not\isStaticField(VARIABLE)
This variable condition checks if a given type denotes an abstract class or interface type.
\isThisReference(var VARIABLE)\not\isThisReference(var VARIABLE)
ensures that the given instantiation for the schemavariable denotes a method whose body may be expanded. For determining the method the callee and the arguments of the method are needed as arguments.
A method may be inlinded if:
\mayExpandMethod(VARIABLE, VARIABLE)\not\mayExpandMethod(VARIABLE, VARIABLE)\mayExpandMethod(VARIABLE, VARIABLE, VARIABLE)\not\mayExpandMethod(VARIABLE, VARIABLE, VARIABLE)
\metaDisjoint(VARIABLE, VARIABLE)
This variable condition ensures that no other label of the same name exists in the context program or one of the schemavariable instantiations.
\newLabel(VARIABLE)
For the loop scope rule, if a local program variable that may be altered by the loop body appears
in the frame condition,
it is necessary to use the value before the loop first executes in the frame condition.
To achieve this, this condition generates (1) the "before" version of each variable that may be
written to by the loop
MiscTools#getLocalOuts(ProgramElement, Services); (2) an update storing the value of each
such PV in its "before" version,
i.e., {...||i_before := i||...}; (3) the reverse of the update, to be applied to the
frame condition, i.e.,
{...||i := i_before||...}.
\newLocalVars(VARIABLE, VARIABLE, VARIABLE, VARIABLE)
This variable condition checks if a type is an enum type.
\reference(VARIABLE, VARIABLE, VARIABLE)\not\reference(VARIABLE, VARIABLE, VARIABLE)
A variable condition that is satisfied if the two arguments are
de.uka.ilkd.key.rule.metaconstruct.ObserverEqualityMetaConstruct only
support observers with a single heap argument, that should be generalised.
\sameObserver(schema1 VARIABLE, schema2 VARIABLE)Create a new condition * `schema1` @param schema1 first argument, must be schema variable * `schema2` @param schema2 2nd argument, must be schema variable
\sameObserver(schema1 VARIABLE, schema2 VARIABLE)Create a new condition * `schema1` @param schema1 first argument, must be schema variable * `schema2` @param schema2 2nd argument, must be schema variable
\simplifyIfThenElseUpdate(VARIABLE, VARIABLE, VARIABLE, VARIABLE, VARIABLE)\simplifyIfThenElseUpdate(VARIABLE, VARIABLE, VARIABLE, VARIABLE, VARIABLE)
ensures that the given instantiation for the schemavariable denotes a static field
\static(VARIABLE)\not\static(VARIABLE)
ensures that the given instantiation for the schemavariable denotes a static method. For determining the method the callee and the arguments of the method are needed as arguments.
\staticMethodReference(VARIABLE, VARIABLE, VARIABLE)\not\staticMethodReference(VARIABLE, VARIABLE, VARIABLE)
Stores the given Statement, after substitution of SchemaVariables, into the given
ProgramSV for later use in other conditions and transformers. The arguments are a
ProgramSV and a JTerm, where the JTerm must contain a JavaBlock
with a StatementBlock containing \modality{#allmodal}{ while (#e) #body }\endmodality(post)); this statement is then
stored (in the example the while statement).
\storeStmtIn(VARIABLE, TERM)
This variable condition checks if an instantiation for a formula has sub formulas which are formulas. It returns false for an arity equal to zero or no sub formulas. This is needed to simplify distinguishing between different well-definedness operators in taclets, since the difference exists only for formulas.
\subFormulas(VARIABLE)\not\subFormulas(VARIABLE)