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: /** class contains a pair of SchemaVariables, the first part has to be
12: * match a QuantifiableVariable, the second one a
13: * Term in order to model a pair of the not-free-in relation of
14: * an Taclet.*/package de.uka.ilkd.key.rule;
15:
16: import de.uka.ilkd.key.logic.op.SchemaVariable;
17:
18: public class NotFreeIn {
19:
20: private SchemaVariable first;
21: private SchemaVariable second;
22:
23: /**
24: * constructs a pair of variables given two SchemaVariables. The first SchemaVariable
25: * has to occur bound in the Taclet, while the second one can stand for a
26: * an arbitrary term of formula, in order to model a pair of the not-free-in relation of
27: * an Taclet.
28: */
29: public NotFreeIn(SchemaVariable first, SchemaVariable second) {
30: if (!first.isVariableSV()) {
31: throw new RuntimeException("Expected a SchemaVariable "
32: + "that has been only allowed to match "
33: + "variables");
34: }
35: this .first = first;
36: this .second = second;
37: }
38:
39: /** returns the first SchemaVariable of the pair. This
40: * SchemaVariable has to be matched to a QuantifiableVariable
41: */
42: public SchemaVariable first() {
43: return first;
44: }
45:
46: /** returns the second SchemaVariable of the pair. */
47: public SchemaVariable second() {
48: return second;
49: }
50:
51: public String toString() {
52: return "\\notFreeIn(" + first() + "," + second() + ")";
53: }
54:
55: public boolean equals(Object o) {
56: NotFreeIn nfi = (NotFreeIn) o;
57: return (nfi.first == first() && nfi.second == second());
58: }
59:
60: public int hashCode() {
61: int result = 17;
62: result = 37 * result + first().hashCode();
63: result = 37 * result + second().hashCode();
64: return result;
65: }
66:
67: }
|