public class ObserverEqualityMetaConstruct extends AbstractTermTransformer
It takes two arguments of any sort and the result is a formula.
This construct is asymmetric. The second argument is the call with the base heap, i.e., the one with fewer created objects. The first argument is the one with the larger heap, i.e., after modification and with potentially more created objects.
The construct implements the condition (9.10) in Sect. 9.4.4 in the new KeY book.
It is probably less efficient than UseDependencyContractRule
, however
it is more generally applicable. It mitigates the problem, that in
interactive proving the above builtin rule is often not available if desired.
UseDependencyContractRule
,
SameObserverCondition
Modifier and Type | Field and Description |
---|---|
static java.lang.String |
NAME
The unique identifier name.
|
ADD_CAST, ARRAY_BASE_INSTANCE_OF, CONSTANT_VALUE, CREATE_BEFORE_LOOP_UPDATE, CREATE_FRAME_COND, CREATE_HEAP_ANON_UPDATE, CREATE_LOCAL_ANON_UPDATE, CREATE_WELLFORMED_COND, DIVIDE_LCR_MONOMIALS, DIVIDE_MONOMIALS, ENUM_CONSTANT_VALUE, EXPAND_QUERIES, INTRODUCE_ATPRE_DEFINITIONS, MEMBER_PV_TO_FIELD, META_ADD, META_AND, META_DIV, META_EQ, META_GEQ, META_GREATER, META_LEQ, META_LESS, META_MUL, META_OR, META_POW, META_SHIFTLEFT, META_SHIFTRIGHT, META_SUB, META_XOR, METASORT, NAME_TO_META_OP, OBSERVER_EQUALITY
Constructor and Description |
---|
ObserverEqualityMetaConstruct()
This constructor is probably only called from
AbstractTermTransformer . |
Modifier and Type | Method and Description |
---|---|
int |
arity()
the arity of this operator
|
boolean |
bindVarsAt(int n)
Tells whether the operator binds variables at the n-th subterm.
|
boolean |
isRigid()
Tells whether the operator is rigid.
|
Name |
name()
returns the name of this element
|
java.lang.String |
toString() |
Term |
transform(Term term,
SVInstantiations svInst,
Services services)
Given two terms termExt and termBase, produce a formula which implies
equality of the two terms.
|
void |
validTopLevelException(Term term)
Checks whether the top level structure of the given @link Term
is syntactically valid, given the assumption that the top level
operator of the term is the same as this Operator.
|
protected ImmutableArray<java.lang.Boolean> |
whereToBind() |
convertToDecimalString, name2metaop
additionalValidTopLevel, argSort, argSorts, sort, sort
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
argSort, argSorts, sort
arity, bindVarsAt, isRigid, sort, validTopLevel, validTopLevelException
public static final java.lang.String NAME
public ObserverEqualityMetaConstruct()
AbstractTermTransformer
.public Term transform(Term term, SVInstantiations svInst, Services services)
It is easy to write a taclet that violates this. The method should
therefore been written defensively. Since the method must not throw
declared exceptions, IllegalArgumentException
s are used.
term
- A term of the type #ObserverEquality(t1, t2)
, not
null.svInst
- instantiations of schema variables, not usedservices
- non-null Services
java.lang.IllegalArgumentException
- if the term argument is not as expectedprotected final ImmutableArray<java.lang.Boolean> whereToBind()
public final Name name()
Named
public final int arity()
Operator
public final boolean bindVarsAt(int n)
Operator
bindVarsAt
in interface Operator
public final boolean isRigid()
Operator
public void validTopLevelException(Term term) throws TermCreationException
Operator
validTopLevelException
in interface Operator
TermCreationException
- if a construction error was recognisepublic java.lang.String toString()
toString
in class java.lang.Object
Copyright © 2003-2019 The KeY-Project.