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: package de.uka.ilkd.key.proof.examples;
10:
11: import de.uka.ilkd.key.java.Services;
12: import de.uka.ilkd.key.logic.*;
13: import de.uka.ilkd.key.logic.op.Op;
14: import de.uka.ilkd.key.proof.*;
15:
16: /** The {@link #run} method of this class will construct a proof object
17: * for the sequent that has the formula <code>true</code> in the succedent.
18: * It then prints out the proof and its list of open goals.
19: */
20:
21: public class BuildProofForTrue {
22:
23: /** Return a taclet index with no taclets in it. */
24: public TacletIndex buildTacletIndex() {
25: return new TacletIndex();
26: }
27:
28: /** Return an empty built-in rule index */
29: public BuiltInRuleIndex buildBuiltInRuleIndex() {
30: return new BuiltInRuleIndex();
31: }
32:
33: /** Return a RuleAppIndex appropriate for our rules.*/
34: public RuleAppIndex buildRuleAppIndex() {
35: return new RuleAppIndex(new TacletAppIndex(buildTacletIndex()),
36: new BuiltInRuleAppIndex(buildBuiltInRuleIndex()));
37: }
38:
39: /** Return the formula <code>true</code> */
40: public Term buildFormula() {
41: TermFactory tf = TermFactory.DEFAULT;
42: return tf.createJunctorTerm(Op.TRUE, new Term[0]);
43: }
44:
45: /** return a sequent containing the formula true. */
46: public Sequent buildSequent() {
47: ConstrainedFormula cf = new ConstrainedFormula(buildFormula());
48: Semisequent succ = Semisequent.EMPTY_SEMISEQUENT.insert(0, cf)
49: .semisequent();
50: return Sequent.createSuccSequent(succ);
51: }
52:
53: /** return the proof for the constructed sequent. */
54: public Proof buildInitialProof() {
55: Proof proof = new Proof(new Services());
56: Sequent seq = buildSequent();
57: Node rootNode = new Node(proof, seq);
58: proof.setRoot(rootNode);
59: Goal firstGoal = new Goal(rootNode, buildRuleAppIndex());
60: proof.add(firstGoal);
61: return proof;
62: }
63:
64: /** Build an initial proof with a formula in it. */
65: public void run() {
66: Proof proof = buildInitialProof();
67: printProof("initial Proof", proof);
68: }
69:
70: public void printProof(String name, Proof proof) {
71: System.out.println(name + ":");
72: System.out.println(proof);
73: System.out.println("Open Goals:");
74: System.out.println(proof.openGoals());
75: System.out.println();
76: }
77:
78: public static void main(String[] args) {
79: new BuildProofForTrue().run();
80: }
81: }
|