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.SVSubstitute;
15: import de.uka.ilkd.key.logic.op.SchemaVariable;
16: import de.uka.ilkd.key.rule.VariableConditionAdapter;
17: import de.uka.ilkd.key.rule.inst.SVInstantiations;
18:
19: public class TestNonImplicitQuery extends VariableConditionAdapter {
20:
21: private SchemaVariable sv;
22:
23: public TestNonImplicitQuery(SchemaVariable sv) {
24: this .sv = sv;
25: }
26:
27: public SchemaVariable schemaVariable() {
28: return sv;
29: }
30:
31: public boolean check(SchemaVariable var, SVSubstitute methodName,
32: SVInstantiations matchCond, Services services) {
33: if (var != schemaVariable()) {
34: return true; // not responsible
35: }
36: return !methodName.toString().startsWith("<");
37: }
38:
39: public String toString() {
40: return "\\isNonImplicitQuery(" + schemaVariable() + ")";
41: }
42:
43: public boolean equals(Object o) {
44: if (!(o instanceof TestNonImplicitQuery)) {
45: return false;
46: }
47: TestNonImplicitQuery tq = (TestNonImplicitQuery) o;
48: return (tq.schemaVariable() == schemaVariable());
49: }
50:
51: public int hashCode() {
52: int result = 5;
53: result = 37 * result + schemaVariable().hashCode();
54: return result;
55: }
56:
57: }
|