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.java.Services;
14: import de.uka.ilkd.key.logic.ConstrainedFormula;
15: import de.uka.ilkd.key.proof.ProofSaver;
16:
17: /**
18: * Instantiation of an if-formula that has to be proven by an explicit
19: * if-goal
20: */
21:
22: public class IfFormulaInstDirect implements IfFormulaInstantiation {
23:
24: /**
25: * Simply the formula
26: */
27: private ConstrainedFormula cf;
28:
29: public IfFormulaInstDirect(ConstrainedFormula p_cf) {
30: cf = p_cf;
31: }
32:
33: /**
34: * @return the cf this is pointing to
35: */
36: public ConstrainedFormula getConstrainedFormula() {
37: return cf;
38: }
39:
40: public String toString() {
41: return toString(null);
42: }
43:
44: public boolean equals(Object p_obj) {
45: if (!(p_obj instanceof IfFormulaInstDirect)) {
46: return false;
47: }
48: return cf.equals(((IfFormulaInstDirect) p_obj).cf);
49: }
50:
51: public int hashCode() {
52: int result = 17;
53: result = 37 * result + cf.hashCode();
54: return result;
55: }
56:
57: public String toString(Services services) {
58: return ProofSaver.printAnything(cf.formula(), services)
59: + (cf.constraint().isBottom() ? "" : "<<"
60: + cf.constraint());
61: }
62: }
|