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 junit.framework.TestCase;
016: import de.uka.ilkd.key.java.ArrayOfProgramElement;
017: import de.uka.ilkd.key.java.Services;
018: import de.uka.ilkd.key.java.StatementBlock;
019: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
020: import de.uka.ilkd.key.java.abstraction.PrimitiveType;
021: import de.uka.ilkd.key.java.reference.ExecutionContext;
022: import de.uka.ilkd.key.java.reference.TypeRef;
023: import de.uka.ilkd.key.java.statement.MethodFrame;
024: import de.uka.ilkd.key.logic.*;
025: import de.uka.ilkd.key.logic.op.*;
026: import de.uka.ilkd.key.logic.sort.ClassInstanceSortImpl;
027: import de.uka.ilkd.key.logic.sort.PrimitiveSort;
028: import de.uka.ilkd.key.logic.sort.SetAsListOfSort;
029: import de.uka.ilkd.key.logic.sort.Sort;
030: import de.uka.ilkd.key.proof.IHTacletFilter;
031: import de.uka.ilkd.key.proof.TacletIndex;
032: import de.uka.ilkd.key.util.Debug;
033:
034: public class TestMatchTaclet extends TestCase {
035: FindTaclet if_addrule_conflict;
036: FindTaclet find_addrule_conflict;
037: FindTaclet if_find_clash;
038: FindTaclet if_add_no_clash;
039: FindTaclet not_free_conflict;
040: FindTaclet all_left;
041: FindTaclet assign_n;
042: TacletApp close_rule;
043: Term matchExc;
044: Taclet[] conflict;
045: Services services;
046:
047: public TestMatchTaclet(String name) {
048: super (name);
049: }
050:
051: public TestMatchTaclet(String name, boolean b) {
052: super (name);
053: Debug.ENABLE_DEBUG = b;
054: }
055:
056: public void setUp() {
057: TacletForTests.setStandardFile(System.getProperty("key.home")
058: + java.io.File.separator + "system"
059: + java.io.File.separator
060: + "de/uka/ilkd/key/logic/testRuleMatch.txt");
061: TacletForTests.parse();
062:
063: services = TacletForTests.services();
064:
065: all_left = (FindTaclet) TacletForTests.getTaclet(
066: "TestMatchTaclet_for_all").taclet();
067: if_addrule_conflict = (FindTaclet) TacletForTests.getTaclet(
068: "if_addrule_clash").taclet();
069:
070: find_addrule_conflict = (FindTaclet) TacletForTests.getTaclet(
071: "find_addrule_clash").taclet();
072:
073: if_find_clash = (FindTaclet) TacletForTests.getTaclet(
074: "if_find_clash").taclet();
075:
076: if_add_no_clash = (FindTaclet) TacletForTests.getTaclet(
077: "if_add_no_clash").taclet();
078:
079: not_free_conflict = (FindTaclet) TacletForTests.getTaclet(
080: "not_free_conflict").taclet();
081: close_rule = TacletForTests.getTaclet("close_rule");
082:
083: conflict = new Taclet[4];
084: conflict[0] = (FindTaclet) TacletForTests.getTaclet(
085: "test_rule_one").taclet();
086: conflict[1] = (FindTaclet) TacletForTests.getTaclet(
087: "test_rule_two").taclet();
088: conflict[2] = (FindTaclet) TacletForTests.getTaclet(
089: "test_rule_three").taclet();
090: conflict[3] = (FindTaclet) TacletForTests.getTaclet(
091: "test_rule_four").taclet();
092:
093: assign_n = (FindTaclet) TacletForTests.getTaclet(
094: "TestMatchTaclet_assign_n").taclet();
095:
096: }
097:
098: public void tearDown() {
099: if_addrule_conflict = null;
100: find_addrule_conflict = null;
101: if_find_clash = null;
102: if_add_no_clash = null;
103: not_free_conflict = null;
104: all_left = null;
105: assign_n = null;
106: close_rule = null;
107: matchExc = null;
108: conflict = null;
109: services = null;
110: }
111:
112: public void testStatementListMatch() {
113: Term match = TacletForTests
114: .parseTerm("\\<{ l1:{l2:{while (true) {break; "
115: + "int k=1; {int j = 1; j++;} int c = 56;}}} }\\> true");
116:
117: FindTaclet break_while = (FindTaclet) TacletForTests.getTaclet(
118: "TestMatchTaclet_break_while").taclet();
119:
120: MatchConditions svi = break_while.matchJavaBlock(match,
121: (Term) break_while.find(),
122: MatchConditions.EMPTY_MATCHCONDITIONS, services);
123:
124: assertNotNull("Matches have been expected.", svi);
125:
126: SchemaVariable sv = TacletForTests.svLookup("#stmnt_list");
127: assertTrue("Expected list of statement to be instantiated.",
128: svi.getInstantiations().isInstantiated(sv));
129: assertTrue(
130: "The three statements behind the break should be matched.",
131: ((ArrayOfProgramElement) svi.getInstantiations()
132: .getInstantiation(sv)).size() == 3);
133: }
134:
135: public void testProgramMatch0() {
136: Term match = TacletForTests
137: .parseTerm("\\<{ l1:{l2:{while (true) {break;} "
138: + "int k=1;}} }\\> true");
139: FindTaclet taclet = (FindTaclet) TacletForTests.getTaclet(
140: "TestMatchTaclet_whileright").taclet();
141: MatchConditions svi = taclet.matchJavaBlock(match,
142: (Term) taclet.find(),
143: MatchConditions.EMPTY_MATCHCONDITIONS, services);
144:
145: assertNotNull("There should be instantiations", svi);
146: assertTrue("#e2 should be instantiated", svi
147: .getInstantiations().isInstantiated(
148: TacletForTests.svLookup("#e2")));
149: assertTrue("#p1 should be instantiated", svi
150: .getInstantiations().isInstantiated(
151: TacletForTests.svLookup("#p1")));
152:
153: Term matchTwo = TacletForTests
154: .parseTerm("\\<{ l1:{l2:{while (true) {boolean b=true; break;} "
155: + "}int k=1;} }\\> true");
156: FindTaclet tacletTwo = (FindTaclet) TacletForTests.getTaclet(
157: "TestMatchTaclet_whileright_labeled").taclet();
158:
159: svi = tacletTwo.matchJavaBlock(matchTwo, (Term) tacletTwo
160: .find(), MatchConditions.EMPTY_MATCHCONDITIONS,
161: services);
162: assertNotNull(svi);
163:
164: assertTrue(svi.getInstantiations().isInstantiated(
165: TacletForTests.svLookup("#e2")));
166: assertTrue(svi.getInstantiations().isInstantiated(
167: TacletForTests.svLookup("#p1")));
168: assertTrue(svi.getInstantiations().isInstantiated(
169: TacletForTests.svLookup("#lab")));
170:
171: Term match3 = TacletForTests
172: .parseTerm("\\<{ l1:{l2:{while (true) {boolean b=false; break;} "
173: + "int k=1;}} }\\> true");
174: FindTaclet taclet3 = (FindTaclet) TacletForTests.getTaclet(
175: "TestMatchTaclet_whileright_labeled").taclet();
176:
177: svi = taclet3.matchJavaBlock(match3, (Term) taclet3.find(),
178: MatchConditions.EMPTY_MATCHCONDITIONS, services);
179: assertNull(svi);
180:
181: Term emptyBlock = TacletForTests
182: .parseTerm("\\<{ { {} int i = 0; } }\\> true");
183: FindTaclet empty_block_taclet = (FindTaclet) TacletForTests
184: .getTaclet("TestMatchTaclet_empty_block").taclet();
185:
186: svi = empty_block_taclet.matchJavaBlock(emptyBlock,
187: (Term) empty_block_taclet.find(),
188: MatchConditions.EMPTY_MATCHCONDITIONS, services);
189: assertTrue(svi != null);
190:
191: Term emptyBlock2 = TacletForTests
192: .parseTerm("\\<{ { {} } }\\> true");
193:
194: svi = empty_block_taclet.matchJavaBlock(emptyBlock2,
195: (Term) empty_block_taclet.find(),
196: MatchConditions.EMPTY_MATCHCONDITIONS, services);
197:
198: assertNotNull(svi);
199:
200: Debug.out("%%%%%%%%%%%%");
201: Term emptyBlock3 = TacletForTests
202: .parseTerm("\\<{ { {} l1:{} } }\\> true");
203: svi = empty_block_taclet.matchJavaBlock(emptyBlock3,
204: (Term) empty_block_taclet.find(),
205: MatchConditions.EMPTY_MATCHCONDITIONS, services);
206: assertNotNull(svi);
207:
208: FindTaclet var_decl_taclet = (FindTaclet) TacletForTests
209: .getTaclet("TestMatchTaclet_variable_declaration")
210: .taclet();
211:
212: svi = var_decl_taclet.matchJavaBlock(emptyBlock,
213: (Term) var_decl_taclet.find(),
214: MatchConditions.EMPTY_MATCHCONDITIONS, services);
215: assertNull(svi);
216:
217: Term emptyLabel = TacletForTests
218: .parseTerm("\\<{ { l1:{} } }\\> true");
219: FindTaclet empty_label_taclet = (FindTaclet) TacletForTests
220: .getTaclet("TestMatchTaclet_empty_label").taclet();
221: svi = empty_label_taclet.matchJavaBlock(emptyLabel,
222: (Term) empty_label_taclet.find(),
223: MatchConditions.EMPTY_MATCHCONDITIONS, services);
224: assertNotNull(svi);
225:
226: Term emptyLabel2 = TacletForTests
227: .parseTerm("\\<{ l2:{ l1:{} } }\\> true");
228: svi = empty_label_taclet.matchJavaBlock(emptyLabel2,
229: (Term) empty_label_taclet.find(),
230: MatchConditions.EMPTY_MATCHCONDITIONS, services);
231: assertNotNull(svi);
232:
233: Term emptyLabel3 = TacletForTests
234: .parseTerm("\\<{ {l3:{{l2:{l1:{}}}} int i = 0;} }\\> true");
235: svi = empty_label_taclet.matchJavaBlock(emptyLabel3,
236: (Term) empty_label_taclet.find(),
237: MatchConditions.EMPTY_MATCHCONDITIONS, services);
238: assertNotNull(svi);
239: }
240:
241: public void testProgramMatch1() {
242: Services services = TacletForTests.services();
243: de.uka.ilkd.key.java.Recoder2KeY c2k = new de.uka.ilkd.key.java.Recoder2KeY(
244: services, new NamespaceSet());
245: JavaBlock jb = c2k.readBlock("{ int i; int j; i=++j;"
246: + " while(true) {break;}}", c2k.createEmptyContext());
247:
248: de.uka.ilkd.key.java.StatementBlock sb = (de.uka.ilkd.key.java.StatementBlock) jb
249: .program();
250:
251: JavaBlock javaBlock = JavaBlock
252: .createJavaBlock(new de.uka.ilkd.key.java.StatementBlock(
253: new de.uka.ilkd.key.java.ArrayOfStatement(
254: new de.uka.ilkd.key.java.Statement[] {
255: (de.uka.ilkd.key.java.Statement) sb
256: .getChildAt(2),
257: (de.uka.ilkd.key.java.Statement) sb
258: .getChildAt(3) })));
259:
260: Term match = TermFactory.DEFAULT.createDiamondTerm(javaBlock,
261: TermFactory.DEFAULT.createJunctorTerm(Op.TRUE));
262:
263: FindTaclet taclet = (FindTaclet) TacletForTests.getTaclet(
264: "TestMatchTaclet_preincrement").taclet();
265:
266: MatchConditions svi = taclet.matchJavaBlock(match,
267: (Term) taclet.find(),
268: MatchConditions.EMPTY_MATCHCONDITIONS, services);
269:
270: assertTrue(svi.getInstantiations().isInstantiated(
271: TacletForTests.svLookup("#slhs1")));
272: assertTrue(svi.getInstantiations().isInstantiated(
273: TacletForTests.svLookup("#slhs2")));
274: }
275:
276: public void testProgramMatch2() {
277: Term match = TacletForTests
278: .parseTerm("\\<{int i; int k;}\\>(\\<{for (int i=0;"
279: + " i<2; i++) {break;} "
280: + "int k=1; }\\> true)");
281: FindTaclet taclet = (FindTaclet) TacletForTests.getTaclet(
282: "TestMatchTaclet_for_right").taclet();
283: MatchConditions svi = taclet.matchJavaBlock(match.sub(0),
284: (Term) taclet.find(),
285: MatchConditions.EMPTY_MATCHCONDITIONS, services);
286:
287: assertNotNull(svi);
288: assertTrue(svi.getInstantiations().isInstantiated(
289: TacletForTests.svLookup("#loopInit")));
290: assertTrue(svi.getInstantiations().isInstantiated(
291: TacletForTests.svLookup("#guard")));
292: assertTrue(svi.getInstantiations().isInstantiated(
293: TacletForTests.svLookup("#forupdates")));
294: assertTrue(svi.getInstantiations().isInstantiated(
295: TacletForTests.svLookup("#p1")));
296: }
297:
298: /*
299: public void testProgramMatch3() {
300: Term match = TacletForTests.parseTerm("<{ {int i=0; break; } }> true");
301: FindTaclet taclet
302: =(FindTaclet)TacletForTests.getTaclet("TestMatchTaclet_local_variable_rename").taclet();
303: SVInstantiations svi=(taclet.matchJavaProgram
304: (match.javaBlock(),
305: (ContextStatementBlock)taclet.find().javaBlock().program(),
306: taclet.createInitialInstantiation()));
307:
308: System.out.println(svi);
309: }
310: */
311:
312: public void testProgramMatch4() {
313: Term match = TacletForTests
314: .parseTerm("\\<{{while (1==1) {if (1==2) {break;}} return 1==3;}}\\>A");
315:
316: FindTaclet taclet = (FindTaclet) TacletForTests.getTaclet(
317: "TestMatchTaclet_while0").taclet();
318:
319: MatchConditions mc = (taclet.match(match, taclet.find(),
320: MatchConditions.EMPTY_MATCHCONDITIONS, services,
321: Constraint.BOTTOM));
322: assertNotNull(mc);
323: }
324:
325: public void testVarOccursInIfAndAddRule() {
326:
327: Term match = TacletForTests
328: .parseTerm("\\forall testSort z; (p(z) -> A)");
329:
330: // test at the subformula p(z) -> A that has a free variable
331: // therefore no match should be found
332:
333: Sequent seq = Sequent.createSequent(
334: Semisequent.EMPTY_SEMISEQUENT.insert(
335: 0,
336: new ConstrainedFormula(match.sub(1),
337: Constraint.BOTTOM)).semisequent(),
338: Semisequent.EMPTY_SEMISEQUENT);
339:
340: assertTrue(
341: "An area conflict should happen because there is a free"
342: + " variable and the matching part is in the if and addrule",
343: NoPosTacletApp
344: .createNoPosTacletApp(if_addrule_conflict)
345: .findIfFormulaInstantiations(seq, services,
346: Constraint.BOTTOM).size() == 0);
347:
348: // we bind the free variable now a match should be found
349: seq = Sequent.createSequent(
350: Semisequent.EMPTY_SEMISEQUENT
351: .insert(
352: 0,
353: new ConstrainedFormula(match,
354: Constraint.BOTTOM))
355: .semisequent(), Semisequent.EMPTY_SEMISEQUENT);
356:
357: assertTrue(
358: "No area conflict should happen because all variables are bound.",
359: NoPosTacletApp
360: .createNoPosTacletApp(if_addrule_conflict)
361: .findIfFormulaInstantiations(seq, services,
362: Constraint.BOTTOM).size() != 0);
363: }
364:
365: public void testVarOccursInFindAndAddRule() {
366: Term match = TacletForTests
367: .parseTerm("\\forall testSort z; (p(z) -> A)");
368:
369: //seq contains term that can match but has a free variable, so
370: //matching to a should be not possible
371:
372: PosTacletApp app = PosTacletApp.createPosTacletApp(
373: (FindTaclet) find_addrule_conflict,
374: find_addrule_conflict.match(match.sub(0),
375: find_addrule_conflict.find(), false,
376: MatchConditions.EMPTY_MATCHCONDITIONS,
377: services, Constraint.BOTTOM)
378: .getInstantiations(), new PosInOccurrence(
379: new ConstrainedFormula(match),
380: PosInTerm.TOP_LEVEL.down(0), true));
381:
382: assertTrue(
383: "A match has been found but there is a free variable in"
384: + " the term that has been matched and therefore an area"
385: + " conflict with find and addrule should have happened.",
386: app == null);
387:
388: // var is not free, match should be found
389: app = PosTacletApp.createPosTacletApp(
390: (FindTaclet) find_addrule_conflict,
391: find_addrule_conflict.match(match,
392: find_addrule_conflict.find(), false,
393: MatchConditions.EMPTY_MATCHCONDITIONS,
394: services, Constraint.BOTTOM)
395: .getInstantiations(), new PosInOccurrence(
396: new ConstrainedFormula(match),
397: PosInTerm.TOP_LEVEL, true));
398: assertTrue(
399: "A match should have been found,"
400: + " because here there formerly free variable is bound.",
401: app != null);
402: }
403:
404: public void testRWVarOccursFindAndIf() {
405: // the find expression is not a sequent, therefore find and if
406: // are two different areas and if find matches a term that
407: // contains a free variable, no match should be possible
408: //seq contains term that can match but has a free variable, so
409: //matching to a should be not possible
410: Term match = TacletForTests
411: .parseTerm("\\forall testSort z; (p(z) -> A)");
412: TacletApp app = PosTacletApp.createPosTacletApp(if_find_clash,
413: if_find_clash.match(match.sub(0), if_find_clash.find(),
414: false, MatchConditions.EMPTY_MATCHCONDITIONS,
415: services, Constraint.BOTTOM)
416: .getInstantiations(), new PosInOccurrence(
417: new ConstrainedFormula(match.sub(0)),
418: PosInTerm.TOP_LEVEL.down(0), true));
419:
420: assertTrue("Match found but match term contains free var and"
421: + "matching var occurs in two instantiation areas"
422: + " (if and find)", app == null);
423:
424: assertTrue("Match not found", if_find_clash.match(match,
425: if_find_clash.find(), false,
426: MatchConditions.EMPTY_MATCHCONDITIONS, services,
427: Constraint.BOTTOM) != null);
428: }
429:
430: public void testRWVarOccursInAddAndIf() {
431: // no clash should happen because in this case the add and if
432: // sections are the same area
433: Term match = TacletForTests
434: .parseTerm("\\forall testSort z; (p(z) -> A)");
435:
436: assertTrue("Match not found but should exist"
437: + " because add and if are same area", if_add_no_clash
438: .match(match.sub(0), if_add_no_clash.find(), false,
439: MatchConditions.EMPTY_MATCHCONDITIONS,
440: services, Constraint.BOTTOM) != null);
441: }
442:
443: public void testXNotFreeInYConflict() {
444: Term free_in = TacletForTests
445: .parseTerm("\\forall testSort z; (p(z) & p(f(z)))");
446: // matching the not_free_conflict Taclet with (P(f(z),z) should
447: // result in a conflict, because z is free in f(z) but
448: // the Taclet demands z not free in f(z)
449: assertTrue(
450: "Match should not be found because of conflict with "
451: + "..not free in..",
452: NoPosTacletApp.createNoPosTacletApp(not_free_conflict,
453: not_free_conflict.match(free_in,
454: not_free_conflict.find(), false,
455: MatchConditions.EMPTY_MATCHCONDITIONS,
456: services, Constraint.BOTTOM)) == null);
457:
458: Term not_free_in = TacletForTests
459: .parseTerm("\\forall testSort z; (p(z) & p(c))");
460: assertTrue("Match should be found because .. not free in.. "
461: + "is not relevant", NoPosTacletApp
462: .createNoPosTacletApp(not_free_conflict,
463: not_free_conflict.match(not_free_in,
464: not_free_conflict.find(), false,
465: MatchConditions.EMPTY_MATCHCONDITIONS,
466: services, Constraint.BOTTOM)) != null);
467: }
468:
469: public void testCloseWithBoundRenaming() {
470: Term closeable_one = TacletForTests
471: .parseTerm("\\forall testSort z; p(z)");
472: Term closeable_two = TacletForTests
473: .parseTerm("\\forall testSort y; p(y)");
474: Sequent seq = Sequent.createSequent(
475: Semisequent.EMPTY_SEMISEQUENT.insert(0,
476: new ConstrainedFormula(closeable_one))
477: .semisequent(), Semisequent.EMPTY_SEMISEQUENT
478: .insert(0,
479: new ConstrainedFormula(closeable_two))
480: .semisequent());
481: TacletIndex index = new TacletIndex();
482: index.add(close_rule.taclet());
483: PosInOccurrence posAntec = new PosInOccurrence(
484: new ConstrainedFormula(closeable_two, Constraint.BOTTOM),
485: PosInTerm.TOP_LEVEL, false);
486:
487: TacletApp tacletApp = index.getSuccedentTaclet(posAntec,
488: new IHTacletFilter(true, SLListOfRuleSet.EMPTY_LIST),
489: services, Constraint.BOTTOM).iterator().next();
490: assertTrue("Match should be possible(modulo renaming)",
491: tacletApp.findIfFormulaInstantiations(seq, services,
492: Constraint.BOTTOM).size() > 0);
493: }
494:
495: // a greater test
496: public void testConflict() {
497: Term match = TacletForTests.parseTerm("p1(m1(n))");
498: for (int i = 0; i < conflict.length; i++) {
499: assertTrue(
500: "Match should not be found because of area conflict:"
501: + i, conflict[i].match(match,
502: ((FindTaclet) conflict[i]).find(),
503: MatchConditions.EMPTY_MATCHCONDITIONS,
504: services, Constraint.BOTTOM) == null);
505: }
506: }
507:
508: // test match of update terms
509: public void testUpdateMatch() {
510: Term match = TacletForTests
511: .parseTerm("\\<{int i;}\\>{i:=2}(\\forall nat z; (q1(z)))");
512: match = match.sub(0);
513: assertTrue(
514: "Instantiations should be found as updates can be ignored if "
515: + "only the term that is matched has an update and the "
516: + "template it is matched to has none.",
517: all_left.match(match, ((FindTaclet) all_left).find(),
518: true, MatchConditions.EMPTY_MATCHCONDITIONS,
519: services, Constraint.BOTTOM) != null);
520:
521: Term match2 = TacletForTests
522: .parseTerm("\\<{int i;}\\>{i:=Z(2(#))} true");
523: match2 = match2.sub(0);
524: assertTrue("Instantiations should be found.", assign_n.match(
525: match2, ((FindTaclet) assign_n).find(), true,
526: MatchConditions.EMPTY_MATCHCONDITIONS, services,
527: Constraint.BOTTOM) != null);
528: }
529:
530: public void testIgnoredQuantifiedUpdateEquals() {
531: Term match = TacletForTests
532: .parseTerm("\\<{int im;}\\>({\\for int j; im := j }true & {\\for int k; im := k }true)");
533:
534: assertTrue(
535: "Updates should be equal modulo bound renaming (upd1, upd2)"
536: + match.sub(0).sub(0) + "::"
537: + match.sub(0).sub(1), new UpdatePair(match
538: .sub(0).sub(0)).equals(new UpdatePair(match
539: .sub(0).sub(1))));
540:
541: Term match2 = TacletForTests
542: .parseTerm("\\<{ java.lang.Object obj; java.lang.String s; }\\>"
543: + "({\\for java.lang.String j; obj := j }true & {\\for java.lang.Object k; obj := k }true)");
544:
545: assertFalse(
546: "Updates should not be equal modulo bound renaming (upd1, upd2) as "
547: + "even if the quantified variables have not the same sorts (compatible ones, "
548: + "yes...but not equal ones)"
549: + match2.sub(0).sub(0) + "::"
550: + match2.sub(0).sub(1), new UpdatePair(match2
551: .sub(0).sub(0)).equals(new UpdatePair(match2
552: .sub(0).sub(1))));
553:
554: assertFalse(
555: "Updates should not be equal modulo bound renaming (upd1, upd2) as "
556: + "even if the quantified variables have not the same sorts (compatible ones, "
557: + "yes...but not equal ones)"
558: + match2.sub(0).sub(1) + "::"
559: + match2.sub(0).sub(0), new UpdatePair(match2
560: .sub(0).sub(1)).equals(new UpdatePair(match2
561: .sub(0).sub(0))));
562:
563: }
564:
565: public void testProgramMatchEmptyBlock() {
566: Term match = TacletForTests.parseTerm("\\<{ }\\>true ");
567: FindTaclet taclet = (FindTaclet) TacletForTests.getTaclet(
568: "empty_diamond").taclet();
569: MatchConditions mc = (taclet.match(match, taclet.find(),
570: MatchConditions.EMPTY_MATCHCONDITIONS, services,
571: Constraint.BOTTOM));
572:
573: assertNotNull(mc);
574:
575: match = TacletForTests.parseTerm("\\<{ {} }\\>true ");
576: taclet = (FindTaclet) TacletForTests.getTaclet(
577: "TestMatchTaclet_empty_block").taclet();
578:
579: mc = (taclet.match(match, taclet.find(),
580: MatchConditions.EMPTY_MATCHCONDITIONS, services,
581: Constraint.BOTTOM));
582:
583: assertNotNull(mc);
584:
585: match = TacletForTests.parseTerm("\\<{ {int i = 0;} }\\>true ");
586: mc = (taclet.match(match, taclet.find(),
587: MatchConditions.EMPTY_MATCHCONDITIONS, services,
588: Constraint.BOTTOM));
589:
590: assertNull("The block is not empty", mc);
591:
592: }
593:
594: //Assume A is a supersort of B. Then a term SV of sort A should match
595: //a term of sort B. (assertNotNull)
596: public void testWithSubSortsTermSV() {
597: Sort osort1 = (Sort) TacletForTests.getSorts().lookup(
598: new Name("Obj"));
599: Sort osort2 = new ClassInstanceSortImpl(new Name("os2"),
600: osort1, false);
601: Sort osort3 = new ClassInstanceSortImpl(new Name("os3"),
602: osort1, false);
603: Sort osort4 = new ClassInstanceSortImpl(new Name("os4"),
604: SetAsListOfSort.EMPTY_SET.add(osort2).add(osort3),
605: false);
606: Function v4 = new RigidFunction(new Name("v4"), osort4,
607: new Sort[0]);
608: TermFactory tf = TermFactory.DEFAULT;
609: Term match = tf.createFunctionTerm(v4);
610: FindTaclet taclet = (FindTaclet) TacletForTests.getTaclet(
611: "TestMatchTaclet_subsort_termSV").taclet();
612: MatchConditions mc = taclet.match(match, taclet.find(),
613: MatchConditions.EMPTY_MATCHCONDITIONS, services,
614: Constraint.BOTTOM);
615: assertNotNull(mc);
616: }
617:
618: //Assume A is a supersort of B. Then a variable SV of sort A should _NOT_
619: //match a logic variable of sort B. (assertNull)
620: public void testWithSubSortsVariableSV() {
621: Sort osort1 = (Sort) TacletForTests.getSorts().lookup(
622: new Name("Obj"));
623: Sort osort2 = new ClassInstanceSortImpl(new Name("os2"),
624: osort1, false);
625: Sort osort3 = new ClassInstanceSortImpl(new Name("os3"),
626: osort1, false);
627: Sort osort4 = new ClassInstanceSortImpl(new Name("os4"),
628: SetAsListOfSort.EMPTY_SET.add(osort2).add(osort3),
629: false);
630: TermFactory tf = TermFactory.DEFAULT;
631: Function aPred = (Function) TacletForTests.getFunctions()
632: .lookup(new Name("A"));
633: Term sub = tf.createFunctionTerm(aPred);
634: Term match = tf.createQuantifierTerm(Op.ALL, new LogicVariable(
635: new Name("lv"), osort4), sub);
636: FindTaclet taclet = (FindTaclet) TacletForTests.getTaclet(
637: "TestMatchTaclet_subsort_variableSV").taclet();
638: MatchConditions mc = taclet.match(match, taclet.find(),
639: MatchConditions.EMPTY_MATCHCONDITIONS, services,
640: Constraint.BOTTOM);
641: assertNull(mc);
642: }
643:
644: public void testNoContextMatching() {
645: Term match = TacletForTests
646: .parseTerm("\\<{{ int i = 0;}}\\>true ");
647: FindTaclet taclet = (FindTaclet) TacletForTests.getTaclet(
648: "TestMatchTaclet_nocontext").taclet();
649: MatchConditions mc = (taclet.match(match, taclet.find(),
650: MatchConditions.EMPTY_MATCHCONDITIONS, services,
651: Constraint.BOTTOM));
652: assertNotNull("No context matching corrupt.", mc);
653: }
654:
655: public void testPrefixMatching() {
656: TermFactory tf = TermFactory.DEFAULT;
657: Term match = TacletForTests.parseTerm("\\<{return;}\\>true ");
658: StatementBlock prg = (StatementBlock) match.javaBlock()
659: .program();
660: ExecutionContext ec = new ExecutionContext(new TypeRef(
661: new KeYJavaType(PrimitiveType.JAVA_BYTE,
662: new PrimitiveSort(new Name("byte")))),
663: new LocationVariable(new ProgramElementName("testVar"),
664: new PrimitiveSort(new Name("testSort"))));
665: MethodFrame mframe = new MethodFrame(null, ec, prg);
666: match = tf.createDiamondTerm(JavaBlock
667: .createJavaBlock(new StatementBlock(mframe)), match
668: .sub(0));
669: FindTaclet taclet = (FindTaclet) TacletForTests.getTaclet(
670: "TestMatchTaclet_methodframe").taclet();
671: MatchConditions mc = (taclet.match(match, taclet.find(),
672: MatchConditions.EMPTY_MATCHCONDITIONS, services,
673: Constraint.BOTTOM));
674: assertNotNull("Method-Frame should match", mc);
675:
676: Term termWithPV = TacletForTests.parseTerm("\\<{int i;}\\>i=0");
677: match = TacletForTests.parseTerm("\\<{return 2;}\\>true ");
678: prg = (StatementBlock) match.javaBlock().program();
679: mframe = new MethodFrame((IProgramVariable) termWithPV.sub(0)
680: .sub(0).op(), ec, prg);
681: match = tf.createDiamondTerm(JavaBlock
682: .createJavaBlock(new StatementBlock(mframe)), match
683: .sub(0));
684: taclet = (FindTaclet) TacletForTests.getTaclet(
685: "TestMatchTaclet_methodframe_value").taclet();
686: mc = (taclet.match(match, taclet.find(),
687: MatchConditions.EMPTY_MATCHCONDITIONS, services,
688: Constraint.BOTTOM));
689: assertNotNull("Method-Frame with return value should match", mc);
690:
691: }
692:
693: public void testBugsThathaveBeenRemoved() {
694:
695: Term match = TacletForTests
696: .parseTerm("\\<{ int i = 0; }\\>true ");
697: FindTaclet taclet = (FindTaclet) TacletForTests.getTaclet(
698: "TestMatchTaclet_eliminate_variable_declaration")
699: .taclet();
700: MatchConditions mc = (taclet.match(match, taclet.find(),
701: MatchConditions.EMPTY_MATCHCONDITIONS, services,
702: Constraint.BOTTOM));
703:
704: assertNull(
705: "The reason for this bug was related to the introduction of "
706: + "statementlist schemavariables and that we could not end the "
707: + "match if the size of nonterminalelements was unequal "
708: + "The solution was to weaken the check for statement blocks but NOT "
709: + "for other statement or expressions containers. The bug occured because "
710: + "the weaker test was also "
711: + "performed for expressions.", mc);
712:
713: match = TacletForTests
714: .parseTerm("\\<{ {{throw null;} int i = 0;} }\\>true ");
715: taclet = (FindTaclet) TacletForTests.getTaclet(
716: "TestMatchTaclet_throw_in_block").taclet();
717: mc = (taclet.match(match, taclet.find(),
718: MatchConditions.EMPTY_MATCHCONDITIONS, services,
719: Constraint.BOTTOM));
720: assertNull("No match expected.", mc);
721:
722: match = TacletForTests
723: .parseTerm("\\<{{ int l1=1;} if (true);}\\>true");
724: taclet = (FindTaclet) TacletForTests.getTaclet(
725: "TestMatchTaclet_elim_double_block").taclet();
726: mc = (taclet.match(match, taclet.find(),
727: MatchConditions.EMPTY_MATCHCONDITIONS, services,
728: Constraint.BOTTOM));
729: assertNull("Removed bug #118. No match expected.", mc);
730:
731: match = TacletForTests.parseTerm("\\<{ {} {int i;} }\\> true");
732: taclet = (FindTaclet) TacletForTests.getTaclet(
733: "TestMatchTaclet_wrap_blocks").taclet();
734: mc = (taclet.match(match, taclet.find(),
735: MatchConditions.EMPTY_MATCHCONDITIONS, services,
736: Constraint.BOTTOM));
737: assertNotNull(
738: "Bug originally failed to match the first empty block.",
739: mc);
740:
741: match = TacletForTests.parseTerm("\\<{ {} {int i;} }\\> true");
742: taclet = (FindTaclet) TacletForTests.getTaclet(
743: "TestMatchTaclet_wrap_blocks_two_empty_lists").taclet();
744: mc = (taclet.match(match, taclet.find(),
745: MatchConditions.EMPTY_MATCHCONDITIONS, services,
746: Constraint.BOTTOM));
747: assertNotNull(
748: "Bug originally failed to match the first empty block,"
749: + " because of he was not able to match two succeeding empty lists.",
750: mc);
751:
752: match = TacletForTests.parseTerm("\\<{ {{}} {} }\\> true");
753: taclet = (FindTaclet) TacletForTests.getTaclet(
754: "TestMatchTaclet_remove_empty_blocks").taclet();
755: mc = (taclet.match(match, taclet.find(),
756: MatchConditions.EMPTY_MATCHCONDITIONS, services,
757: Constraint.BOTTOM));
758: assertNotNull("Bug matching empty blocks using list svs.", mc);
759:
760: match = TacletForTests
761: .parseTerm("\\<{ { int i; } {} }\\> true");
762: taclet = (FindTaclet) TacletForTests.getTaclet(
763: "TestMatchTaclet_bug_matching_lists").taclet();
764: mc = (taclet.match(match, taclet.find(),
765: MatchConditions.EMPTY_MATCHCONDITIONS, services,
766: Constraint.BOTTOM));
767: assertNotNull("List matching bug.", mc);
768:
769: }
770:
771: public static void main(String args[]) {
772: TestMatchTaclet t = new TestMatchTaclet("XXX", true);
773: t.setUp();
774: t.testPrefixMatching();
775: // t.testBugsThathaveBeenRemoved();
776: //t.testStatementListMatch();
777: }
778:
779: }
|