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: //
010:
011: package de.uka.ilkd.key.proof;
012:
013: import junit.framework.TestCase;
014: import de.uka.ilkd.key.java.Services;
015: import de.uka.ilkd.key.logic.ConstrainedFormula;
016: import de.uka.ilkd.key.logic.Semisequent;
017: import de.uka.ilkd.key.logic.Sequent;
018: import de.uka.ilkd.key.rule.TacletForTests;
019:
020: /** class tests the goal, especially the split and set back mechanism.
021: */
022:
023: public class TestGoal extends TestCase {
024:
025: Proof proof;
026:
027: public TestGoal(String name) {
028: super (name);
029: }
030:
031: public void setUp() {
032: TacletForTests.parse();
033: proof = new Proof(new Services());
034:
035: }
036:
037: public void tearDown() {
038: proof = null;
039: }
040:
041: public void testSetBack0() {
042: Sequent seq = Sequent
043: .createSuccSequent(Semisequent.EMPTY_SEMISEQUENT
044: .insert(
045: 0,
046: new ConstrainedFormula(TacletForTests
047: .parseTerm("A"))).semisequent());
048: Goal g = new Goal(new Node(proof, seq), new RuleAppIndex(
049: new TacletAppIndex(new TacletIndex()),
050: new BuiltInRuleAppIndex(new BuiltInRuleIndex())));
051: ListOfGoal lg = g.split(3);
052: lg.head().addNoPosTacletApp(
053: TacletForTests.getRules().lookup("imp_right"));
054: lg.tail().head().addNoPosTacletApp(
055: TacletForTests.getRules().lookup("imp_left"));
056: lg.tail().tail().head().addNoPosTacletApp(
057: TacletForTests.getRules().lookup("or_right"));
058: //just check if the test is trivially correct because of rules not found
059: assertNotNull(lg.head().indexOfTaclets().lookup("imp_right"));
060: ListOfGoal lg0 = lg.head().split(3);
061: ListOfGoal lg00 = lg0.tail().head().split(8);
062: ListOfGoal lg1 = lg.tail().tail().head().split(2);
063: ListOfGoal res = lg.tail().head().setBack(
064: lg1.append(lg00).append(lg0.head()).append(
065: lg0.tail().tail().head()).append(
066: lg.tail().head()));
067: assertTrue(res.size() == 1);
068: assertNull(
069: "Taclet Index of set back goal contains rule \"imp-right\" that were not "
070: + "there before", res.head().indexOfTaclets()
071: .lookup("imp_right"));
072: assertNull(
073: "Taclet Index of set back goal contains rule \"or-right\"that were not "
074: + "there before", res.head().indexOfTaclets()
075: .lookup("or_right"));
076: assertNull(
077: "Taclet Index of set back goal contains rule \"imp-left\" that were not "
078: + "there before", res.head().indexOfTaclets()
079: .lookup("imp_left"));
080:
081: }
082:
083: public void invalidtestSetBack1() {
084: Sequent seq = Sequent
085: .createSuccSequent(Semisequent.EMPTY_SEMISEQUENT
086: .insert(
087: 0,
088: new ConstrainedFormula(TacletForTests
089: .parseTerm("A"))).semisequent());
090: Goal g = new Goal(new Node(proof, seq), new RuleAppIndex(
091: new TacletAppIndex(new TacletIndex()),
092: new BuiltInRuleAppIndex(new BuiltInRuleIndex())));
093: ListOfGoal lg = g.split(3);
094: lg.head().addNoPosTacletApp(
095: TacletForTests.getRules().lookup("imp_right"));
096: lg.tail().head().addNoPosTacletApp(
097: TacletForTests.getRules().lookup("imp_left"));
098: lg.tail().tail().head().addNoPosTacletApp(
099: TacletForTests.getRules().lookup("or_right"));
100: //just check if the test is trivially correct because of rules not found
101: assertNotNull(lg.head().indexOfTaclets().lookup("imp_right"));
102:
103: ListOfGoal lg0 = lg.head().split(4);
104: lg0.head().addNoPosTacletApp(
105: TacletForTests.getRules().lookup("or_left"));
106: lg0.tail().head().addNoPosTacletApp(
107: TacletForTests.getRules().lookup("or_left"));
108: ListOfGoal lg1 = lg.tail().tail().head().split(2);
109: ListOfGoal res = lg0.tail().head().setBack(
110: lg1.append(lg0).append(lg.tail().head()));
111: assertTrue(res.size() == 4);
112:
113: assertTrue(res.contains(lg1.head()));
114: assertNotNull(lg1.head().indexOfTaclets().lookup("or_right"));
115: // assertTrue(lg1.head().indexOfTaclets().lookup("or_left")==null);
116: res = res.removeAll(lg1.head());
117:
118: assertTrue(res.contains(lg1.tail().head()));
119: assertNotNull(lg1.tail().head().indexOfTaclets().lookup(
120: "or_right"));
121: // assertTrue(lg1.tail().head().indexOfTaclets().lookup("or_left")==null);
122: res = res.removeAll(lg1.tail().head());
123: if (res.head().indexOfTaclets().lookup("imp_right") != null) {
124: assertNotNull(res.tail().head().indexOfTaclets().lookup(
125: "imp_left"));
126: } else {
127: assertNotNull(res.head().indexOfTaclets()
128: .lookup("imp_left"));
129: assertNotNull(res.tail().head().indexOfTaclets().lookup(
130: "imp_right"));
131: }
132: assertNull(res.head().indexOfTaclets().lookup("or_left"));
133: assertNull(res.tail().head().indexOfTaclets().lookup("or_left"));
134:
135: }
136:
137: }
|