The instantiations of a schemavariable can be restricted on rule scope by
attaching conditions on these variables. Such a condition is realized by a class
which implements this interface.
The usual place where to put these implementations is inside package
de.uka.ilkd.key.rule.conditions. For variable conditions
that know only black and white answers there exists a convenience class
de.uka.ilkd.key.rule.VariableConditionAdapter .
check(SchemaVariable var, SVSubstitute instCandidate, MatchConditions matchCond, Services services) checks if the condition for a correct instantiation is fulfilled
Parameters: var - the SchemaVariable to be instantiated Parameters: instCandidate - the SVSubstitute (e.g.
checks if the condition for a correct instantiation is fulfilled
Parameters: var - the SchemaVariable to be instantiated Parameters: instCandidate - the SVSubstitute (e.g. Term, ProgramElement) to be mapped to var Parameters: matchCond - the MatchCondition with the current matching state and in particular the SVInstantiations that are already known to be needed Parameters: services - the program information object modified match results if the condition can be satisfied,or null otherwise