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: * This variable condition checks if a schemavariable is instantiated with a reference type
22: */
23: public class NonImplicitTypeCondition extends VariableConditionAdapter {
24:
25: private SchemaVariable var;
26:
27: /**
28: * creates an instance of this condition checking if var has reference type
29: * @param var the SchemaVariable to be checked
30: */
31: public NonImplicitTypeCondition(SchemaVariable var) {
32: this .var = var;
33: }
34:
35: /**
36: * checks if the condition for a correct instantiation is fulfilled
37: * @param var the template Variable to be instantiated
38: * @param candidate the SVSubstitute which is a candidate for an
39: * instantiation of var
40: * @param svInst the SVInstantiations that are already known to be needed
41: * @return true iff condition is fulfilled
42: */
43: public boolean check(SchemaVariable var, SVSubstitute candidate,
44: SVInstantiations svInst, Services services) {
45: if (var != this .var)
46: return true;
47: return !((candidate instanceof ProgramVariable) && ((ProgramVariable) candidate)
48: .isImplicit());
49: }
50:
51: public String toString() {
52: return "\\isNonImplicit(" + var + ")";
53: }
54:
55: }
|