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.proof.*;
014: import de.uka.ilkd.key.rule.*;
015:
016: public class TransformProgram {
017:
018: private Services services = new Services();
019: static final String ORIG_PROGRAM = "\\<{ try {} catch ( Exception e ) {} catch ( Throwable e ) {} }\\> true";
020:
021: /** return the taclet <code>find(==>true) close goal</code> */
022: public Taclet buildTaclet() {
023: SuccTacletBuilder builder = new SuccTacletBuilder();
024: builder.setName(new Name("our_true_right"));
025: /* we can reuse the buildFormula method to construct the
026: true for the find part. */
027: builder.setFind(buildFormula());
028: /* For taclets that do not close the goal, one would need
029: to add some TacletGoalTemplates, but we are finished here. */
030: return builder.getTaclet();
031: }
032:
033: /** Return a taclet index with our taclet in it. */
034:
035: public TacletIndex buildTacletIndex() {
036: /*
037: TacletIndex tacInd = new TacletIndex();
038: tacInd.add(buildTaclet());
039: return tacInd;
040: */
041: TacletForTests
042: .setStandardFile(System.getProperty("key.home")
043: + "/system/resources/de/uka/ilkd/key/proof/rules/javaRules.key");
044: TacletForTests.parse();
045: return TacletForTests.getRules();
046:
047: }
048:
049: /** Return an empty built-in rule index */
050: public BuiltInRuleIndex buildBuiltInRuleIndex() {
051: return new BuiltInRuleIndex();
052: }
053:
054: /** Return a RuleAppIndex appropriate for our rules.*/
055: public RuleAppIndex buildRuleAppIndex() {
056: return new RuleAppIndex(new TacletAppIndex(buildTacletIndex()),
057: new BuiltInRuleAppIndex(buildBuiltInRuleIndex()));
058: }
059:
060: public Term buildFormula() {
061: return TacletForTests.parseTerm(ORIG_PROGRAM, services);
062: }
063:
064: /** return a sequent containing the formula true. */
065: public Sequent buildSequent() {
066: ConstrainedFormula cf = new ConstrainedFormula(buildFormula());
067: Semisequent succ = Semisequent.EMPTY_SEMISEQUENT.insert(0, cf)
068: .semisequent();
069: return Sequent.createSuccSequent(succ);
070: }
071:
072: /** return the proof for the constructed sequent. */
073: public Proof buildInitialProof() {
074: Proof proof = new Proof("A Hand-made proof", services);
075: Sequent seq = buildSequent();
076: Node rootNode = new Node(proof, seq);
077: proof.setRoot(rootNode);
078: Goal firstGoal = new Goal(rootNode, buildRuleAppIndex());
079: proof.add(firstGoal);
080: /* In order to apply rules, the Namespaces need to be in place.*/
081: proof.setNamespaces(new NamespaceSet());
082: return proof;
083: }
084:
085: /** Return a {@link RuleApp} that will apply
086: * <code>taclet</code> on the first formula of the succedent.
087: */
088: public RuleApp getRuleApp(Goal goal) {
089: /* We find a position that points to the top level of the
090: * first formula in our sequent */
091: PosInOccurrence pos = new PosInOccurrence(goal.sequent()
092: .succedent().getFirst(), PosInTerm.TOP_LEVEL, false);
093:
094: /* now we get the list of rules applicable here... */
095: ListOfTacletApp rApplist = goal.ruleAppIndex().getTacletAppAt(
096: TacletFilter.TRUE, pos, null, Constraint.BOTTOM);
097: return rApplist.head();
098: }
099:
100: private void oneStep(Proof proof) {
101: Goal goal = proof.openGoals().head();
102: RuleApp rapp = getRuleApp(goal);
103: System.out.println("Going to apply:" + rapp);
104: System.out.println(rapp.complete());
105: // Now, apply the rule
106: goal.apply(rapp);
107: printProof("one step later", proof);
108: }
109:
110: /** Build an initial proof with a formula in it. */
111: public void run() {
112: TacletForTests.setStandardFile(TacletForTests.testRules);
113: TacletForTests.parse();
114:
115: Proof proof = buildInitialProof();
116: proof.setSimplifier(new UpdateSimplifier());
117: printProof("initial Proof", proof);
118:
119: oneStep(proof);
120: oneStep(proof);
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 TransformProgram().run();
135: }
136: }
|