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: import de.uka.ilkd.key.rule.inst.SVInstantiations;
17:
18: /**
19: * The variable condition adapter can be used by variable conditions
20: * which can either fail or be successful, but which do not create a
21: * constraint.
22: */
23:
24: public abstract class VariableConditionAdapter implements
25: VariableCondition {
26:
27: /**
28: * checks if the condition for a correct instantiation is fulfilled
29: * @param var the template Variable to be instantiated
30: * @param instMap the MatchCondition with the current matching state and in particular
31: * the SVInstantiations that are already known to be needed
32: * @param services the program information object
33: * @return true iff condition is fulfilled
34: */
35: public abstract boolean check(SchemaVariable var,
36: SVSubstitute instCandidate, SVInstantiations instMap,
37: Services services);
38:
39: /**
40: * checks if the condition for a correct instantiation is fulfilled
41: * @param var the template Variable to be instantiated
42: * @param instCandidate the SVSubstitute the schemavariable is matched against
43: * @param matchCond the MatchCondition with the current matching state and in particular
44: * the SVInstantiations that are already known to be needed
45: * @param services the program information object
46: * @return modified match results if the condition can be satisfied,
47: * or <code>null</code> otherwise
48: */
49: public MatchConditions check(SchemaVariable var,
50: SVSubstitute instCandidate, MatchConditions matchCond,
51: Services services) {
52: return check(var, instCandidate, matchCond.getInstantiations(),
53: services) ? matchCond : null;
54: }
55:
56: }
|