0001: // This file is part of KeY - Integrated Deductive Software Design
0002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
0003: // Universitaet Koblenz-Landau, Germany
0004: // Chalmers University of Technology, Sweden
0005: //
0006: // The KeY system is protected by the GNU General Public License.
0007: // See LICENSE.TXT for details.
0008: //
0009: //
0010:
0011: package de.uka.ilkd.key.rule;
0012:
0013: import junit.framework.TestCase;
0014: import de.uka.ilkd.key.java.NameAbstractionTable;
0015: import de.uka.ilkd.key.java.ProgramElement;
0016: import de.uka.ilkd.key.java.Services;
0017: import de.uka.ilkd.key.logic.*;
0018: import de.uka.ilkd.key.logic.op.*;
0019: import de.uka.ilkd.key.logic.sort.PrimitiveSort;
0020: import de.uka.ilkd.key.logic.sort.Sort;
0021: import de.uka.ilkd.key.proof.*;
0022:
0023: /**
0024: * class tests the apply methods in Taclet
0025: */
0026: public class TestApplyTaclet extends TestCase {
0027:
0028: final static String[] strs = {
0029: "",
0030: "(A -> B) -> (!(!(A -> B)))",
0031: "",
0032: "\\forall s z; p(z)",
0033: "(A -> B) -> (!(!(A -> B)))",
0034: "(A -> B) -> (!(!(A -> B)))",
0035: "(A -> B) -> (!(!(A -> B)))",
0036: "",
0037: "",
0038: "\\<{try{while (1==1) {if (1==2) {break;}} return 1==3; int i=17; } catch (Exception e) { return null;}}\\>A",
0039: "A & B",
0040: "",
0041: "s{}::isEmpty(sset)",
0042: "s{}::size(sset)=0",
0043: "A & (A & B)",
0044: "",
0045: "f(const)=const",
0046: "const=f(f(const))",
0047: "f(const)=const",
0048: "const=f(const)",
0049: "f(const)=const",
0050: "A & {i:=0}(const=f(const))",
0051: "f(const)=const",
0052: "A & {i:=0}(const=f(f(const)))",
0053: "{i:=0}(f(const)=const)",
0054: "{i:=1}(const=f(const)) & \\<{i=2;}\\>(const=f(const)) "
0055: + "& {i:=0}(const=f(const))",
0056: "{i:=0}(f(const)=const)",
0057: "{i:=1}(const=f(const)) & \\<{i=2;}\\>(const=f(const)) "
0058: + "& {i:=0}(const=const)",
0059: "",
0060: "\\<{ {} {break;} }\\> true",
0061: "",
0062: "\\<{ {{}} {{break;}} }\\> true",
0063: "",
0064: "\\<{ try {} catch ( Exception e ) {} catch ( Throwable e ) {} }\\> true",
0065: "",
0066: "\\<{ try {} catch ( Exception e ) {} try {} catch ( Throwable e ) {} }\\> true",
0067: "",
0068: "\\<{ try {} catch ( Exception e ) {break;} catch ( Throwable e ) {continue;} }\\> true",
0069: "",
0070: "\\<{ try {} catch ( Exception e ) {break;} try {} catch ( Throwable e ) {continue;} }\\> true",
0071: "",
0072: "\\<{ try {} catch ( Exception e ) {} catch ( Throwable e ) {} finally {} }\\> true",
0073: "",
0074: "\\<{ try {} catch ( Exception e ) {} finally {} try {} catch ( Throwable e ) {} }\\> true",
0075: "",
0076: "\\<{try{while (1==1) {if (1==2) {break;}} return 1==3; int i=17; } catch (Exception e) { return null;}}\\>\\forall int i; i>0",
0077: "",
0078: "\\<{try{ {} while (1==1) {if (1==2) {break;}} return 1==3; int i=17; } catch (Exception e) { return null;}}\\>\\forall int i; i>0" };
0079: Proof[] proof;
0080: Proof mvProof;
0081: // mv=f(X,c)
0082: Constraint consMV_f_X_c;
0083: // mv=f(c,X)
0084: Constraint consMV_f_c_X;
0085:
0086: public TestApplyTaclet(String name) {
0087: super (name);
0088: // Debug.ENABLE_DEBUG = true;
0089:
0090: }
0091:
0092: private static Semisequent parseTermForSemisequent(String t) {
0093: if ("".equals(t)) {
0094: return Semisequent.EMPTY_SEMISEQUENT;
0095: }
0096: ConstrainedFormula cf0 = new ConstrainedFormula(TacletForTests
0097: .parseTerm(t));
0098: return Semisequent.EMPTY_SEMISEQUENT.insert(0, cf0)
0099: .semisequent();
0100: }
0101:
0102: public void setUp() {
0103: TermBuilder tf = TermBuilder.DF;
0104:
0105: TacletForTests.setStandardFile(TacletForTests.testRules);
0106: TacletForTests.parse();
0107: UpdateSimplifier sus = new UpdateSimplifier();
0108: Services services = new Services();
0109: proof = new Proof[strs.length / 2];
0110:
0111: for (int i = 0; i < proof.length; i++) {
0112: Semisequent antec = parseTermForSemisequent(strs[2 * i]);
0113: Semisequent succ = parseTermForSemisequent(strs[2 * i + 1]);
0114: Sequent s = Sequent.createSequent(antec, succ);
0115: proof[i] = new Proof(services);
0116: proof[i].setSimplifier(sus);
0117: proof[i].setRoot(new Node(proof[i], s));
0118: }
0119:
0120: // proof required to test application with mv
0121: mvProof = new Proof(services);
0122: mvProof.setSimplifier(sus);
0123:
0124: Sort s = new PrimitiveSort(new Name("test"));
0125:
0126: Function f = new RigidFunction(new Name("f"), s, new Sort[] {
0127: s, s });
0128: Function c = new RigidFunction(new Name("c"), s, new Sort[] {});
0129:
0130: Metavariable mv_x = new Metavariable(new Name("X"), s);
0131: Metavariable mv = new Metavariable(new Name("mv"), s);
0132:
0133: Term t_mv = tf.func(mv);
0134: Term t_mv_x = tf.func(mv_x);
0135:
0136: Term t_c = tf.func(c);
0137: Term t_f_X_c = tf.func(f, new Term[] { t_mv_x, t_c });
0138: Term t_f_c_X = tf.func(f, new Term[] { t_c, t_mv_x });
0139:
0140: consMV_f_c_X = Constraint.BOTTOM.unify(t_mv, t_f_c_X, null);
0141: consMV_f_X_c = Constraint.BOTTOM.unify(t_mv, t_f_X_c, null);
0142:
0143: assertTrue(consMV_f_c_X.isSatisfiable()
0144: && consMV_f_X_c.isSatisfiable());
0145:
0146: ConstrainedFormula cf1 = new ConstrainedFormula(TacletForTests
0147: .parseTerm("A & B"), consMV_f_c_X);
0148: ConstrainedFormula cf2 = new ConstrainedFormula(TacletForTests
0149: .parseTerm("!(A | B)"), consMV_f_X_c);
0150:
0151: Sequent seq = Sequent.createSequent(
0152: Semisequent.EMPTY_SEMISEQUENT.insertLast(cf1)
0153: .semisequent(), Semisequent.EMPTY_SEMISEQUENT
0154: .insertLast(cf2).semisequent());
0155:
0156: mvProof.setRoot(new Node(mvProof, seq));
0157: }
0158:
0159: public void tearDown() {
0160: proof = null;
0161: mvProof = null;
0162: // mv=f(X,c)
0163: consMV_f_X_c = null;
0164: // mv=f(c,X)
0165: consMV_f_c_X = null;
0166: }
0167:
0168: public void testSuccTacletWithoutIf() {
0169: Term fma = proof[0].root().sequent().succedent().getFirst()
0170: .formula();
0171: NoPosTacletApp impright = TacletForTests.getRules().lookup(
0172: "imp_right");
0173: TacletIndex tacletIndex = new TacletIndex();
0174: tacletIndex.add(impright);
0175: Goal goal = createGoal(proof[0].root(), tacletIndex);
0176: PosInOccurrence applyPos = new PosInOccurrence(goal.sequent()
0177: .succedent().getFirst(), PosInTerm.TOP_LEVEL, false);
0178: ListOfTacletApp rApplist = goal.ruleAppIndex().getTacletAppAt(
0179: TacletFilter.TRUE, applyPos, null, Constraint.BOTTOM);
0180: assertTrue("Too many or zero rule applications.", rApplist
0181: .size() == 1);
0182: RuleApp rApp = rApplist.head();
0183: assertTrue("Rule App should be complete", rApp.complete());
0184: ListOfGoal goals = rApp
0185: .execute(goal, TacletForTests.services());
0186: assertTrue("Too many or zero goals for imp-right.", goals
0187: .size() == 1);
0188: Sequent seq = goals.head().sequent();
0189: assertEquals("Wrong antecedent after imp-right", seq
0190: .antecedent().getFirst().formula(), fma.sub(0));
0191: assertEquals("Wrong succedent after imp-right", seq.succedent()
0192: .getFirst().formula(), fma.sub(1));
0193: }
0194:
0195: public void testAddingRule() {
0196: Term fma = proof[0].root().sequent().succedent().getFirst()
0197: .formula();
0198: NoPosTacletApp imprightadd = TacletForTests.getRules().lookup(
0199: "TestApplyTaclet_imp_right_add");
0200: TacletIndex tacletIndex = new TacletIndex();
0201: tacletIndex.add(imprightadd);
0202: Goal goal = createGoal(proof[0].root(), tacletIndex);
0203: PosInOccurrence applyPos = new PosInOccurrence(goal.sequent()
0204: .succedent().getFirst(), PosInTerm.TOP_LEVEL, false);
0205: ListOfTacletApp rApplist = goal.ruleAppIndex().getTacletAppAt(
0206: TacletFilter.TRUE, applyPos, null, Constraint.BOTTOM);
0207: assertTrue("Too many or zero rule applications.", rApplist
0208: .size() == 1);
0209: RuleApp rApp = rApplist.head();
0210: assertTrue("Rule App should be complete", rApp.complete());
0211: ListOfGoal goals = rApp
0212: .execute(goal, TacletForTests.services());
0213: assertTrue("Too many or zero goals for imp_right_add.", goals
0214: .size() == 1);
0215: Sequent seq = goals.head().sequent();
0216: assertEquals("Wrong antecedent after imp_right_add", seq
0217: .antecedent().getFirst().formula(), fma.sub(0));
0218: assertEquals("Wrong succedent after imp_right_add", seq
0219: .succedent().getFirst().formula(), fma.sub(1));
0220: ListOfNoPosTacletApp nfapp = goals.head().indexOfTaclets()
0221: .getNoFindTaclet(
0222: new IHTacletFilter(true,
0223: SLListOfRuleSet.EMPTY_LIST), null,
0224: Constraint.BOTTOM);
0225: Term aimpb = TacletForTests.parseTerm("A -> B");
0226: assertTrue("Cut Rule should be inserted to TacletIndex.", nfapp
0227: .size() == 1);
0228: assertTrue(
0229: "Inserted cut rule's b should be instantiated to A -> B.",
0230: nfapp.head().instantiations().getInstantiation(
0231: (SchemaVariable) TacletForTests.getVariables()
0232: .lookup(new Name("b"))).equals(aimpb));
0233: assertTrue("Rule App should be complete", rApp.complete());
0234: goals = nfapp.head().execute(goals.head(),
0235: TacletForTests.services());
0236: Sequent seq1 = goals.head().sequent();
0237: Sequent seq2 = goals.tail().head().sequent();
0238: assertTrue("Preinstantiated cut-rule should be executed", goals
0239: .size() == 2);
0240: assertTrue(
0241: "A->B should be in the succedent of one of the new goals now, "
0242: + "it's in the antecedent, anyway.", seq1
0243: .succedent().getFirst().formula().equals(aimpb)
0244: || seq2.succedent().getFirst().formula()
0245: .equals(aimpb)
0246: || (seq1.succedent().get(1) != null && seq1
0247: .succedent().get(1).formula().equals(
0248: aimpb))
0249: || (seq2.succedent().get(1) != null && seq2
0250: .succedent().get(1).formula().equals(
0251: aimpb)));
0252: }
0253:
0254: public void testSuccTacletAllRight() {
0255: NoPosTacletApp allright = TacletForTests.getRules().lookup(
0256: "all_right");
0257: TacletIndex tacletIndex = new TacletIndex();
0258: tacletIndex.add(allright);
0259: Goal goal = createGoal(proof[1].root(), tacletIndex);
0260: PosInOccurrence applyPos = new PosInOccurrence(goal.sequent()
0261: .succedent().getFirst(), PosInTerm.TOP_LEVEL, false);
0262: ListOfTacletApp rApplist = goal.ruleAppIndex().getTacletAppAt(
0263: TacletFilter.TRUE, applyPos, null, Constraint.BOTTOM);
0264: assertTrue("Too many or zero rule applications.", rApplist
0265: .size() == 1);
0266: RuleApp rApp = rApplist.head();
0267: rApp = ((TacletApp) rApp).tryToInstantiate(goal, TacletForTests
0268: .services());
0269: rApp = ((TacletApp) rApp).createSkolemFunctions(
0270: new Namespace(), TacletForTests.services());
0271: assertTrue("Rule App should be complete", rApp.complete());
0272: ListOfGoal goals = rApp
0273: .execute(goal, TacletForTests.services());
0274: assertTrue("Too many or zero goals for all-right.", goals
0275: .size() == 1);
0276: Sequent seq = goals.head().sequent();
0277: assertEquals("Wrong antecedent after all-right", seq
0278: .antecedent(), Semisequent.EMPTY_SEMISEQUENT);
0279: assertEquals("Wrong succedent after all-right (op mismatch)",
0280: seq.succedent().getFirst().formula().op(),
0281: TacletForTests.getFunctions().lookup(new Name("p")));
0282: }
0283:
0284: public void testTacletWithIf() {
0285: Services services = new Services();
0286: NoPosTacletApp close = TacletForTests.getRules().lookup(
0287: "close_goal");
0288: TacletIndex tacletIndex = new TacletIndex();
0289: tacletIndex.add(close);
0290: Goal goal = createGoal(proof[2].root(), tacletIndex);
0291: PosInOccurrence applyPos = new PosInOccurrence(goal.sequent()
0292: .succedent().getFirst(), PosInTerm.TOP_LEVEL, false);
0293: ListOfTacletApp rApplist = goal.ruleAppIndex().getTacletAppAt(
0294: TacletFilter.TRUE, applyPos, null, Constraint.BOTTOM);
0295: assertTrue("Too many or zero rule applications.\napp list:"
0296: + rApplist, rApplist.size() == 1);
0297:
0298: TacletApp rApp = rApplist.head();
0299: ListOfTacletApp appList = rApp.findIfFormulaInstantiations(goal
0300: .sequent(), services, Constraint.BOTTOM);
0301: assertTrue("Match Failed.",
0302: appList != SLListOfTacletApp.EMPTY_LIST);
0303: assertTrue("Too many matches.", appList.size() == 1);
0304: assertTrue("Wrong match found.", appList.head()
0305: .instantiations() == rApp.instantiations());
0306: assertTrue("Rule App should be complete", appList.head()
0307: .complete());
0308: ListOfGoal goals = appList.head().execute(goal,
0309: TacletForTests.services);
0310: assertTrue("Wrong number of goals for close.",
0311: goals.size() == 1);
0312: proof[2].closeGoal(goals.head(), appList.head().constraint());
0313: assertTrue("Proof should be closed.", proof[2].closed());
0314: /*
0315: ListOfSVInstantiations svilist=rApp.taclet().matchIf(goal.sequent(),
0316: rApp.instantiations(), null);
0317: assertTrue("Match Failed.", svilist!=SLListOfSVInstantiations.EMPTY_LIST);
0318: assertTrue("Too many matches.", svilist.size()==1);
0319: assertTrue("Wrong match found.", svilist.head()==rApp.instantiations());
0320: assertTrue("Rule App should be complete", rApp.complete());
0321: ListOfGoal goals=rApp.execute(goal, TacletForTests.services());
0322: assertTrue("Too many goals for close.", goals.size()==0);
0323: */
0324: }
0325:
0326: public void testAntecTacletWithoutIf() {
0327: Term fma = proof[3].root().sequent().antecedent().getFirst()
0328: .formula();
0329: NoPosTacletApp impleft = TacletForTests.getRules().lookup(
0330: "imp_left");
0331: TacletIndex tacletIndex = new TacletIndex();
0332: tacletIndex.add(impleft);
0333: Goal goal = createGoal(proof[3].root(), tacletIndex);
0334: PosInOccurrence applyPos = new PosInOccurrence(goal.sequent()
0335: .antecedent().getFirst(), PosInTerm.TOP_LEVEL, true);
0336: ListOfTacletApp rApplist = goal.ruleAppIndex().getTacletAppAt(
0337: TacletFilter.TRUE, applyPos, null, Constraint.BOTTOM);
0338: assertTrue("Too many or zero rule applications.", rApplist
0339: .size() == 1);
0340: RuleApp rApp = rApplist.head();
0341: assertTrue("Rule App should be complete", rApp.complete());
0342: ListOfGoal goals = rApp
0343: .execute(goal, TacletForTests.services());
0344: assertTrue("Too many or zero goals for imp-left.",
0345: goals.size() == 2);
0346: Sequent seq = goals.head().sequent();
0347: if (seq.succedent() != Semisequent.EMPTY_SEMISEQUENT) {
0348: assertEquals("Wrong succedent after imp-left", seq
0349: .succedent().getFirst().formula(), fma.sub(0));
0350: goals = goals.tail();
0351: seq = goals.head().node().sequent();
0352: assertEquals("Wrong antecedent after imp-left", seq
0353: .antecedent().getFirst().formula(), fma.sub(1));
0354: } else {
0355: assertEquals("Wrong antecedent after imp-left", seq
0356: .antecedent().getFirst().formula(), fma.sub(1));
0357: goals = goals.tail();
0358: seq = goals.head().node().sequent();
0359:
0360: assertEquals("Wrong succedent after imp-left", seq
0361: .succedent().getFirst().formula(), fma.sub(0));
0362: }
0363: }
0364:
0365: public void testRewriteTacletWithoutIf() {
0366: NoPosTacletApp contradiction = TacletForTests.getRules()
0367: .lookup("TestApplyTaclet_contradiction");
0368: TacletIndex tacletIndex = new TacletIndex();
0369: tacletIndex.add(contradiction);
0370: Goal goal = createGoal(proof[0].root(), tacletIndex);
0371: PosInOccurrence pos = new PosInOccurrence(goal.sequent()
0372: .succedent().getFirst(), PosInTerm.TOP_LEVEL.down(1)
0373: .down(0).down(0), false);
0374: ListOfTacletApp rApplist = goal.ruleAppIndex().getTacletAppAt(
0375: TacletFilter.TRUE, pos, null, Constraint.BOTTOM);
0376:
0377: assertTrue("Too many or zero rule applications.", rApplist
0378: .size() == 1);
0379: RuleApp rApp = rApplist.head();
0380: assertTrue("Rule App should be complete", rApp.complete());
0381: ListOfGoal goals = rApp
0382: .execute(goal, TacletForTests.services());
0383: assertTrue("Too many or zero goals for contradiction.", goals
0384: .size() == 1);
0385: Sequent seq = goals.head().sequent();
0386: Term term = seq.succedent().getFirst().formula().sub(1).sub(0)
0387: .sub(0);
0388: assertTrue(term.equals(TacletForTests.parseTerm("!B -> !A")));
0389: }
0390:
0391: public void testNoFindTacletWithoutIf() {
0392: NoPosTacletApp cut = TacletForTests.getRules().lookup(
0393: "TestApplyTaclet_cut");
0394: TacletIndex tacletIndex = new TacletIndex();
0395: Term t_c = TacletForTests.parseTerm("D");
0396: tacletIndex.add(cut);
0397: Goal goal = createGoal(proof[0].root(), tacletIndex);
0398: PosInOccurrence pos = new PosInOccurrence(goal.sequent()
0399: .succedent().getFirst(), PosInTerm.TOP_LEVEL, false);
0400: ListOfTacletApp rApplist = goal.ruleAppIndex().getTacletAppAt(
0401: TacletFilter.TRUE, pos, null, Constraint.BOTTOM);
0402: assertTrue("Too many or zero rule applications.", rApplist
0403: .size() == 1);
0404: TacletApp rApp = rApplist.head().addInstantiation(
0405: (SchemaVariable) TacletForTests.getVariables().lookup(
0406: new Name("b")), t_c, false);
0407: assertTrue("Rule App should be complete", rApp.complete());
0408: ListOfGoal goals = rApp
0409: .execute(goal, TacletForTests.services());
0410: assertTrue("Too many or too few goals.", goals.size() == 2);
0411: Sequent seq1 = goals.head().sequent();
0412: goals = goals.tail();
0413: Sequent seq2 = goals.head().sequent();
0414: if (seq1.antecedent() != Semisequent.EMPTY_SEMISEQUENT
0415: && seq1.antecedent().getFirst().formula().equals(t_c)) {
0416: assertTrue(
0417: "D is in antecedent of 1st goal but not in succedent of 2nd",
0418: seq2.succedent().getFirst().formula().equals(t_c)
0419: || seq2.succedent().get(1).formula()
0420: .equals(t_c));
0421: } else {
0422: assertTrue("D is not in antecedent and not in succedent "
0423: + "of first new goal", seq1.succedent().getFirst()
0424: .formula().equals(t_c)
0425: || seq1.succedent().get(1).formula().equals(t_c));
0426: assertTrue(
0427: "D is in succedent of first new goal, but not in antecedent "
0428: + "of second new goal", seq2.antecedent()
0429: .getFirst().formula().equals(t_c));
0430: }
0431: }
0432:
0433: /*
0434: public String automaticProof(Sequent initSeq, TacletIndex index){
0435: String out="";
0436: Proof proof=new Proof();
0437: proof.setRoot(new Node(proof, initSeq));
0438: ListOfGoal goals=SLListOfGoal.EMPTY_LIST;
0439: Goal goal=new Goal(proof.root(),new RuleAppIndex(index));
0440: goals=goals.prepend(goal);
0441: while (goals.size()!=0) {
0442: ConstrainedFormula cfma=null;
0443: ConstrainedFormula userCfma=null; // in the real system the
0444: //user would select this
0445: ListOfTacletApp rapplist=SLListOfTacletApp.EMPTY_LIST;
0446: out="\n"+out+("Goals: "+goals+"\n");
0447: goal=goals.head();
0448: IteratorOfConstrainedFormula
0449: it=goal.node().sequent().antecedent().iterator();
0450: while (it.hasNext()) {
0451: userCfma=it.next();
0452: rapplist=rapplist.prepend(goal.ruleAppIndex().
0453: getTacletAppAtAndBelow(TacletFilter.TRUE, new
0454: PosInOccurrence(userCfma, PosInTerm.TOP_LEVEL,
0455: goal.node().sequent())));
0456: }
0457: if (rapplist==SLListOfTacletApp.EMPTY_LIST) {
0458: it=goal.node().sequent().succedent().iterator();
0459: while (it.hasNext()) {
0460: userCfma=it.next();
0461: rapplist=rapplist.prepend(goal.ruleAppIndex()
0462: .getTacletAppAtAndBelow(TacletFilter.TRUE, new
0463: PosInOccurrence(userCfma, PosInTerm.TOP_LEVEL,
0464: goal.node().sequent()))) ;
0465: }
0466: }
0467: out="\n"+out+("GOAL INDEX:"+goal.indexOfTaclets());
0468: out="\n"+out+("Rule apps: "+rapplist);
0469: out="\n"+out+("Choose for if-test: "+rapplist.head()+"\n");
0470: goals=goals.tail();
0471: boolean executed=false;
0472: while (!executed && rapplist!=SLListOfTacletApp.EMPTY_LIST) {
0473: ListOfMapFromSchemaVariableToTerm
0474: mrlist=((Taclet)(rapplist.head().rule())).matchIf(goal.node().sequent(),
0475: rapplist.head().instantiations());
0476: out="\n"+out+("List of if-seq matches:"+mrlist);
0477: if (mrlist!=SLListOfMapFromSchemaVariableToTerm.EMPTY_LIST) {
0478: out+="Execute: "+rapplist.head()+"\n";
0479: goals=goals.prepend(rapplist.head().execute(goal));
0480: executed=true;
0481: }
0482: rapplist=rapplist.tail();
0483: }
0484: out="\n"+out+("Tree: "+proof.root()+"\n *** \n");
0485: if (!executed) {
0486: return out+"\nPROOF FAILED.";
0487: }
0488: }
0489: if (goals.size()==0) out=out+"\nPROOF.";
0490: return out;
0491: }
0492:
0493:
0494: public void testNatAutomatically() {
0495: TacletAppIndex index=new TacletAppIndex(new TacletIndex());
0496: index.addTaclet(TacletForTests.getRules().lookup("close_goal"));
0497: index.addTaclet(TacletForTests.getRules().lookup("imp_left"));
0498: index.addTaclet(TacletForTests.getRules().lookup("imp_right"));
0499: index.addTaclet(TacletForTests.getRules().lookup("not_left"));
0500: index.addTaclet(TacletForTests.getRules().lookup("not_right"));
0501: index.addTaclet(TacletForTests.getRules().lookup
0502: ("TestApplyTaclet_predsuccelim"));
0503: index.addTaclet(pluszeroelim);
0504: index.addTaclet(zeropluselim);
0505: index.addTaclet(succelim);
0506: index.addTaclet(switchsecondsucc);
0507: index.addTaclet(switchfirstsucc);
0508: index.addTaclet(closewitheq);
0509: String s=(automaticProof(seq_testNat, index));
0510: assertTrue("Automatic proof with nats failed",
0511: s.substring(s.length()-6).equals("PROOF."));
0512: }
0513:
0514: */
0515:
0516: public void testIncompleteNoFindTacletApp() {
0517: NoPosTacletApp cut = TacletForTests.getRules().lookup(
0518: "TestApplyTaclet_cut");
0519: assertTrue(
0520: "TacletApp should not be complete, as b is not instantiated",
0521: !cut.complete());
0522: SchemaVariable b = (SchemaVariable) TacletForTests
0523: .getVariables().lookup(new Name("b"));
0524: assertTrue("b should be in the set of not instantiated SVs",
0525: cut.uninstantiatedVars().contains(b));
0526: }
0527:
0528: public void testIncompleteSuccTacletApp() {
0529: TacletApp orright = TacletForTests.getRules()
0530: .lookup("or_right");
0531: assertTrue(
0532: "TacletApp should not be complete, as SVs are not instantiated",
0533: !orright.complete());
0534:
0535: SchemaVariable b = (SchemaVariable) TacletForTests
0536: .getVariables().lookup(new Name("b"));
0537: SchemaVariable c = (SchemaVariable) TacletForTests
0538: .getVariables().lookup(new Name("c"));
0539: assertTrue(
0540: "b and c should be in the set of not instantiated SVs",
0541: orright.uninstantiatedVars().equals(
0542: SetAsListOfSchemaVariable.EMPTY_SET.add(b).add(
0543: c)));
0544: orright = orright.addInstantiation(b, TacletForTests
0545: .parseTerm("A"), false);
0546: assertTrue(
0547: "TacletApp should not be complete, as B is not instantiated",
0548: !orright.complete());
0549: orright = orright.addInstantiation(c, TacletForTests
0550: .parseTerm("B"), false);
0551: assertTrue(
0552: "TacletApp should not be complete, as Position unknown",
0553: !orright.complete());
0554: Sequent seq = proof[0].root().sequent();
0555: orright = orright.setPosInOccurrence(new PosInOccurrence(seq
0556: .succedent().get(0), PosInTerm.TOP_LEVEL, false));
0557: assertTrue(
0558: "TacletApp should now be complete with Position set and SVs "
0559: + "instantiated", orright.complete());
0560: }
0561:
0562: public void testPrgTacletApp() {
0563: NoPosTacletApp wh0 = TacletForTests.getRules().lookup(
0564: "TestApplyTaclet_while0");
0565: SchemaVariable e2 = (SchemaVariable) TacletForTests
0566: .getVariables().lookup(new Name("#e2"));
0567: SchemaVariable p1 = (SchemaVariable) TacletForTests
0568: .getVariables().lookup(new Name("#p1"));
0569: // wh0=wh0.addInstantiation(e2,TacletForTests.parseExpr("boolean", "false"));
0570: // wh0=wh0.addInstantiation(p1,TacletForTests.parsePrg("{if (false){}}"));
0571: Sequent seq = proof[4].root().sequent();
0572: PosInOccurrence pio = new PosInOccurrence(seq.succedent()
0573: .get(0), PosInTerm.TOP_LEVEL, false);
0574: TacletIndex tacletIndex = new TacletIndex();
0575: tacletIndex.add(wh0);
0576: Goal goal = createGoal(proof[4].root(), tacletIndex);
0577: ListOfTacletApp rApplist = goal.ruleAppIndex().getTacletAppAt(
0578: TacletFilter.TRUE, pio, null, Constraint.BOTTOM);
0579:
0580: final TacletApp app = rApplist.head();
0581: assertTrue("#e2 not instantiated", app.instantiations()
0582: .isInstantiated(e2));
0583: assertTrue("#p1 not instantiated", app.instantiations()
0584: .isInstantiated(p1));
0585:
0586: ListOfGoal goals = app.execute(goal, TacletForTests.services);
0587:
0588: assertTrue("Unexpected number of goals", goals.size() == 1);
0589: }
0590:
0591: public void testBugBrokenApply() {
0592: // several times the following bug got broken
0593: // The application of
0594: // 'find (b==>) replacewith(b==>); add (==>b);'
0595: // resulted in
0596: // ==> , b==>b instead of
0597: // b==> , b==>b
0598: NoPosTacletApp cdr = TacletForTests.getRules().lookup(
0599: "TestApplyTaclet_cut_direct_r");
0600:
0601: Sequent seq = proof[1].root().sequent();
0602: PosInOccurrence pio = new PosInOccurrence(seq.succedent()
0603: .get(0), PosInTerm.TOP_LEVEL, false);
0604: TacletIndex tacletIndex = new TacletIndex();
0605: tacletIndex.add(cdr);
0606: Goal goal = createGoal(proof[1].root(), tacletIndex);
0607: ListOfTacletApp rApplist = goal.ruleAppIndex().getTacletAppAt(
0608: TacletFilter.TRUE, pio, null, Constraint.BOTTOM);
0609: ListOfGoal goals = rApplist.head().execute(goal,
0610: TacletForTests.services);
0611:
0612: assertTrue("Expected two goals", goals.size() == 2);
0613: assertTrue("First goal should be 'b==>b', but is "
0614: + goals.head().sequent(), goals.head().sequent()
0615: .antecedent().size() == 1
0616: && goals.head().sequent().antecedent().iterator()
0617: .next().formula().op() == Op.ALL
0618: && goals.head().sequent().succedent().size() == 1
0619: && goals.head().sequent().succedent().iterator().next()
0620: .formula().op() == Op.ALL);
0621: goals = goals.tail();
0622: assertTrue("Second goal should be '==>b', but is "
0623: + goals.head().sequent(), goals.head().sequent()
0624: .antecedent().size() == 0
0625: && goals.head().sequent().succedent().size() == 1
0626: && goals.head().sequent().succedent().iterator().next()
0627: .formula().op() == Op.ALL);
0628:
0629: }
0630:
0631: public void testBugID176() {
0632: // the last time the bug above had been fixed, the hidden
0633: // taclets got broken (did not hide anymore)
0634: // also known as bug #176
0635: NoPosTacletApp hide_r = TacletForTests.getRules().lookup(
0636: "TestApplyTaclet_hide_r");
0637:
0638: Sequent seq = proof[1].root().sequent();
0639: PosInOccurrence pio = new PosInOccurrence(seq.succedent()
0640: .get(0), PosInTerm.TOP_LEVEL, false);
0641: TacletIndex tacletIndex = new TacletIndex();
0642: tacletIndex.add(hide_r);
0643: Goal goal = createGoal(proof[1].root(), tacletIndex);
0644:
0645: ListOfTacletApp rApplist = goal.ruleAppIndex().getTacletAppAt(
0646: TacletFilter.TRUE, pio, null, Constraint.BOTTOM);
0647: ListOfGoal goals = rApplist.head().execute(goal,
0648: TacletForTests.services());
0649:
0650: assertTrue("Expected one goal", goals.size() == 1);
0651: assertTrue("Expected '==>', but is " + goals.head().sequent(),
0652: goals.head().sequent() == Sequent.EMPTY_SEQUENT);
0653:
0654: }
0655:
0656: public void testBugID177() {
0657: // bug #177
0658: NoPosTacletApp al = TacletForTests.getRules()
0659: .lookup("and_left");
0660:
0661: Sequent seq = proof[5].root().sequent();
0662: PosInOccurrence pio = new PosInOccurrence(seq.antecedent().get(
0663: 0), PosInTerm.TOP_LEVEL, true);
0664: TacletIndex tacletIndex = new TacletIndex();
0665: tacletIndex.add(al);
0666: Goal goal = createGoal(proof[5].root(), tacletIndex);
0667:
0668: ListOfTacletApp rApplist = goal.ruleAppIndex().getTacletAppAt(
0669: TacletFilter.TRUE, pio, null, Constraint.BOTTOM);
0670: ListOfGoal goals = rApplist.head().execute(goal,
0671: TacletForTests.services());
0672:
0673: assertTrue("Expected one goal", goals.size() == 1);
0674: IteratorOfConstrainedFormula it = goals.head().sequent()
0675: .antecedent().iterator();
0676: assertTrue("Expected 'A, B ==>', but is "
0677: + goals.head().sequent(), goals.head().sequent()
0678: .antecedent().size() == 2
0679: && it.next().formula().equals(
0680: TacletForTests.parseTerm("A"))
0681: && it.next().formula().equals(
0682: TacletForTests.parseTerm("B")));
0683: }
0684:
0685: public void testBugID188() {
0686: //bug #188
0687:
0688: NoPosTacletApp al = TacletForTests.getRules()
0689: .lookup("and_left");
0690: Sequent seq = proof[7].root().sequent();
0691: PosInOccurrence pio = new PosInOccurrence(seq.antecedent().get(
0692: 0), PosInTerm.TOP_LEVEL, true);
0693:
0694: TacletIndex tacletIndex = new TacletIndex();
0695: tacletIndex.add(al);
0696:
0697: Goal goal = createGoal(proof[7].root(), tacletIndex);
0698:
0699: ListOfTacletApp rApplist = goal.ruleAppIndex().getTacletAppAt(
0700: TacletFilter.TRUE, pio, null, Constraint.BOTTOM);
0701: ListOfGoal goals = rApplist.head().execute(goal,
0702: TacletForTests.services());
0703:
0704: seq = goals.head().sequent();
0705: pio = new PosInOccurrence(seq.antecedent().get(1),
0706: PosInTerm.TOP_LEVEL, true);
0707: tacletIndex = new TacletIndex();
0708: tacletIndex.add(al);
0709:
0710: goal = createGoal(goals.head().node(), tacletIndex);
0711:
0712: rApplist = goal.ruleAppIndex().getTacletAppAt(
0713: TacletFilter.TRUE, pio, null, Constraint.BOTTOM);
0714:
0715: goals = rApplist.head()
0716: .execute(goal, TacletForTests.services());
0717:
0718: assertTrue("Expected one goal", goals.size() == 1);
0719:
0720: IteratorOfConstrainedFormula it = goals.head().sequent()
0721: .antecedent().iterator();
0722:
0723: assertTrue("Expected 'A, B ==>', but is "
0724: + goals.head().sequent(), goals.head().sequent()
0725: .antecedent().size() == 2
0726: && goals.head().sequent().succedent().size() == 0
0727: && it.next().formula().equals(
0728: TacletForTests.parseTerm("A"))
0729: && it.next().formula().equals(
0730: TacletForTests.parseTerm("B")));
0731: }
0732:
0733: public void testConstraintApplication() {
0734: NoPosTacletApp t_al = TacletForTests.getRules().lookup(
0735: "TestApplyTaclet_and_left_alternative");
0736: Sequent seq = mvProof.root().sequent();
0737: PosInOccurrence pio = new PosInOccurrence(seq.antecedent().get(
0738: 0), PosInTerm.TOP_LEVEL, true);
0739: TacletIndex tacletIndex = new TacletIndex();
0740: tacletIndex.add(t_al);
0741:
0742: Goal goal = createGoal(mvProof.root(), tacletIndex);
0743:
0744: ListOfTacletApp rApplist = goal.ruleAppIndex().getTacletAppAt(
0745: TacletFilter.TRUE, pio, null, Constraint.BOTTOM);
0746: RuleApp rApp = rApplist.head();
0747:
0748: rApp = ((TacletApp) rApp).findIfFormulaInstantiations(
0749: goal.sequent(), new Services(), Constraint.BOTTOM)
0750: .head();
0751:
0752: assertTrue("Rule application should be complete.", rApp
0753: .complete());
0754:
0755: ListOfGoal goals = rApp
0756: .execute(goal, TacletForTests.services());
0757: Sequent result = goals.head().sequent();
0758:
0759: assertTrue("Expected one goal", goals.size() == 1);
0760:
0761: ConstrainedFormula antec_1 = new ConstrainedFormula(
0762: TacletForTests.parseTerm("A"), consMV_f_c_X.join(
0763: consMV_f_X_c, null));
0764: assertTrue(antec_1.constraint().isSatisfiable());
0765: Semisequent expected_antec = mvProof.root().sequent()
0766: .antecedent().insertFirst(antec_1).semisequent();
0767: Semisequent expected_succ = mvProof.root().sequent()
0768: .succedent();
0769:
0770: assertTrue(
0771: "Expected 'A<<mv=f_c_X, X=c ==> !(A | B)<<mv=f_X_c', but is "
0772: + result, result.antecedent().equals(
0773: expected_antec)
0774: && result.succedent().equals(expected_succ));
0775: }
0776:
0777: public void testSetTaclets0() {
0778: Services services = TacletForTests.services();
0779: NoPosTacletApp set_isEmpty = TacletForTests.getRules().lookup(
0780: "set_isEmpty");
0781: TacletIndex tacletIndex = new TacletIndex();
0782: tacletIndex.add(set_isEmpty);
0783: NoPosTacletApp set_isEmpty_Size = TacletForTests.getRules()
0784: .lookup("set_isEmpty_Size");
0785: tacletIndex.add(set_isEmpty_Size);
0786: Goal goal = createGoal(proof[6].root(), tacletIndex);
0787: PosInOccurrence pos = new PosInOccurrence(goal.sequent()
0788: .antecedent().getFirst(), PosInTerm.TOP_LEVEL, true);
0789: ListOfTacletApp rApplist = goal.ruleAppIndex().getTacletAppAt(
0790: TacletFilter.TRUE, pos, services, Constraint.BOTTOM);
0791:
0792: assertTrue("Too many or zero rule applications.", rApplist
0793: .size() == 1);
0794: RuleApp rApp = rApplist.head();
0795: SchemaVariable e1 = (SchemaVariable) TacletForTests
0796: .getVariables().lookup(new Name("e1"));
0797: Sort s = TacletForTests.sortLookup("s");
0798: rApp = ((TacletApp) rApp).addInstantiation(e1,
0799: TermFactory.DEFAULT
0800: .createVariableTerm(new LogicVariable(new Name(
0801: "var"), s)), false);
0802: assertTrue("Rule App should be complete", rApp.complete());
0803: // This should apply the taclet set_isEmpty to the formula of the
0804: // antecedent, creating the quantified formula below
0805: ListOfGoal goals = rApp
0806: .execute(goal, TacletForTests.services());
0807: assertTrue("Too many or zero goals.", goals.size() == 1);
0808: Sequent seq = goals.head().sequent();
0809: Term term = seq.antecedent().getFirst().formula();
0810: assertTrue(term.equalsModRenaming(TacletForTests
0811: .parseTerm("\\forall s x; ! s{}::includes(sset,x)")));
0812:
0813: goal = goals.head();
0814: pos = new PosInOccurrence(
0815: goal.sequent().succedent().getFirst(),
0816: PosInTerm.TOP_LEVEL, false);
0817: rApplist = goal.ruleAppIndex().getTacletAppAtAndBelow(
0818: TacletFilter.TRUE, pos, null, Constraint.BOTTOM);
0819: assertTrue("Too many or zero rule applications.", rApplist
0820: .size() == 1);
0821:
0822: rApplist = rApplist.head().findIfFormulaInstantiations(
0823: goal.sequent(), TacletForTests.services(),
0824: Constraint.BOTTOM);
0825: assertTrue("Too many or zero rule applications.", rApplist
0826: .size() == 1);
0827:
0828: rApp = rApplist.head();
0829: assertTrue("Rule App should be complete", rApp.complete());
0830: // This applies the taclet set_isEmpty_size to the formula of the
0831: // succedent, using the quantified formula from above as instantiation
0832: // of the if-formula
0833: goals = rApp.execute(goal, TacletForTests.services());
0834: assertTrue("Too many or zero goals.", goals.size() == 1);
0835: seq = goals.head().sequent();
0836: term = seq.succedent().getFirst().formula();
0837: assertTrue(term.equalsModRenaming(TacletForTests
0838: .parseTerm("0=0")));
0839: }
0840:
0841: public void testModalityLevel0() {
0842: Services services = TacletForTests.services();
0843: NoPosTacletApp apply_eq_nonrigid = TacletForTests.getRules()
0844: .lookup("apply_eq_nonrigid");
0845: TacletIndex tacletIndex = new TacletIndex();
0846: tacletIndex.add(apply_eq_nonrigid);
0847: Goal goal = createGoal(proof[8].root(), tacletIndex);
0848: PosInOccurrence pos = new PosInOccurrence(goal.sequent()
0849: .succedent().getFirst(), PosInTerm.TOP_LEVEL, false);
0850: ListOfTacletApp rApplist = goal.ruleAppIndex()
0851: .getTacletAppAtAndBelow(TacletFilter.TRUE, pos,
0852: services, Constraint.BOTTOM);
0853:
0854: assertTrue("Expected four rule applications.",
0855: rApplist.size() == 4);
0856:
0857: ListOfTacletApp appList = SLListOfTacletApp.EMPTY_LIST;
0858: IteratorOfTacletApp appIt = rApplist.iterator();
0859: while (appIt.hasNext())
0860: appList = appList.prepend(appIt.next()
0861: .findIfFormulaInstantiations(goal.sequent(),
0862: services, Constraint.BOTTOM));
0863:
0864: assertTrue("Expected one match.", appList.size() == 1);
0865: assertTrue("Rule App should be complete", appList.head()
0866: .complete());
0867:
0868: ListOfGoal goals = appList.head().execute(goal,
0869: TacletForTests.services());
0870: assertTrue("Too many or zero goals.", goals.size() == 1);
0871: Sequent seq = goals.head().sequent();
0872: Sequent correctSeq = proof[9].root().sequent();
0873: assertEquals("Wrong result", seq, correctSeq);
0874: }
0875:
0876: public void testModalityLevel1() {
0877: Services services = TacletForTests.services();
0878: NoPosTacletApp apply_eq_nonrigid = TacletForTests.getRules()
0879: .lookup("apply_eq_nonrigid");
0880: TacletIndex tacletIndex = new TacletIndex();
0881: tacletIndex.add(apply_eq_nonrigid);
0882: Goal goal = createGoal(proof[10].root(), tacletIndex);
0883: PosInOccurrence pos = new PosInOccurrence(goal.sequent()
0884: .succedent().getFirst(), PosInTerm.TOP_LEVEL, false);
0885: ListOfTacletApp rApplist = goal.ruleAppIndex()
0886: .getTacletAppAtAndBelow(TacletFilter.TRUE, pos,
0887: services, Constraint.BOTTOM);
0888:
0889: assertTrue("Expected three rule applications.",
0890: rApplist.size() == 3);
0891:
0892: ListOfTacletApp appList = SLListOfTacletApp.EMPTY_LIST;
0893: IteratorOfTacletApp appIt = rApplist.iterator();
0894: while (appIt.hasNext())
0895: appList = appList.prepend(appIt.next()
0896: .findIfFormulaInstantiations(goal.sequent(),
0897: services, Constraint.BOTTOM));
0898:
0899: assertTrue("Did not expect a match.", appList.size() == 0);
0900:
0901: Term ifterm = TacletForTests
0902: .parseTerm("{i:=0}(f(const)=f(f(const)))");
0903: ConstrainedFormula ifformula = new ConstrainedFormula(ifterm,
0904: Constraint.BOTTOM);
0905: ListOfIfFormulaInstantiation ifInsts = SLListOfIfFormulaInstantiation.EMPTY_LIST
0906: .prepend(new IfFormulaInstDirect(ifformula));
0907: appIt = rApplist.iterator();
0908: while (appIt.hasNext()) {
0909: TacletApp a = appIt.next().setIfFormulaInstantiations(
0910: ifInsts, TacletForTests.services(),
0911: Constraint.BOTTOM);
0912: if (a != null)
0913: appList = appList.prepend(a);
0914: }
0915:
0916: assertTrue("Expected one match.", appList.size() == 1);
0917: assertTrue("Rule App should be complete", appList.head()
0918: .complete());
0919:
0920: ListOfGoal goals = appList.head().execute(goal,
0921: TacletForTests.services());
0922: assertTrue("Expected two goals.", goals.size() == 2);
0923:
0924: { // Goal one
0925: Sequent correctSeq = proof[11].root().sequent().addFormula(
0926: ifformula, true, true).sequent();
0927: assertEquals("Wrong result", goals.head().sequent(),
0928: correctSeq);
0929: }
0930:
0931: { // Goal two
0932: Sequent correctSeq = proof[10].root().sequent().addFormula(
0933: ifformula, false, true).sequent();
0934: assertEquals("Wrong result", goals.tail().head().sequent(),
0935: correctSeq);
0936: }
0937: }
0938:
0939: public void testModalityLevel2() {
0940: Services services = TacletForTests.services();
0941: NoPosTacletApp make_insert_eq_nonrigid = TacletForTests
0942: .getRules().lookup("make_insert_eq_nonrigid");
0943: TacletIndex tacletIndex = new TacletIndex();
0944: tacletIndex.add(make_insert_eq_nonrigid);
0945: Goal goal = createGoal(proof[12].root(), tacletIndex);
0946: PosInOccurrence pos = new PosInOccurrence(goal.sequent()
0947: .antecedent().getFirst(), PosInTerm.TOP_LEVEL, true);
0948: ListOfTacletApp rApplist = goal.ruleAppIndex()
0949: .getTacletAppAtAndBelow(TacletFilter.TRUE, pos,
0950: services, Constraint.BOTTOM);
0951:
0952: assertTrue("Expected one rule application.",
0953: rApplist.size() == 1);
0954: assertTrue("Rule App should be complete", rApplist.head()
0955: .complete());
0956:
0957: ListOfGoal goals = rApplist.head().execute(goal,
0958: TacletForTests.services());
0959: assertTrue("Expected one goal.", goals.size() == 1);
0960:
0961: goal = goals.head();
0962:
0963: pos = new PosInOccurrence(
0964: goal.sequent().succedent().getFirst(),
0965: PosInTerm.TOP_LEVEL, false);
0966: rApplist = goal.ruleAppIndex().getTacletAppAtAndBelow(
0967: TacletFilter.TRUE, pos, services, Constraint.BOTTOM);
0968:
0969: assertTrue("Expected one rule application.",
0970: rApplist.size() == 1);
0971: assertTrue("Rule App should be complete", rApplist.head()
0972: .complete());
0973:
0974: goals = rApplist.head()
0975: .execute(goal, TacletForTests.services());
0976: assertTrue("Expected one goal.", goals.size() == 1);
0977:
0978: Sequent seq = goals.head().sequent();
0979: Sequent correctSeq = proof[13].root().sequent();
0980: assertEquals("Wrong result", seq, correctSeq);
0981: }
0982:
0983: public void testBugEmptyBlock() {
0984: NoPosTacletApp testApplyTaclet_wrap_blocks_two_empty_lists = TacletForTests
0985: .getRules().lookup(
0986: "TestApplyTaclet_wrap_blocks_two_empty_lists");
0987: TacletIndex tacletIndex = new TacletIndex();
0988: tacletIndex.add(testApplyTaclet_wrap_blocks_two_empty_lists);
0989: Goal goal = createGoal(proof[14].root(), tacletIndex);
0990: PosInOccurrence pos = new PosInOccurrence(goal.sequent()
0991: .succedent().getFirst(), PosInTerm.TOP_LEVEL, false);
0992:
0993: ListOfTacletApp rApplist = goal.ruleAppIndex()
0994: .getTacletAppAtAndBelow(TacletFilter.TRUE, pos, null,
0995: Constraint.BOTTOM);
0996:
0997: assertTrue("Expected one rule application.",
0998: rApplist.size() == 1);
0999: assertTrue("Rule App should be complete", rApplist.head()
1000: .complete());
1001:
1002: // the bug was: the next method throws the exception
1003: // java.util.NoSuchElementException
1004: ListOfGoal goals = rApplist.head().execute(goal,
1005: TacletForTests.services());
1006:
1007: assertTrue("Expected one goal.", goals.size() == 1);
1008:
1009: Sequent correctSeq = proof[15].root().sequent();
1010: assertEquals("Wrong result", goals.head().sequent(), correctSeq);
1011: }
1012:
1013: public void testCatchList() {
1014: doTestCatchList(16);
1015: doTestCatchList(18);
1016: doTestCatchList(20);
1017: }
1018:
1019: private void doTestCatchList(int p_proof) {
1020: NoPosTacletApp test_catch_list0 = TacletForTests.getRules()
1021: .lookup("test_catch_list0");
1022: NoPosTacletApp test_catch_list1 = TacletForTests.getRules()
1023: .lookup("test_catch_list1");
1024: TacletIndex tacletIndex = new TacletIndex();
1025: tacletIndex.add(test_catch_list0);
1026: tacletIndex.add(test_catch_list1);
1027: Goal goal = createGoal(proof[p_proof].root(), tacletIndex);
1028: PosInOccurrence pos = new PosInOccurrence(goal.sequent()
1029: .succedent().getFirst(), PosInTerm.TOP_LEVEL, false);
1030:
1031: ListOfTacletApp rApplist = goal.ruleAppIndex()
1032: .getTacletAppAtAndBelow(TacletFilter.TRUE, pos, null,
1033: Constraint.BOTTOM);
1034:
1035: assertTrue("Expected one rule application.",
1036: rApplist.size() == 1);
1037: assertTrue("Rule App should be complete.", rApplist.head()
1038: .complete());
1039:
1040: ListOfGoal goals = rApplist.head().execute(goal,
1041: TacletForTests.services());
1042:
1043: assertTrue("Expected one goal.", goals.size() == 1);
1044:
1045: Sequent correctSeq = proof[p_proof + 1].root().sequent();
1046:
1047: Term resultFormula = goals.head().sequent().getFormulabyNr(1)
1048: .formula();
1049: Term correctFormula = correctSeq.getFormulabyNr(1).formula();
1050:
1051: assertTrue("Wrong result", resultFormula
1052: .equalsModRenaming(correctFormula));
1053: }
1054:
1055: private Goal createGoal(Node n, TacletIndex tacletIndex) {
1056: final BuiltInRuleAppIndex birIndex = new BuiltInRuleAppIndex(
1057: new BuiltInRuleIndex());
1058: final RuleAppIndex ruleAppIndex = new RuleAppIndex(tacletIndex,
1059: birIndex);
1060: final Goal goal = new Goal(n, ruleAppIndex);
1061: return goal;
1062: }
1063:
1064: public void testShadowedUpdateLocation() {
1065: NoPosTacletApp shadowed_update = TacletForTests.getRules()
1066: .lookup("test_shadowed_update_location");
1067: TacletIndex tacletIndex = new TacletIndex();
1068: tacletIndex.add(shadowed_update);
1069: Goal goal = createGoal(proof[0].root(), tacletIndex);
1070: ListOfNoPosTacletApp rApplist = goal.ruleAppIndex()
1071: .getNoFindTaclet(TacletFilter.TRUE, null,
1072: Constraint.BOTTOM);
1073: assertTrue("Too many or zero rule applications.", rApplist
1074: .size() == 1);
1075: RuleApp rApp = rApplist.head();
1076: assertTrue("Rule App should be complete", rApp.complete());
1077:
1078: ListOfGoal goals = rApp
1079: .execute(goal, TacletForTests.services());
1080: assertTrue(
1081: "Too many or zero goals for test_shadowed_update_location.",
1082: goals.size() == 1);
1083: }
1084:
1085: /**
1086: * tests if the variable sv collector pays attention to schema variables
1087: * occuring as part of attributes and/or updates (there was a bug where
1088: * this has been forgotten, and as a result after applying a method contract
1089: * schemavariables have been introduces into a goal sequent)
1090: *
1091: */
1092: public void testTacletVariableCollector() {
1093: TacletSchemaVariableCollector coll = new TacletSchemaVariableCollector();
1094: Taclet t = TacletForTests.getRules().lookup(
1095: "testUninstantiatedSVCollector").taclet();
1096: coll.visit(t, false);
1097: SetOfSchemaVariable collSet = SetAsListOfSchemaVariable.EMPTY_SET;
1098: IteratorOfSchemaVariable it = coll.varIterator();
1099: while (it.hasNext()) {
1100: collSet = collSet.add(it.next());
1101: }
1102:
1103: assertTrue("Expected four uninstantiated variables in taclet "
1104: + t + ", but found " + collSet.size(),
1105: collSet.size() == 4);
1106: }
1107:
1108: /**
1109: * tests a bug, which causedthe first statement in a context block to be discarded
1110: * in cases where the complete program has been matched by the prefix and suffix of the context
1111: * block i.e.
1112: * a rule like
1113: * <code>
1114: * \find ( <.. ...>\forall u; post )
1115: * \replacewith (\forall u;<.. ..>post)
1116: * </code>
1117: * applied on
1118: * <code> < method-frame():{ while (...) {...} } >\forall int i; i>0</code>
1119: * created the goal
1120: * <code> \forall int i;< method-frame():{ } >i>0 </code>
1121: * which is of course incorrect.
1122: */
1123:
1124: public void testCompleteContextAddBug() {
1125: NoPosTacletApp app = TacletForTests.getRules().lookup(
1126: "TestApplyTaclet_allPullOutBehindDiamond");
1127:
1128: TacletIndex tacletIndex = new TacletIndex();
1129: tacletIndex.add(app);
1130: Goal goal = createGoal(proof[22].root(), tacletIndex);
1131: PosInOccurrence pos = new PosInOccurrence(goal.sequent()
1132: .succedent().getFirst(), PosInTerm.TOP_LEVEL, false);
1133:
1134: ListOfTacletApp rApplist = goal.ruleAppIndex()
1135: .getTacletAppAtAndBelow(TacletFilter.TRUE, pos, null,
1136: Constraint.BOTTOM);
1137:
1138: assertTrue("Expected one rule application.",
1139: rApplist.size() == 1);
1140: assertTrue("Rule App should be complete", rApplist.head()
1141: .complete());
1142:
1143: ListOfGoal goals = rApplist.head().execute(goal,
1144: TacletForTests.services());
1145:
1146: assertTrue("Expected one goal.", goals.size() == 1);
1147:
1148: // the content of the diamond must not have changed
1149: ProgramElement expected = proof[22].root().sequent()
1150: .getFormulabyNr(1).formula().javaBlock().program();
1151: ProgramElement is = goals.head().sequent().getFormulabyNr(1)
1152: .formula().sub(0).javaBlock().program();
1153: assertEquals("Context has been thrown away.", expected, is);
1154:
1155: }
1156:
1157: /**
1158: *
1159: */
1160: public void testContextAdding() {
1161: NoPosTacletApp app = TacletForTests.getRules().lookup(
1162: "TestApplyTaclet_addEmptyStatement");
1163:
1164: TacletIndex tacletIndex = new TacletIndex();
1165: tacletIndex.add(app);
1166: Goal goal = createGoal(proof[22].root(), tacletIndex);
1167: PosInOccurrence pos = new PosInOccurrence(goal.sequent()
1168: .succedent().getFirst(), PosInTerm.TOP_LEVEL, false);
1169:
1170: ListOfTacletApp rApplist = goal.ruleAppIndex()
1171: .getTacletAppAtAndBelow(TacletFilter.TRUE, pos, null,
1172: Constraint.BOTTOM);
1173:
1174: assertTrue("Expected one rule application.",
1175: rApplist.size() == 1);
1176: assertTrue("Rule App should be complete", rApplist.head()
1177: .complete());
1178:
1179: ListOfGoal goals = rApplist.head().execute(goal,
1180: TacletForTests.services());
1181:
1182: assertTrue("Expected one goal.", goals.size() == 1);
1183:
1184: // the content of the diamond must not have changed
1185: ProgramElement expected = TacletForTests
1186: .parsePrg("{try{ ; while (1==1) {if (1==2) {break;}} return 1==3; "
1187: + "int i=17; } catch (Exception e) { return null;}}");
1188:
1189: ProgramElement is = goals.head().sequent().getFormulabyNr(1)
1190: .formula().javaBlock().program();
1191: assertTrue("Expected:" + expected + "\n but was:" + is,
1192: expected.equalsModRenaming(is,
1193: new NameAbstractionTable()));
1194: }
1195:
1196: /**
1197: * this test is different from the other empty block removal test
1198: */
1199: public void testRemoveEmptyBlock() {
1200: NoPosTacletApp app = TacletForTests.getRules().lookup(
1201: "TestApplyTaclet_removeEmptyBlock");
1202:
1203: TacletIndex tacletIndex = new TacletIndex();
1204: tacletIndex.add(app);
1205: Goal goal = createGoal(proof[23].root(), tacletIndex);
1206: PosInOccurrence pos = new PosInOccurrence(goal.sequent()
1207: .succedent().getFirst(), PosInTerm.TOP_LEVEL, false);
1208:
1209: ListOfTacletApp rApplist = goal.ruleAppIndex()
1210: .getTacletAppAtAndBelow(TacletFilter.TRUE, pos, null,
1211: Constraint.BOTTOM);
1212:
1213: assertTrue("Expected one rule application.",
1214: rApplist.size() == 1);
1215: assertTrue("Rule App should be complete", rApplist.head()
1216: .complete());
1217:
1218: ListOfGoal goals = rApplist.head().execute(goal,
1219: TacletForTests.services());
1220:
1221: assertTrue("Expected one goal.", goals.size() == 1);
1222:
1223: // the content of the diamond must not have changed
1224: ProgramElement expected = TacletForTests
1225: .parsePrg("{try{while (1==1) {if (1==2) {break;}} return 1==3; "
1226: + "int i=17; } catch (Exception e) { return null;}}");
1227:
1228: ProgramElement is = goals.head().sequent().getFormulabyNr(1)
1229: .formula().javaBlock().program();
1230: assertTrue("Expected:" + expected + "\n but was:" + is,
1231: expected.equalsModRenaming(is,
1232: new NameAbstractionTable()));
1233: }
1234:
1235: }
|