001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: package de.uka.ilkd.key.proof.examples;
010:
011: import de.uka.ilkd.key.java.Services;
012: import de.uka.ilkd.key.logic.*;
013: import de.uka.ilkd.key.logic.op.Op;
014: import de.uka.ilkd.key.proof.*;
015: import de.uka.ilkd.key.rule.ListOfTacletApp;
016: import de.uka.ilkd.key.rule.RuleApp;
017: import de.uka.ilkd.key.rule.SuccTacletBuilder;
018: import de.uka.ilkd.key.rule.Taclet;
019:
020: /** The {@link #run} method of this class will construct a proof object
021: * for the sequent that has the formula <code>true</code> in the succedent.
022: * It then prints out the proof and its list of open goals.
023: * Next, it constructs a taclet that will close such a goal and
024: * applies it.
025: *
026: * <p>Note that it is not strictly necessary to put our taclet into
027: * the Taclet index. We do it here, because TacletApp objects are
028: * rather complicated to construct by hand and the {@link
029: * RuleAppIndex} can do it for us.
030: */
031:
032: public class CloseProofForTrue {
033:
034: /** return the taclet <code>find(==>true) close goal</code> */
035: public Taclet buildTaclet() {
036: SuccTacletBuilder builder = new SuccTacletBuilder();
037: builder.setName(new Name("our_true_right"));
038: /* we can reuse the buildFormula method to construct the
039: true for the find part. */
040: builder.setFind(buildFormula());
041: /* For taclets that do not close the goal, one would need
042: to add some TacletGoalTemplates, but we are finished here. */
043: return builder.getTaclet();
044: }
045:
046: /** Return a taclet index with our taclet in it. */
047:
048: public TacletIndex buildTacletIndex() {
049: TacletIndex tacInd = new TacletIndex();
050: tacInd.add(buildTaclet());
051: return tacInd;
052: }
053:
054: /** Return an empty built-in rule index */
055: public BuiltInRuleIndex buildBuiltInRuleIndex() {
056: return new BuiltInRuleIndex();
057: }
058:
059: /** Return a RuleAppIndex appropriate for our rules.*/
060: public RuleAppIndex buildRuleAppIndex() {
061: return new RuleAppIndex(new TacletAppIndex(buildTacletIndex()),
062: new BuiltInRuleAppIndex(buildBuiltInRuleIndex()));
063: }
064:
065: public Term buildFormula() {
066: TermFactory tf = TermFactory.DEFAULT;
067: return tf.createJunctorTerm(Op.TRUE, new Term[0]);
068: }
069:
070: /** return a sequent containing the formula true. */
071: public Sequent buildSequent() {
072: ConstrainedFormula cf = new ConstrainedFormula(buildFormula());
073: Semisequent succ = Semisequent.EMPTY_SEMISEQUENT.insert(0, cf)
074: .semisequent();
075: return Sequent.createSuccSequent(succ);
076: }
077:
078: /** return the proof for the constructed sequent. */
079: public Proof buildInitialProof() {
080: Proof proof = new Proof("A Hand-made proof", new Services());
081: Sequent seq = buildSequent();
082: Node rootNode = new Node(proof, seq);
083: proof.setRoot(rootNode);
084: Goal firstGoal = new Goal(rootNode, buildRuleAppIndex());
085: proof.add(firstGoal);
086: /* In order to apply rules, the Namespaces need to be in place.*/
087: proof.setNamespaces(new NamespaceSet());
088: return proof;
089: }
090:
091: /** Return a {@link RuleApp} that will apply
092: * <code>taclet</code> on the first formula of the succedent.
093: */
094: public RuleApp getRuleApp(Goal goal) {
095: /* We find a position that points to the top level of the
096: * first formula in our sequent */
097: PosInOccurrence pos = new PosInOccurrence(goal.sequent()
098: .succedent().getFirst(), PosInTerm.TOP_LEVEL, false);
099:
100: /* now we get the list of rules applicable here... */
101: ListOfTacletApp rApplist = goal.ruleAppIndex().getTacletAppAt(
102: TacletFilter.TRUE, pos, null, Constraint.BOTTOM);
103: return rApplist.head();
104: }
105:
106: /** Build an initial proof with a formula in it. */
107: public void run() {
108: Proof proof = buildInitialProof();
109: printProof("initial Proof", proof);
110:
111: Goal goal = proof.openGoals().head();
112: RuleApp rapp = getRuleApp(goal);
113: System.out.println("Going to apply:" + rapp);
114: System.out.println(rapp.complete());
115:
116: /* Now, apply the rule */
117: goal.apply(rapp);
118:
119: printProof("one step later", proof);
120:
121: }
122:
123: public void printProof(String name, Proof proof) {
124: System.out.println(name + ":");
125: System.out.println(proof);
126: System.out.println("Open Goals:");
127: System.out.println(proof.openGoals());
128: System.out.println("Is the proof closed? : "
129: + (proof.closed() ? "Yes!" : "No..."));
130: System.out.println();
131: }
132:
133: public static void main(String[] args) {
134: new CloseProofForTrue().run();
135: }
136: }
|