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;
12:
13: import de.uka.ilkd.key.logic.op.SchemaVariable;
14:
15: /**
16: * class containing a pair of SchemaVariables, the first one being a
17: * TermSV, the second one a FormulaSV, representing a "c new depending
18: * on phi" statement within a varcond of a taclet
19: */
20: public class NewDependingOn {
21:
22: private SchemaVariable first;
23: private SchemaVariable second;
24:
25: /**
26: * constructs a pair of variables given two SchemaVariables. The first SchemaVariable
27: * has to occur bound in the Taclet, while the second one can stand for a
28: * an arbitrary term of formula, in order to model a pair of the not-free-in relation of
29: * an Taclet.
30: */
31: public NewDependingOn(SchemaVariable first, SchemaVariable second) {
32: if (!((first.isSkolemTermSV() || first.isFormulaSV()) && (second
33: .isFormulaSV() || second.isTermSV()))) {
34: throw new RuntimeException(
35: "NewDependingOn: First SchemaVariable has to be a SkolemTermSV or FormulaSV, "
36: + "the second one has to be a FormulaSV or a TermSV");
37: }
38: this .first = first;
39: this .second = second;
40: }
41:
42: /** returns the first SchemaVariable of the pair. This
43: * SchemaVariable has to be matched to a QuantifiableVariable
44: */
45: public SchemaVariable first() {
46: return first;
47: }
48:
49: /** returns the second SchemaVariable of the pair. */
50: public SchemaVariable second() {
51: return second;
52: }
53:
54: public String toString() {
55: return "\\new(" + first() + ", \\dependingOn(" + second()
56: + "))";
57: }
58:
59: public boolean equals(Object o) {
60: NewDependingOn nfi = (NewDependingOn) o;
61: return (nfi.first == first() && nfi.second == second());
62: }
63:
64: public int hashCode() {
65: int result = 17;
66: result = 37 * result + first().hashCode();
67: result = 37 * result + second().hashCode();
68: return result;
69: }
70:
71: }
|