001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.parser;
012:
013: import java.io.PrintWriter;
014: import java.io.StringReader;
015: import java.io.StringWriter;
016:
017: import junit.framework.TestCase;
018: import de.uka.ilkd.key.java.Recoder2KeY;
019: import de.uka.ilkd.key.java.Services;
020: import de.uka.ilkd.key.logic.*;
021: import de.uka.ilkd.key.logic.op.*;
022: import de.uka.ilkd.key.logic.sort.AbstractSort;
023: import de.uka.ilkd.key.logic.sort.Sort;
024: import de.uka.ilkd.key.pp.AbbrevMap;
025: import de.uka.ilkd.key.rule.SetAsListOfTaclet;
026: import de.uka.ilkd.key.rule.TacletForTests;
027: import de.uka.ilkd.key.util.DefaultExceptionHandler;
028: import de.uka.ilkd.key.util.ExceptionHandlerException;
029:
030: public class TestTermParser extends TestCase {
031:
032: private TermFactory tf = TermFactory.DEFAULT;
033:
034: NamespaceSet nss;
035:
036: Services serv;
037:
038: Recoder2KeY r2k;
039:
040: Sort elem, list, int_sort;
041:
042: Function head, tail, nil, cons, isempty, p;
043:
044: LogicVariable x, y, z, xs, ys, zs;
045:
046: Term t_x, t_y, t_z, t_xs, t_ys, t_zs;
047: Term t_headxs, t_tailxs, t_tailys, t_nil;
048:
049: public TestTermParser(String name) {
050: super (name);
051: }
052:
053: public void setUp() {
054: nss = new NamespaceSet();
055: serv = TacletForTests.services();
056: r2k = new Recoder2KeY(serv, nss);
057: r2k.parseSpecialClasses();
058: parseDecls("\\sorts { boolean; elem; list; int; int_sort; numbers; }\n"
059: + "\\functions {\n"
060: + " elem head(list);\n"
061: + " list tail(list);\n"
062: + " list nil;\n"
063: + " list cons(elem,list);\n"
064: + "numbers #;\n"
065: + "numbers 0 (numbers);\n"
066: + "numbers 1 (numbers);\n"
067: + "numbers 2 (numbers);\n"
068: + "numbers 3 (numbers);\n"
069: + "numbers 4 (numbers);\n"
070: + "numbers 5 (numbers);\n"
071: + "numbers 6 (numbers);\n"
072: + "numbers 7 (numbers);\n"
073: + "numbers 8 (numbers);\n"
074: + "numbers 9 (numbers);\n"
075: + "numbers neglit (numbers);\n"
076: + "int Z (numbers);\n"
077: + "int neg (int);\n"
078: + "int add (int,int);\n"
079: + "int sub (int,int);\n"
080: + "int mul (int,int);\n"
081: + "int div (int,int);\n"
082: + "int mod (int,int);\n"
083: + "int aa ;\n"
084: + "int bb ;\n"
085: + "int cc ;\n"
086: + "int dd ;\n"
087: + "int ee ;\n"
088: + "}\n"
089: + "\\predicates {\n"
090: + " lt(int,int);\n"
091: + " leq(int,int);\n"
092: + " isempty(list);\n"
093: + " p(elem,list);\n" + "}\n"
094:
095: );
096:
097: int_sort = lookup_sort("int");
098: ((AbstractSort) int_sort).addDefinedSymbols(serv
099: .getNamespaces().functions(), serv.getNamespaces()
100: .sorts());
101: elem = lookup_sort("elem");
102: list = lookup_sort("list");
103:
104: head = lookup_func("head");
105: tail = lookup_func("tail");
106: nil = lookup_func("nil");
107: cons = lookup_func("cons");
108: isempty = lookup_func("isempty");
109: p = lookup_func("p");
110:
111: // The declaration parser cannot parse LogicVariables; these
112: // are normally declared in quantifiers, so we introduce them
113: // ourselves!
114: x = declareVar("x", elem);
115: t_x = tf.createVariableTerm(x);
116: y = declareVar("y", elem);
117: t_y = tf.createVariableTerm(y);
118: z = declareVar("z", elem);
119: t_z = tf.createVariableTerm(z);
120: xs = declareVar("xs", list);
121: t_xs = tf.createVariableTerm(xs);
122: ys = declareVar("ys", list);
123: t_ys = tf.createVariableTerm(ys);
124: zs = declareVar("zs", list);
125: t_zs = tf.createVariableTerm(zs);
126:
127: t_headxs = tf.createFunctionTerm(head, t_xs);
128: t_tailxs = tf.createFunctionTerm(tail, t_xs);
129: t_tailys = tf.createFunctionTerm(tail, t_ys);
130: t_nil = tf.createFunctionTerm(nil);
131: }
132:
133: Sort lookup_sort(String name) {
134: return (Sort) nss.sorts().lookup(new Name(name));
135: }
136:
137: Function lookup_func(String name) {
138: return (Function) nss.functions().lookup(new Name(name));
139: }
140:
141: LogicVariable declareVar(String name, Sort sort) {
142: LogicVariable v = new LogicVariable(new Name(name), sort);
143: nss.variables().add(v);
144: return v;
145: }
146:
147: private KeYParser stringDeclParser(String s) {
148: // fills namespaces
149: new Recoder2KeY(TacletForTests.services(), nss)
150: .parseSpecialClasses();
151: return new KeYParser(
152: ParserMode.DECLARATION,
153: new KeYLexer(new StringReader(s), null),
154: "No file. Call of parser from parser/TestTermParser.java",
155: serv, nss);
156: }
157:
158: public void parseDecls(String s) {
159: try {
160: stringDeclParser(s).decls();
161: } catch (Exception e) {
162: StringWriter sw = new StringWriter();
163: PrintWriter pw = new PrintWriter(sw);
164: e.printStackTrace(pw);
165: throw (RuntimeException) new RuntimeException(
166: "Exc while Parsing:\n" + sw).initCause(e);
167: }
168: }
169:
170: public Term parseProblem(String s) {
171: try {
172: new Recoder2KeY(TacletForTests.services(), nss)
173: .parseSpecialClasses();
174: return new KeYParser(
175: ParserMode.PROBLEM,
176: new KeYLexer(new StringReader(s), null),
177: "No file. Call of parser from parser/TestTermParser.java",
178: new ParserConfig(serv, nss), new ParserConfig(serv,
179: nss), null, SetAsListOfTaclet.EMPTY_SET,
180: null).problem();
181: } catch (Exception e) {
182: StringWriter sw = new StringWriter();
183: PrintWriter pw = new PrintWriter(sw);
184: e.printStackTrace(pw);
185: throw new RuntimeException("Exc while Parsing:\n" + sw);
186: }
187: }
188:
189: private KeYParser stringTermParser(String s) {
190: return new KeYParser(
191: ParserMode.TERM,
192: new KeYLexer(new StringReader(s),
193: new DefaultExceptionHandler()),
194: "No file. Call of parser from parser/TestTermParser.java",
195: tf, r2k = new Recoder2KeY(TacletForTests.services(),
196: nss), TacletForTests.services(), nss,
197: new AbbrevMap());
198:
199: }
200:
201: public Term parseTerm(String s) {
202: try {
203: return stringTermParser(s).term();
204: } catch (Exception e) {
205: StringWriter sw = new StringWriter();
206: PrintWriter pw = new PrintWriter(sw);
207: e.printStackTrace(pw);
208: throw new RuntimeException("Exc while Parsing:\n" + sw);
209: }
210: }
211:
212: public SetOfLocationDescriptor parseModifies(String s) {
213: try {
214: return stringTermParser(s).location_list();
215: } catch (Exception e) {
216: StringWriter sw = new StringWriter();
217: PrintWriter pw = new PrintWriter(sw);
218: e.printStackTrace(pw);
219: throw new RuntimeException("Exc while Parsing:\n" + sw);
220: }
221: }
222:
223: public Term parseFma(String s) {
224: try {
225: return stringTermParser(s).formula();
226: } catch (Exception e) {
227: StringWriter sw = new StringWriter();
228: PrintWriter pw = new PrintWriter(sw);
229: e.printStackTrace(pw);
230: throw new RuntimeException("Exc while Parsing:\n" + sw);
231: }
232: }
233:
234: public void test1() {
235: assertEquals("parse x", t_x, parseTerm("x"));
236: }
237:
238: public void test1a() {
239: boolean parsed = false;
240: try {
241: parseTerm("x()");
242: parsed = true;
243: } catch (Exception e) {
244: }
245: assertFalse("parse x() should fail", parsed);
246: }
247:
248: public void test2() {
249: assertEquals("parse head(xs)", t_headxs, parseTerm("head(xs)"));
250: }
251:
252: public void test3() {
253: Term t = tf.createFunctionTerm(cons, t_headxs, t_tailys);
254:
255: assertEquals("parse cons(head(xs),tail(ys))", t,
256: parseTerm("cons(head(xs),tail(ys))"));
257: }
258:
259: public void test5() {
260: Term t = tf.createEqualityTerm(tf.createFunctionTerm(head, tf
261: .createFunctionTerm(cons, t_x, t_xs)), tf
262: .createFunctionTerm(head, tf.createFunctionTerm(cons,
263: t_x, t_nil)));
264:
265: assertEquals("parse head(cons(x,xs))=head(cons(x,nil))", t,
266: parseFma("head(cons(x,xs))=head(cons(x,nil))"));
267: assertEquals("parse head(cons(x,xs))=head(cons(x,nil))", t,
268: parseFma("head(cons(x,xs))=head(cons(x,nil()))"));
269: }
270:
271: public void testNotEqual() {
272: Term t = tf.createJunctorTerm(Op.NOT, tf.createEqualityTerm(tf
273: .createFunctionTerm(head, tf.createFunctionTerm(cons,
274: t_x, t_xs)), tf.createFunctionTerm(head, tf
275: .createFunctionTerm(cons, t_x, t_nil))));
276:
277: assertEquals("parse head(cons(x,xs))!=head(cons(x,nil))", t,
278: parseFma("head(cons(x,xs))!=head(cons(x,nil))"));
279: }
280:
281: public void test6() {
282: Term t = tf.createJunctorTerm(Op.EQV, tf.createJunctorTerm(
283: Op.IMP, tf.createJunctorTerm(Op.OR, tf
284: .createEqualityTerm(t_x, t_x), tf
285: .createEqualityTerm(t_y, t_y)), tf
286: .createJunctorTerm(Op.AND, tf
287: .createEqualityTerm(t_z, t_z), tf
288: .createEqualityTerm(t_xs, t_xs))), tf
289: .createJunctorTerm(Op.NOT, tf.createEqualityTerm(t_ys,
290: t_ys)));
291:
292: assertEquals("parse x=x | y=y -> z=z & xs =xs <-> ! ys = ys",
293: t, parseFma("x=x|y=y->z=z&xs=xs<->!ys=ys"));
294: }
295:
296: public void test7() {
297: /** Bound variables are newly created by the parser,
298: * so we have to parse first, then extract the used variables,
299: * then build the formulae. */
300:
301: String s = "\\forall list x; \\forall list l1; ! x = l1";
302: Term t = parseFma(s);
303:
304: LogicVariable this x = (LogicVariable) t.varsBoundHere(0)
305: .getQuantifiableVariable(0);
306: LogicVariable l1 = (LogicVariable) t.sub(0).varsBoundHere(0)
307: .getQuantifiableVariable(0);
308:
309: Term t1 = tf.createQuantifierTerm(Op.ALL, this x, tf
310: .createQuantifierTerm(Op.ALL, l1, tf.createJunctorTerm(
311: Op.NOT, tf.createEqualityTerm(tf
312: .createVariableTerm(this x), tf
313: .createVariableTerm(l1)))));
314:
315: assertTrue("new variable in quantifier", this x != x);
316: assertEquals(
317: "parse \\forall list x; \\forall list l1; ! x = l1",
318: t1, t);
319:
320: }
321:
322: public void test8() {
323: /** A bit like test7, but for a substitution term */
324:
325: {
326: String s = "{\\subst elem xs; head(xs)} cons(xs,ys)";
327: Term t = parseTerm(s);
328:
329: LogicVariable this xs = (LogicVariable) t.varsBoundHere(1)
330: .getQuantifiableVariable(0);
331:
332: Term t1 = tf.createSubstitutionTerm(Op.SUBST, this xs,
333: t_headxs, tf.createFunctionTerm(cons, tf
334: .createVariableTerm(this xs), t_ys));
335:
336: assertTrue("new variable in subst term", this xs != xs);
337: assertEquals("parse {xs:elem head(xs)} cons(xs,ys)", t1, t);
338: }
339: }
340:
341: public void test9() {
342: /* Try something with a prediate */
343:
344: String s = "\\exists list x; !isempty(x)";
345: Term t = parseFma(s);
346:
347: LogicVariable this x = (LogicVariable) t.varsBoundHere(0)
348: .getQuantifiableVariable(0);
349:
350: Term t1 = tf.createQuantifierTerm(Op.EX, this x, tf
351: .createJunctorTerm(Op.NOT, tf.createFunctionTerm(
352: isempty, tf.createVariableTerm(this x))));
353:
354: assertTrue("new variable in quantifier", this x != x);
355: assertEquals(
356: "parse \\forall list x; \\forall list l1; ! x = l1",
357: t1, t);
358:
359: }
360:
361: public void test10() {
362: // Unquoted, this is
363: // <{ int x = 2; {String x = "\"}";} }> true
364: // String s = "< { int x = 1; {String s = \"\\\"}\";} } > true";
365: String s = "\\<{ int x = 1; {int s = 2;} }\\> x=x";
366: Term t = parseTerm(s);
367:
368: // for now, just check that the parser doesn't crash
369:
370: // System.out.println(t);
371:
372: // Same with a box
373: s = "\\[{ int x = 2; {String s = \"\\\"}\";} }\\] true";
374: //s = "< { int x = 1; {int s = 2;} } > true";
375: t = parseTerm(s);
376: //System.out.println(t);
377: }
378:
379: public void test12() {
380: String s = "\\<{int i; i=0;}\\> \\<{ while (i>0) ;}\\>true";
381: Term t = parseTerm(s);
382: }
383:
384: public void test13() {
385: Term t1 = parseTerm("\\exists elem x; \\forall list ys; \\forall list xs; ( xs ="
386: + " cons(x,ys))");
387: Term t2 = parseTerm("\\exists elem y; \\forall list xs; \\forall list ys; ( ys ="
388: + " cons(y,xs))");
389: Term t3 = parseTerm("\\exists int_sort bi; (\\<{ int p_x = 1;"
390: + " {int s = 2;} }\\>" + " p_x=p_x ->"
391: + "\\<{ int p_x = 1;boolean p_y=2<1;"
392: + " while(p_y){ int s=3 ;} }\\>" + " p_x=p_x)");
393: Term t4 = parseTerm("\\exists int_sort ci; (\\<{ int p_y = 1;"
394: + " {int s = 2;} }\\>" + " p_y=p_y ->"
395: + "\\<{ int p_y = 1;boolean p_x = 2<1;"
396: + "while(p_x){ int s=3 ;} }\\>" + " p_y=p_y)");
397: assertTrue("Terms should be equalModRenaming", t3
398: .equalsModRenaming(t4));
399: }
400:
401: public void test14() {
402: String s = "\\<{int[] i;i=new int[5];}\\>i[3]=i[2]";
403: Term t = parseTerm(s);
404: s = "\\<{int[] i;}\\>\\<{}\\>true";
405: t = parseTerm(s);
406: }
407:
408: public void xtestBindingUpdateTermOldBindingAlternative() {
409: String s = "\\<{int i,j;}\\> {i:=j} i = j";
410: Term t = parseTerm(s);
411: assertTrue("expected {i:=j}(i=j) but is ({i:=j}i)=j)", t.sub(0)
412: .op() instanceof IUpdateOperator);
413: }
414:
415: public void testBindingUpdateTerm() {
416: String s = "\\<{int i,j;}\\> {i:=j} i = j";
417: Term t = parseTerm(s);
418: assertFalse("expected ({i:=j}i)=j) but is {i:=j}(i=j)", t
419: .sub(0).op() instanceof IUpdateOperator);
420: }
421:
422: public void testParsingArray() {
423: String s = "\\<{int[][] i; int j;}\\> i[j][j] = j";
424: Term t = parseTerm(s);
425: }
426:
427: // fails because of lexer matching blocks with braces
428: public void xtestParsingArrayWithSpaces() {
429: String s = "\\<{int[][] i; int j;}\\> i[ j ][ j ] = j";
430: Term t = parseTerm(s);
431: }
432:
433: public void testParsingArrayCombination() {
434: String s = "\\<{int[][] i; int j;}\\> i [i[i[j][j]][i[j][j]]][i[j][i[j][j]]] = j";
435: Term t = parseTerm(s);
436: }
437:
438: public void testAmbigiousFuncVarPred() {
439: // tests bug id 216
440: String s = "\\functions {} \\predicates{gt(int, int);}"
441: + "\n\\problem {\\forall int x; gt(x, 0)}\n \\proof {\n"
442: + "(branch \"dummy ID\""
443: + "(opengoal \" ==> true -> true \") ) }";
444: try {
445: parseProblem(s);
446: } catch (RuntimeException re) {
447: System.out.println(re);
448: assertTrue("Fixed bug 216 occured again. The original bug "
449: + "was due to ambigious rules using semantic "
450: + "predicates in a 'wrong' way", false);
451: }
452: }
453:
454: public void testParseQueriesAndAttributes() {
455: TacletForTests.getJavaInfo().readJavaBlock("{}");
456: r2k.readCompilationUnit("public class T extends "
457: + "java.lang.Object{ " + "private T a;"
458: + "private static T b;" + "T c;" + "static T d;"
459: + "public T e;" + "public static T f;"
460: + "protected T g;" + "protected T h;"
461: + "public T query(){} "
462: + "public static T staticQ(T p){} "
463: + "public static T staticQ() {}}");
464: String s = "\\<{T t;}\\> (t.query()=t & t.query@(T)()=t & T.staticQ()=t "
465: + "& T.staticQ(t)=t & T.b=t.a@(T) & T.d=t.c@(T) & t.e@(T)=T.f & t.g@(T)=t.h@(T))";
466: parseTerm(s);
467: }
468:
469: public void testProgramVariables() {
470: TacletForTests.getJavaInfo().readJavaBlock("{}");
471: r2k.readCompilationUnit("public class T0 extends "
472: + "java.lang.Object{} ");
473: String s = "\\<{T0 t;}\\> t(1,2) = t()";
474: boolean parsed = false;
475: try {
476: parseTerm(s);
477: parsed = true;
478: } catch (Exception e) {
479: }
480: assertFalse("Program variables should not have arguments",
481: parsed);
482: }
483:
484: public void testNegativeLiteralParsing() {
485: String s1 = "-1234";
486: Term t = null;
487: try {
488: t = parseTerm(s1);
489: } catch (Exception e) {
490: fail();
491: }
492: assertTrue("Failed parsing negative literal", ("" + t.op()
493: .name()).equals("Z")
494: && ("" + t.sub(0).op().name()).equals("neglit"));
495:
496: String s2 = "-(1) ";
497: try {
498: t = parseTerm(s2);
499: } catch (Exception e) {
500: fail();
501: }
502: assertTrue("Failed parsing negative complex term", ("" + t.op()
503: .name()).equals("neg")
504: && ("" + t.sub(0).op().name()).equals("Z"));
505:
506: String s3 = "\\forall int i; -i = 0 ";
507: try {
508: t = parseTerm(s3);
509: } catch (Exception e) {
510: fail();
511: }
512: assertTrue("Failed parsing negative variable", ("" + t.sub(0)
513: .sub(0).op().name()).equals("neg"));
514:
515: }
516:
517: public void testIfThenElse() {
518: Term t = null, t2 = null;
519:
520: String s1 = "\\if (3=4) \\then (1) \\else (2)";
521: try {
522: t = parseTerm(s1);
523: } catch (Exception e) {
524: fail();
525: }
526: assertTrue("Failed parsing integer if-then-else term",
527: t.op() == Op.IF_THEN_ELSE
528: && t.sub(0).equals(parseTerm("3=4"))
529: && t.sub(1).equals(parseTerm("1"))
530: && t.sub(2).equals(parseTerm("2")));
531:
532: String s2 = "\\if (3=4 & 1=1) \\then (\\if (3=4) \\then (1) \\else (2)) \\else (2)";
533: try {
534: t2 = parseTerm(s2);
535: } catch (Exception e) {
536: fail();
537: }
538: assertTrue("Failed parsing nested integer if-then-else term",
539: t2.op() == Op.IF_THEN_ELSE
540: && t2.sub(0).equals(parseTerm("3=4 & 1=1"))
541: && t2.sub(1).equals(t)
542: && t2.sub(2).equals(parseTerm("2")));
543:
544: String s3 = "\\if (3=4) \\then (1=2) \\else (2=3)";
545: try {
546: t = parseTerm(s3);
547: } catch (Exception e) {
548: fail();
549: }
550: assertTrue("Failed parsing propositional if-then-else term", t
551: .op() == Op.IF_THEN_ELSE
552: && t.sub(0).equals(parseTerm("3=4"))
553: && t.sub(1).equals(parseTerm("1=2"))
554: && t.sub(2).equals(parseTerm("2=3")));
555:
556: }
557:
558: public void testIfExThenElse() {
559: Term t = null, t2 = null;
560:
561: String s1 = "\\ifEx int x; (3=4) \\then (1) \\else (2)";
562: try {
563: t = parseTerm(s1);
564: } catch (Exception e) {
565: fail();
566: }
567: assertTrue("Failed parsing integer ifEx-then-else term",
568: t.op() == Op.IF_EX_THEN_ELSE
569: && t.varsBoundHere(0).size() == 1
570: && t.sub(0).equals(parseTerm("3=4"))
571: && t.sub(1).equals(parseTerm("1"))
572: && t.sub(2).equals(parseTerm("2")));
573:
574: String s2 = "\\ifEx int x; (3=4 & 1=1) \\then (\\if (3=4) \\then (1) \\else (2)) \\else (2)";
575: try {
576: t2 = parseTerm(s2);
577: } catch (Exception e) {
578: fail();
579: }
580: assertTrue(
581: "Failed parsing nested integer ifEx-then-else term",
582: t2.op() == Op.IF_EX_THEN_ELSE
583: && t.varsBoundHere(0).size() == 1
584: && t2.sub(0).equals(parseTerm("3=4 & 1=1"))
585: && t2
586: .sub(1)
587: .equals(
588: parseTerm("\\if (3=4) \\then (1) \\else (2)"))
589: && t2.sub(2).equals(parseTerm("2")));
590:
591: String s3 = "\\ifEx (int x; int y) (x=y) \\then (1=2) \\else (2=3)";
592: try {
593: t = parseTerm(s3);
594: } catch (Exception e) {
595: fail();
596: }
597: assertTrue("Failed parsing propositional ifEx-then-else term",
598: t.op() == Op.IF_EX_THEN_ELSE
599: && t.sub(0).op() == Op.EQUALS
600: && t.sub(0).sub(0).op() == t.varsBoundHere(0)
601: .getQuantifiableVariable(0)
602: && t.sub(0).sub(1).op() == t.varsBoundHere(0)
603: .getQuantifiableVariable(1)
604: && t.sub(1).equals(parseTerm("1=2"))
605: && t.sub(2).equals(parseTerm("2=3")));
606:
607: }
608:
609: public void testInfix1() {
610: assertEquals("infix1", parseTerm("aa + bb"),
611: parseTerm("add(aa,bb)"));
612: }
613:
614: public void testInfix2() {
615: assertEquals("infix2", parseTerm("aa + bb*cc"),
616: parseTerm("add(aa,mul(bb,cc))"));
617: }
618:
619: public void testInfix3() {
620: assertEquals("infix3", parseTerm("aa + bb*cc < 123 + -90"),
621: parseTerm("lt(add(aa,mul(bb,cc)),add(123,-90))"));
622: }
623:
624: public void testInfix4() {
625: assertEquals("infix4", parseTerm("aa%bb*cc < -123"),
626: parseTerm("lt(mul(mod(aa,bb),cc),-123)"));
627: }
628:
629: public void testCast() {
630: assertEquals("cast stronger than plus", parseTerm("(int)3+2"),
631: parseTerm("((int)3)+2"));
632: }
633:
634: public void testUnnecessaryIntersectionSort() {
635: // AZ is a subsort of Z,
636: TacletForTests.getJavaInfo().readJavaBlock("{}");
637: r2k.parseSpecialClasses();
638: r2k
639: .readCompilationUnit("class Z { } "
640: + "class SubZ extends Z {} "
641: + "class AZ extends Z {} ");
642: boolean unneccessaryIntersectionSortDetected = false;
643: try {
644: parseDecls("\\sorts { \\inter(AZ,Z); }");
645: } catch (Exception e) {
646: assertTrue("expected KeYSemanticException, but is "
647: + e.getCause(),
648: ((ExceptionHandlerException) (e.getCause()))
649: .getCause() instanceof KeYSemanticException);
650: unneccessaryIntersectionSortDetected = true;
651:
652: }
653:
654: assertTrue(
655: "The given intersection sort is unnecessary as it is equal to one "
656: + "of its components and"
657: + "should not be parsed.",
658: unneccessaryIntersectionSortDetected);
659:
660: try {
661: parseDecls("\\sorts { \\inter(AZ, SubZ); }");
662: } catch (Exception e) {
663: fail("failed to parse intersection sort." + e);
664: }
665:
666: }
667:
668: public void testIntersectionSort() {
669: // AZ is a subsort of Z,
670: TacletForTests.getJavaInfo().readJavaBlock("{}");
671: nss = TacletForTests.getNamespaces();
672: r2k = new Recoder2KeY(TacletForTests.getJavaInfo()
673: .getKeYProgModelInfo().getServConf(), TacletForTests
674: .getJavaInfo().rec2key(), nss, TacletForTests
675: .services().getTypeConverter());
676: }
677:
678: public void testModifies() {
679: TacletForTests.getJavaInfo().readJavaBlock("{}");
680: r2k.parseSpecialClasses();
681: r2k
682: .readCompilationUnit("class ZMod { static ZMod z; int a; int[] b; }");
683:
684: SetOfLocationDescriptor locs = null;
685: try {
686: locs = parseModifies("{\\for ZMod x; x.a@(ZMod), "
687: + "\\for int i; \\if(0 <= i & i <= 7) ZMod.z.b@(ZMod)[i], "
688: + "ZMod.z.b@(ZMod)[0..7]}");
689: } catch (Exception e) {
690: fail("Error parsing modifies clause. " + e);
691: }
692: assertTrue("Modifies should contain 3 elements", (locs != null)
693: && (locs.size() == 3));
694: }
695: }
|