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.Sequent;
13: import de.uka.ilkd.key.proof.*;
14:
15: /** The {@link #run} method of this class will construct a proof object
16: * for the empty sequent. It then prints out the proof and its list of
17: * open goals.
18: */
19:
20: public class BuildEmptyProof {
21:
22: /** Return a taclet index with no taclets in it. */
23: public TacletIndex buildTacletIndex() {
24: return new TacletIndex();
25: }
26:
27: /** Return an empty built-in rule index */
28: public BuiltInRuleIndex buildBuiltInRuleIndex() {
29: return new BuiltInRuleIndex();
30: }
31:
32: /** Return a RuleAppIndex appropriate for our rules.*/
33: public RuleAppIndex buildRuleAppIndex() {
34: return new RuleAppIndex(new TacletAppIndex(buildTacletIndex()),
35: new BuiltInRuleAppIndex(buildBuiltInRuleIndex()));
36: }
37:
38: /** return an empty sequent. */
39: public Sequent buildSequent() {
40: return Sequent.EMPTY_SEQUENT;
41: }
42:
43: /** return the proof for the constructed sequent. */
44: public Proof buildInitialProof() {
45: Proof proof = new Proof(new Services());
46: Sequent seq = buildSequent();
47: Node rootNode = new Node(proof, seq);
48: proof.setRoot(rootNode);
49: Goal firstGoal = new Goal(rootNode, buildRuleAppIndex());
50: proof.add(firstGoal);
51: return proof;
52: }
53:
54: /** build a Proof object for the empty sequent. */
55: public void run() {
56: Proof proof = buildInitialProof();
57:
58: System.out.println(proof);
59: System.out.println("Open Goals:");
60: System.out.println(proof.openGoals());
61: }
62:
63: public static void main(String[] args) {
64: new BuildEmptyProof().run();
65: }
66: }
|