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: /**
012: * tests if match checks the variable conditions in Taclets.
013: */package de.uka.ilkd.key.rule;
014:
015: import java.util.HashSet;
016:
017: import junit.framework.TestCase;
018: import de.uka.ilkd.key.java.Services;
019: import de.uka.ilkd.key.logic.*;
020: import de.uka.ilkd.key.logic.op.*;
021: import de.uka.ilkd.key.logic.sort.Sort;
022: import de.uka.ilkd.key.proof.*;
023: import de.uka.ilkd.key.util.Debug;
024:
025: public class TestSchemaModalOperators extends TestCase {
026:
027: String[] strs = { "i=5", "\\<{ while(i>0) {i--;} }\\> i=0", "i=3",
028: "\\[{ if(i==3) {i++;} else {i--;} }\\] i=3", "i=3",
029: "\\[[{ if(i==3) {i++;} else {i--;} }\\]] i=3" };
030: Proof[] proof;
031: Proof mvProof;
032: // mv=f(X,c)
033: Constraint consMV_f_X_c;
034: // mv=f(c,X)
035: Constraint consMV_f_c_X;
036:
037: private static Semisequent parseTermForSemisequent(String t) {
038: if ("".equals(t)) {
039: return Semisequent.EMPTY_SEMISEQUENT;
040: }
041: ConstrainedFormula cf0 = new ConstrainedFormula(TacletForTests
042: .parseTerm(t));
043: return Semisequent.EMPTY_SEMISEQUENT.insert(0, cf0)
044: .semisequent();
045: }
046:
047: public void setUp() {
048: TacletForTests.setStandardFile(TacletForTests.testRules);
049: TacletForTests.parse();
050: UpdateSimplifier sus = new UpdateSimplifier();
051: proof = new Proof[strs.length / 2];
052: for (int i = 0; i < proof.length; i++) {
053: Semisequent antec = parseTermForSemisequent(strs[2 * i]);
054: Semisequent succ = parseTermForSemisequent(strs[2 * i + 1]);
055: Sequent s = Sequent.createSequent(antec, succ);
056: proof[i] = new Proof(new Services());
057: proof[i].setSimplifier(sus);
058: proof[i].setRoot(new Node(proof[i], s));
059: }
060:
061: // proof required to test application with mv
062: /*
063: TermFactory tf=TermFactory.DEFAULT;
064:
065: mvProof = new Proof();
066:
067: mvProof.setSimplifier(sus);
068:
069: Sort s = new PrimitiveSort(new Name("test"));
070:
071: Function f = new Function(new Name("f"), s, new Sort[]{s, s});
072: Function c = new Function(new Name("c"), s, new Sort[]{});
073:
074: Metavariable mv_x = new Metavariable(new Name("X"), s);
075: Metavariable mv_y = new Metavariable(new Name("Y"), s);
076: Metavariable mv = new Metavariable(new Name("mv"), s);
077:
078: Term t_mv = tf.createFunctionTerm(mv, new Term[]{});
079: Term t_mv_x = tf.createFunctionTerm(mv_x, new Term[]{});
080: Term t_mv_y = tf.createFunctionTerm(mv_y, new Term[]{});
081:
082: Term t_c = tf.createFunctionTerm(c, new Term[]{});
083: Term t_f_X_c = tf.createFunctionTerm(f, new Term[]{t_mv_x, t_c});
084: Term t_f_c_X = tf.createFunctionTerm(f, new Term[]{t_c, t_mv_x});
085:
086: consMV_f_c_X = Constraint.BOTTOM.unify(t_mv, t_f_c_X);
087: consMV_f_X_c = Constraint.BOTTOM.unify(t_mv, t_f_X_c);
088:
089: ConstrainedFormula cf1 =
090: new ConstrainedFormula(TacletForTests.parseTerm("A & B"), consMV_f_c_X);
091: ConstrainedFormula cf2 =
092: new ConstrainedFormula(TacletForTests.parseTerm("!(A | B)"), consMV_f_X_c);
093:
094: Sequent seq = Sequent.createSequent
095: (Semisequent.EMPTY_SEMISEQUENT.insertLast(cf1).semisequent(),
096: Semisequent.EMPTY_SEMISEQUENT.insertLast(cf2).semisequent());
097:
098: mvProof.setRoot(new Node(mvProof, seq));
099: */
100: }
101:
102: public void tearDown() {
103: proof = null;
104: }
105:
106: public TestSchemaModalOperators(String name) {
107: super (name);
108: // Debug.ENABLE_DEBUG = true;
109: }
110:
111: public void testSchemaModalities1() {
112: // Debug.ENABLE_DEBUG = true;
113:
114: RewriteTacletBuilder rtb = new RewriteTacletBuilder();
115: TermFactory tf = TermFactory.DEFAULT;
116:
117: SchemaVariable fsv = SchemaVariableFactory.createFormulaSV(
118: new Name("post"), false, true);
119: HashSet modalities = new HashSet(2);
120: modalities.add(Op.DIA);
121: modalities.add(Op.BOX);
122: SchemaVariable osv = SchemaVariableFactory.createOperatorSV(
123: new Name("diabox"), Modality.class, Sort.FORMULA, 1,
124: modalities);
125: Term tpost = tf.createFunctionTerm((SortedSchemaVariable) fsv,
126: new Term[0]);
127:
128: Term find = tf.createProgramTerm(osv,
129: JavaBlock.EMPTY_JAVABLOCK, new Term[] { tpost });
130:
131: Term replace = tf.createProgramTerm(osv,
132: JavaBlock.EMPTY_JAVABLOCK, new Term[] { tf
133: .createJunctorTerm(Op.TRUE) });
134:
135: rtb.setName(new Name("test_schema_modal1"));
136: rtb.setFind(find);
137: rtb.addTacletGoalTemplate(new RewriteTacletGoalTemplate(
138: Sequent.EMPTY_SEQUENT, SLListOfTaclet.EMPTY_LIST,
139: replace));
140:
141: RewriteTaclet t = rtb.getRewriteTaclet();
142:
143: Term goal = tf.createProgramTerm(Op.DIA,
144: JavaBlock.EMPTY_JAVABLOCK, tf
145: .createJunctorTerm(Op.FALSE));
146:
147: MatchConditions mc = (t.match(goal, find,
148: MatchConditions.EMPTY_MATCHCONDITIONS, null,
149: Constraint.BOTTOM));
150: assertNotNull(mc);
151: assertNotNull(mc.getInstantiations().getInstantiation(osv));
152: Debug.out("Match conditions: ", mc.getInstantiations());
153: Debug.out("Find: ", find);
154: Debug.out("Replace: ", replace);
155: Debug.out("Goal: ", goal);
156: Term instreplace = t.syntacticalReplace(replace, null, mc);
157: Term instfind = t.syntacticalReplace(replace, null, mc);
158: Debug.out("Instantiated replace: ", instreplace);
159: Debug.out("Instantiated find: ", instfind);
160: // Debug.ENABLE_DEBUG = false;
161:
162: }
163:
164: public void testSchemaModalities2() {
165: // Debug.ENABLE_DEBUG = true;
166: NoPosTacletApp testmodal1 = TacletForTests.getRules().lookup(
167: "testSchemaModal1");
168: TacletIndex tacletIndex = new TacletIndex();
169: tacletIndex.add(testmodal1);
170: Goal goal = createGoal(proof[0].root(), tacletIndex);
171: PosInOccurrence applyPos = new PosInOccurrence(goal.sequent()
172: .succedent().getFirst(), PosInTerm.TOP_LEVEL, false);
173: ListOfTacletApp rApplist = goal.ruleAppIndex().getTacletAppAt(
174: TacletFilter.TRUE, applyPos, null, Constraint.BOTTOM);
175: assertTrue("Too many or zero rule applications.", rApplist
176: .size() == 1);
177: RuleApp rApp = rApplist.head();
178: assertTrue("Rule App should be complete", rApp.complete());
179: ListOfGoal goals = rApp
180: .execute(goal, TacletForTests.services());
181: assertTrue(
182: "There should be 1 goal for testSchemaModal1 taclet, was "
183: + goals.size(), goals.size() == 1);
184: Sequent seq = goals.head().sequent();
185: Semisequent antec0 = parseTermForSemisequent("\\<{ i--; }\\> i=0");
186: Semisequent antec1 = parseTermForSemisequent("i=5");
187: Semisequent succ = parseTermForSemisequent("\\<{ i--; while(i>0) {i--;} }\\> i=0");
188:
189: assertEquals("Wrong antecedent after testSchemaModal1", seq
190: .antecedent().get(0), antec0.get(0));
191: assertEquals("Wrong antecedent after testSchemaModal1", seq
192: .antecedent().get(1), antec1.get(0));
193: assertEquals("Wrong succedent after testSchemaModal1", seq
194: .succedent().getFirst(), succ.get(0));
195:
196: // Debug.ENABLE_DEBUG = false;
197:
198: }
199:
200: public void testSchemaModalities3() {
201: // Debug.ENABLE_DEBUG = true;
202: NoPosTacletApp testmodal2 = TacletForTests.getRules().lookup(
203: "testSchemaModal2");
204: TacletIndex tacletIndex = new TacletIndex();
205: tacletIndex.add(testmodal2);
206: Goal goal = createGoal(proof[1].root(), tacletIndex);
207: PosInOccurrence applyPos = new PosInOccurrence(goal.sequent()
208: .succedent().getFirst(), PosInTerm.TOP_LEVEL, false);
209: ListOfTacletApp rApplist = goal.ruleAppIndex().getTacletAppAt(
210: TacletFilter.TRUE, applyPos, null, Constraint.BOTTOM);
211: assertTrue("Too many or zero rule applications.", rApplist
212: .size() == 1);
213: RuleApp rApp = rApplist.head();
214: assertTrue("Rule App should be complete", rApp.complete());
215: ListOfGoal goals = rApp
216: .execute(goal, TacletForTests.services());
217: assertTrue(
218: "There should be 1 goal for testSchemaModal2 taclet, was "
219: + goals.size(), goals.size() == 1);
220: Sequent seq = goals.head().sequent();
221: Semisequent antec0 = parseTermForSemisequent("i=3");
222: Semisequent succ = parseTermForSemisequent("\\[{ i++; i--; }\\] i=3");
223:
224: assertEquals("Wrong antecedent after testSchemaModal2", seq
225: .antecedent().get(0), antec0.get(0));
226: assertEquals("Wrong succedent after testSchemaModal2", seq
227: .succedent().getFirst(), succ.get(0));
228:
229: // Debug.ENABLE_DEBUG = false;
230:
231: }
232:
233: public void testSchemaModalities4() {
234: // Debug.ENABLE_DEBUG = true;
235: NoPosTacletApp testmodal3 = TacletForTests.getRules().lookup(
236: "testSchemaModal3");
237: TacletIndex tacletIndex = new TacletIndex();
238: tacletIndex.add(testmodal3);
239: Goal goal = createGoal(proof[1].root(), tacletIndex);
240: PosInOccurrence applyPos = new PosInOccurrence(goal.sequent()
241: .succedent().getFirst(), PosInTerm.TOP_LEVEL, false);
242: ListOfTacletApp rApplist = goal.ruleAppIndex().getTacletAppAt(
243: TacletFilter.TRUE, applyPos, null, Constraint.BOTTOM);
244: assertTrue("Too many or zero rule applications.", rApplist
245: .size() == 1);
246: RuleApp rApp = rApplist.head();
247: assertTrue("Rule App should be complete", rApp.complete());
248: ListOfGoal goals = rApp
249: .execute(goal, TacletForTests.services());
250: assertTrue(
251: "There should be 3 goals for testSchemaModal3 taclet, was "
252: + goals.size(), goals.size() == 3);
253: Sequent seq0 = goals.head().sequent();
254: goals = goals.tail();
255: Sequent seq1 = goals.head().sequent();
256: goals = goals.tail();
257: Sequent seq2 = goals.head().sequent();
258: Semisequent antec0 = parseTermForSemisequent("i=3");
259: Semisequent succ0 = parseTermForSemisequent("\\[{ if(i==3) {i++;} else {i--;} }\\] i=3");
260: Semisequent succ1 = parseTermForSemisequent("\\<{ if(i==3) {i++;} else {i--;} }\\> i=3");
261: Semisequent succ2 = parseTermForSemisequent("\\[{ if(i==3) {i++;} else {i--;} }\\] i=3");
262:
263: assertEquals("Wrong antecedent after testSchemaModal3", seq0
264: .antecedent().get(0), antec0.get(0));
265: assertEquals("Wrong antecedent after testSchemaModal3", seq1
266: .antecedent().get(0), antec0.get(0));
267: assertEquals("Wrong antecedent after testSchemaModal3", seq2
268: .antecedent().get(0), antec0.get(0));
269: assertEquals("Wrong succedent after testSchemaModal3", seq0
270: .succedent().getFirst(), succ0.get(0));
271: assertEquals("Wrong succedent after testSchemaModal3", seq1
272: .succedent().getFirst(), succ1.get(0));
273: assertEquals("Wrong succedent after testSchemaModal3", seq2
274: .succedent().getFirst(), succ2.get(0));
275:
276: // Debug.ENABLE_DEBUG = false;
277:
278: }
279:
280: public void testSchemaModalities5() {
281: // Debug.ENABLE_DEBUG = true;
282: NoPosTacletApp testmodal4 = TacletForTests.getRules().lookup(
283: "testSchemaModal4");
284: TacletIndex tacletIndex = new TacletIndex();
285: tacletIndex.add(testmodal4);
286: Goal goal = createGoal(proof[2].root(), tacletIndex);
287: PosInOccurrence applyPos = new PosInOccurrence(goal.sequent()
288: .succedent().getFirst(), PosInTerm.TOP_LEVEL, false);
289: ListOfTacletApp rApplist = goal.ruleAppIndex().getTacletAppAt(
290: TacletFilter.TRUE, applyPos, null, Constraint.BOTTOM);
291: assertTrue("Too many or zero rule applications.", rApplist
292: .size() == 1);
293: RuleApp rApp = rApplist.head();
294: assertTrue("Rule App should be complete", rApp.complete());
295: ListOfGoal goals = rApp
296: .execute(goal, TacletForTests.services());
297: assertTrue(
298: "There should be 3 goals for testSchemaModal4 taclet, was "
299: + goals.size(), goals.size() == 3);
300: Sequent seq0 = goals.head().sequent();
301: goals = goals.tail();
302: Sequent seq1 = goals.head().sequent();
303: goals = goals.tail();
304: Sequent seq2 = goals.head().sequent();
305: Semisequent antec0 = parseTermForSemisequent("i=3");
306: Semisequent succ0 = parseTermForSemisequent("\\throughout_trc{ if(i==3) {i++;} else {i--;} }\\endmodality(i=3)");
307: Semisequent succ1 = parseTermForSemisequent("\\throughout_tra{ if(i==3) {i++;} else {i--;} }\\endmodality(i=3)");
308: Semisequent succ2 = parseTermForSemisequent("\\throughout{ if(i==3) {i++;} else {i--;} }\\endmodality(i=3)");
309:
310: assertEquals("Wrong antecedent after testSchemaModal4", seq0
311: .antecedent().get(0), antec0.get(0));
312: assertEquals("Wrong antecedent after testSchemaModal4", seq1
313: .antecedent().get(0), antec0.get(0));
314: assertEquals("Wrong antecedent after testSchemaModal4", seq2
315: .antecedent().get(0), antec0.get(0));
316: assertEquals("Wrong succedent after testSchemaModal4", seq0
317: .succedent().getFirst(), succ0.get(0));
318: assertEquals("Wrong succedent after testSchemaModal4", seq1
319: .succedent().getFirst(), succ1.get(0));
320: assertEquals("Wrong succedent after testSchemaModal4", seq2
321: .succedent().getFirst(), succ2.get(0));
322:
323: // Debug.ENABLE_DEBUG = false;
324:
325: }
326:
327: private Goal createGoal(Node n, TacletIndex tacletIndex) {
328: final BuiltInRuleAppIndex birIndex = new BuiltInRuleAppIndex(
329: new BuiltInRuleIndex());
330: final RuleAppIndex ruleAppIndex = new RuleAppIndex(tacletIndex,
331: birIndex);
332: final Goal goal = new Goal(n, ruleAppIndex);
333: return goal;
334: }
335:
336: }
|