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: // This file is part of KeY - Integrated Deductive Software Design
09:
10: package de.uka.ilkd.key.rule.conditions;
11:
12: import de.uka.ilkd.key.java.Services;
13: import de.uka.ilkd.key.logic.op.ProgramVariable;
14: import de.uka.ilkd.key.logic.op.SVSubstitute;
15: import de.uka.ilkd.key.logic.op.SchemaVariable;
16: import de.uka.ilkd.key.logic.Term;
17: import de.uka.ilkd.key.logic.op.IUpdateOperator;
18: import de.uka.ilkd.key.rule.VariableConditionAdapter;
19: import de.uka.ilkd.key.rule.inst.SVInstantiations;
20:
21: /**
22: * Ensures the given ProgramElement denotes a local variable
23: */
24: public class IsUpdatedVariableCondition extends
25: VariableConditionAdapter {
26: private SchemaVariable var;
27: private boolean neg;
28:
29: public IsUpdatedVariableCondition(SchemaVariable var, boolean neg) {
30: this .var = var;
31: this .neg = neg;
32: if (!(var.isFormulaSV() || var.isTermSV())) {
33: throw new IllegalArgumentException(
34: "Illegal schema variable");
35: }
36: }
37:
38: /**
39: * checks if the condition for a correct instantiation is fulfilled
40: * @param var the template Variable to be instantiated
41: * @param candidate the SVSubstitute which is a candidate for an
42: * instantiation of var
43: * @param svInst the SVInstantiations that are already known to be needed
44: * @return true iff condition is fulfilled
45: */
46: public boolean check(SchemaVariable var, SVSubstitute candidate,
47: SVInstantiations svInst, Services services) {
48: if (var != this .var) {
49: return true;
50: }
51: if (candidate == null)
52: return false;
53: if (!(candidate instanceof Term)) {
54: // System.out.println("Candidate is not a term");
55: // System.out.println("Candidate="+candidate.toString());
56: return false;
57: }
58: Term term = (Term) candidate;
59: // System.out.println("Candidate:"+term.toString());
60: return term.op() instanceof IUpdateOperator;
61: }
62:
63: public String toString() {
64: return "\\isUpdated (" + var + ")";
65: }
66:
67: }
|