public final class SameObserverCondition extends java.lang.Object implements VariableCondition
ObserverEqualityMetaConstruct
only support observers with a single heap argument, that should be
generalised.ObserverEqualityMetaConstruct
Constructor and Description |
---|
SameObserverCondition(ParsableVariable schema1,
ParsableVariable schema2)
Create a new condition
|
Modifier and Type | Method and Description |
---|---|
MatchConditions |
check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions mc,
Services services)
checks if the condition for a correct instantiation is fulfilled
|
java.lang.String |
toString() |
public SameObserverCondition(ParsableVariable schema1, ParsableVariable schema2)
schema1
- first argument, must be schema variableschema2
- 2nd argument, must be schema variablejava.lang.IllegalArgumentException
- if the args are not schema variables.public MatchConditions check(SchemaVariable var, SVSubstitute instCandidate, MatchConditions mc, Services services)
VariableCondition
check
in interface VariableCondition
var
- the SchemaVariable to be instantiatedinstCandidate
- the SVSubstitute (e.g. Term, ProgramElement) to be mapped to varmc
- the MatchCondition with the current matching state and in particular
the SVInstantiations that are already known to be neededservices
- the program information objectnull
otherwisepublic java.lang.String toString()
toString
in class java.lang.Object
Copyright © 2003-2019 The KeY-Project.