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: /** this class inherits from TacletGoalTemplate. It is used if there is a
12: * replacewith in the ruleGoals that replaces a sequent with a
13: * sequent. The replacewith for terms/formulae is realized in another
14: * class calles RewriteTacletGoalTemplate.
15: */package de.uka.ilkd.key.rule;
16:
17: import de.uka.ilkd.key.logic.BoundVarsVisitor;
18: import de.uka.ilkd.key.logic.Sequent;
19: import de.uka.ilkd.key.logic.op.SetAsListOfSchemaVariable;
20: import de.uka.ilkd.key.logic.op.SetOfQuantifiableVariable;
21: import de.uka.ilkd.key.logic.op.SetOfSchemaVariable;
22:
23: public class AntecSuccTacletGoalTemplate extends TacletGoalTemplate {
24: /** sequent that replaces another one */
25: private Sequent replacewith = Sequent.EMPTY_SEQUENT;
26:
27: /** creates new Goaldescription
28: *@param addedSeq new Sequent to be added
29: *@param addedRules ListOfTaclet contains the new allowed rules
30: * at this branch
31: *@param ruleVars ListOfRulevariable contains used rulevariables
32: *@param replacewith the Sequent that replaces another one
33: */
34: public AntecSuccTacletGoalTemplate(Sequent addedSeq,
35: ListOfTaclet addedRules, Sequent replacewith,
36: SetOfSchemaVariable pvs) {
37: super (addedSeq, addedRules, pvs);
38: TacletBuilder.checkContainsFreeVarSV(replacewith, null,
39: "replacewith sequent");
40: this .replacewith = replacewith;
41: }
42:
43: public AntecSuccTacletGoalTemplate(Sequent addedSeq,
44: ListOfTaclet addedRules, Sequent replacewith) {
45: this (addedSeq, addedRules, replacewith,
46: SetAsListOfSchemaVariable.EMPTY_SET);
47: }
48:
49: /** a Taclet may replace a Sequent by another. The new Sequent is returned.
50: * this Sequent.
51: * @return Sequent being paramter in the rule goal replacewith(Seq)
52: */
53: public Sequent replaceWith() {
54: return replacewith;
55: }
56:
57: /**
58: * rertieves and returns all variables that are bound in the
59: * goal template
60: * @return all variables that occur bound in this goal template
61: */
62: protected SetOfQuantifiableVariable getBoundVariables() {
63: final BoundVarsVisitor bvv = new BoundVarsVisitor();
64: bvv.visit(replaceWith());
65: return bvv.getBoundVariables().union(super .getBoundVariables());
66: }
67:
68: /**
69: * @return Sequent being paramter in the rule goal replacewith(Seq)
70: */
71: Object replaceWithExpressionAsObject() {
72: return replacewith;
73: }
74:
75: public boolean equals(Object o) {
76: if (!(o instanceof AntecSuccTacletGoalTemplate))
77: return false;
78: AntecSuccTacletGoalTemplate other = (AntecSuccTacletGoalTemplate) o;
79:
80: return super .equals(other)
81: && replacewith.equals(other.replacewith);
82: }
83:
84: public int hashCode() {
85: int result = 17;
86: result = 37 * result + super .hashCode();
87: result = 37 * result + replacewith.hashCode();
88: return result;
89: }
90:
91: /** toString */
92: public String toString() {
93: String result = super .toString();
94: result += "\\replacewith(" + replaceWith() + ") ";
95: return result;
96: }
97:
98: }
|