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.conditions;
12:
13: import de.uka.ilkd.key.java.Services;
14: import de.uka.ilkd.key.logic.op.ProgramVariable;
15: import de.uka.ilkd.key.logic.op.SVSubstitute;
16: import de.uka.ilkd.key.logic.op.SchemaVariable;
17: import de.uka.ilkd.key.rule.VariableConditionAdapter;
18: import de.uka.ilkd.key.rule.inst.SVInstantiations;
19:
20: /**
21: * Ensures the given ProgramElement denotes a local variable
22: */
23: public class LocalVariableCondition extends VariableConditionAdapter {
24:
25: private SchemaVariable var;
26: private boolean neg;
27:
28: public LocalVariableCondition(SchemaVariable var, boolean neg) {
29: this .var = var;
30: this .neg = neg;
31: if (!var.isProgramSV()) {
32: throw new IllegalArgumentException(
33: "Illegal schema variable");
34: }
35: }
36:
37: /**
38: * checks if the condition for a correct instantiation is fulfilled
39: * @param var the template Variable to be instantiated
40: * @param candidate the SVSubstitute which is a candidate for an
41: * instantiation of var
42: * @param svInst the SVInstantiations that are already known to be needed
43: * @return true iff condition is fulfilled
44: */
45: public boolean check(SchemaVariable var, SVSubstitute candidate,
46: SVInstantiations svInst, Services services) {
47:
48: if (var != this .var) {
49: return true;
50: }
51: final boolean isLocalVar = ((candidate instanceof ProgramVariable) && !((ProgramVariable) candidate)
52: .isMember());
53: return neg ? !isLocalVar : isLocalVar;
54: }
55:
56: public String toString() {
57: return "\\isLocalVariable (" + var + ")";
58: }
59:
60: }
|