01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: //
10:
11: package de.uka.ilkd.key.rule;
12:
13: import de.uka.ilkd.key.java.Services;
14: import de.uka.ilkd.key.logic.op.SVSubstitute;
15: import de.uka.ilkd.key.logic.op.SchemaVariable;
16:
17: /**
18: * The instantiations of a schemavariable can be restricted on rule scope by
19: * attaching conditions on these variables. Such a condition is realized by a class
20: * which implements this interface.
21: *
22: * The usual place where to put these implementations is inside package
23: * <code>de.uka.ilkd.key.rule.conditions</code>. For variable conditions
24: * that know only black and white answers there exists a convenience class
25: * {@link de.uka.ilkd.key.rule.VariableConditionAdapter}.
26: */
27: public interface VariableCondition {
28:
29: /**
30: * checks if the condition for a correct instantiation is fulfilled
31: * @param var the SchemaVariable to be instantiated
32: * @param instCandidate the SVSubstitute (e.g. Term, ProgramElement) to be mapped to var
33: * @param matchCond the MatchCondition with the current matching state and in particular
34: * the SVInstantiations that are already known to be needed
35: * @param services the program information object
36: * @return modified match results if the condition can be satisfied,
37: * or <code>null</code> otherwise
38: */
39: MatchConditions check(SchemaVariable var,
40: SVSubstitute instCandidate, MatchConditions matchCond,
41: Services services);
42:
43: }
|