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.Function;
022: import de.uka.ilkd.key.logic.op.SchemaVariable;
023: import de.uka.ilkd.key.logic.op.SortedSchemaVariable;
024: import de.uka.ilkd.key.logic.sort.*;
025:
026: public class TestDeclParser extends TestCase {
027:
028: NamespaceSet nss;
029: Services serv;
030:
031: public TestDeclParser(String name) {
032: super (name);
033: }
034:
035: public void setUp() {
036: nss = new NamespaceSet();
037: serv = new Services();
038: Recoder2KeY r2k = new Recoder2KeY(serv, nss);
039: r2k.parseSpecialClasses();
040: }
041:
042: private KeYParser stringParser(String s) {
043: return new KeYParser(
044: ParserMode.DECLARATION,
045: new KeYLexer(new StringReader(s), null),
046: "No file. Call of parser from parser/TestDeclParser.java",
047: serv, nss);
048: }
049:
050: public void parseDecls(String s) {
051: try {
052: KeYParser p = stringParser(s);
053: p.decls();
054: } catch (Exception e) {
055: StringWriter sw = new StringWriter();
056: PrintWriter pw = new PrintWriter(sw);
057: e.printStackTrace(pw);
058: throw new RuntimeException("Exc while Parsing:\n" + sw);
059: }
060: }
061:
062: public void testSortDecl() {
063: parseDecls("\\sorts { elem; list; }");
064: assertEquals("find sort elem", new Name("elem"), nss.sorts()
065: .lookup(new Name("elem")).name());
066: assertEquals("find sort list", new Name("list"), nss.sorts()
067: .lookup(new Name("list")).name());
068: }
069:
070: protected GenericSort checkGenericSort(Named p_n, SetOfSort p_ext,
071: SetOfSort p_oneof) {
072: assertTrue("Generic sort does not exist", p_n != null);
073: assertTrue("Generic sort does not have type GenericSort, but "
074: + p_n.getClass(), p_n instanceof GenericSort);
075:
076: GenericSort gs = (GenericSort) p_n;
077:
078: assertEquals("Generic sort has wrong supersorts", p_ext, gs
079: .extendsSorts());
080: assertEquals("Generic sort has wrong oneof-list", p_oneof, gs
081: .getOneOf());
082:
083: return gs;
084: }
085:
086: protected Sort checkSort(Named p_n) {
087: assertTrue("Sort does not exist", p_n != null);
088: assertTrue("Sort does not have type Sort, but "
089: + p_n.getClass(), p_n instanceof Sort);
090:
091: return (Sort) p_n;
092: }
093:
094: public void testGenericSortDecl() {
095: Named n;
096: GenericSort G, H;
097: Sort S, T;
098:
099: nss = new NamespaceSet();
100: parseDecls("\\sorts { \\generic G; \\generic H \\extends G; }");
101:
102: G = checkGenericSort(nss.sorts().lookup(new Name("G")),
103: SetAsListOfSort.EMPTY_SET, SetAsListOfSort.EMPTY_SET);
104: H = checkGenericSort(nss.sorts().lookup(new Name("H")),
105: SetAsListOfSort.EMPTY_SET.add(G),
106: SetAsListOfSort.EMPTY_SET);
107:
108: nss = new NamespaceSet();
109: parseDecls("\\sorts { S; \\generic G; \\generic H \\extends G, S; }");
110:
111: S = checkSort(nss.sorts().lookup(new Name("S")));
112: G = checkGenericSort(nss.sorts().lookup(new Name("G")),
113: SetAsListOfSort.EMPTY_SET, SetAsListOfSort.EMPTY_SET);
114: H = checkGenericSort(nss.sorts().lookup(new Name("H")),
115: SetAsListOfSort.EMPTY_SET.add(S).add(G),
116: SetAsListOfSort.EMPTY_SET);
117:
118: nss = new NamespaceSet();
119: parseDecls("\\sorts { S; T; \\generic H \\oneof {S, T}; }");
120:
121: S = checkSort(nss.sorts().lookup(new Name("S")));
122: T = checkSort(nss.sorts().lookup(new Name("T")));
123: H = checkGenericSort(nss.sorts().lookup(new Name("H")),
124: SetAsListOfSort.EMPTY_SET, SetAsListOfSort.EMPTY_SET
125: .add(S).add(T));
126:
127: nss = new NamespaceSet();
128: parseDecls("\\sorts { S; T; \\generic G; \\generic H \\oneof {S} \\extends T, G; }");
129:
130: S = checkSort(nss.sorts().lookup(new Name("S")));
131: T = checkSort(nss.sorts().lookup(new Name("T")));
132: G = checkGenericSort(nss.sorts().lookup(new Name("G")),
133: SetAsListOfSort.EMPTY_SET, SetAsListOfSort.EMPTY_SET);
134: H = checkGenericSort(nss.sorts().lookup(new Name("H")),
135: SetAsListOfSort.EMPTY_SET.add(T).add(G),
136: SetAsListOfSort.EMPTY_SET.add(S));
137:
138: nss = new NamespaceSet();
139: parseDecls("\\sorts { S, T; \\generic G,G2; \\generic H,H2 \\oneof {S} \\extends T, G; }");
140:
141: S = checkSort(nss.sorts().lookup(new Name("S")));
142: T = checkSort(nss.sorts().lookup(new Name("T")));
143: G = checkGenericSort(nss.sorts().lookup(new Name("G")),
144: SetAsListOfSort.EMPTY_SET, SetAsListOfSort.EMPTY_SET);
145: checkGenericSort(nss.sorts().lookup(new Name("G2")),
146: SetAsListOfSort.EMPTY_SET, SetAsListOfSort.EMPTY_SET);
147: H = checkGenericSort(nss.sorts().lookup(new Name("H")),
148: SetAsListOfSort.EMPTY_SET.add(T).add(G),
149: SetAsListOfSort.EMPTY_SET.add(S));
150: checkGenericSort(nss.sorts().lookup(new Name("H2")),
151: SetAsListOfSort.EMPTY_SET.add(T).add(G),
152: SetAsListOfSort.EMPTY_SET.add(S));
153:
154: nss = new NamespaceSet();
155: String str = "\\sorts { \\generic G; \\generic H \\oneof {G}; }";
156: try {
157: KeYParser p = stringParser(str);
158: p.decls();
159:
160: fail("Expected an GenericSortException");
161: } catch (Exception e) {
162: assertTrue(
163: "Expected a GenericSortException",
164: e instanceof de.uka.ilkd.key.parser.GenericSortException
165: || e.getCause() instanceof de.uka.ilkd.key.parser.GenericSortException);
166: }
167: }
168:
169: /** asserts that the found object is a schemavariable and
170: * that the allowed macthing type is QuantifiableVariable
171: */
172: public void assertVariableSV(String msg, Object o) {
173: assertTrue("The named object: " + o + " is of type "
174: + o.getClass()
175: + ", but the type SchemaVariable was expected",
176: o instanceof SchemaVariable);
177:
178: assertTrue(msg, ((SchemaVariable) o).isVariableSV());
179: }
180:
181: /** asserts that the SchemaVariable matches to term but not to a
182: * formula
183: */
184: public void assertTermSV(String msg, Object o) {
185:
186: assertTrue("The named object: " + o + " is of type "
187: + o.getClass()
188: + ", but the type SchemaVariable was expected",
189: o instanceof SchemaVariable);
190: assertSame(msg, ((SchemaVariable) o).matchType(), Term.class);
191: assertTrue(
192: "Schemavariable is not allowed to match a term of sort FORMULA.",
193: ((SortedSchemaVariable) o).sort() != Sort.FORMULA);
194: }
195:
196: /** asserts that the SchemaVariable matches to a formula
197: * and not to a term (of sort != Sort.FORMULA)
198: */
199: public void assertFormulaSV(String msg, Object o) {
200: assertTrue("The named object: " + o + " is of type "
201: + o.getClass()
202: + ", but the type SchemaVariable was expected",
203: o instanceof SchemaVariable);
204: assertSame(msg, ((SchemaVariable) o).matchType(), Term.class);
205: assertSame("Only matches to terms of sort FORMULA allowed. "
206: + "But term has sort "
207: + ((SortedSchemaVariable) o).sort(),
208: ((SortedSchemaVariable) o).sort(), Sort.FORMULA);
209:
210: }
211:
212: public void testArrayDecl() {
213: parseDecls("\\sorts { aSort;}\n" + "\\functions {\n"
214: + " aSort[][] f(aSort);\n" + "}\n");
215: Sort aSort = (Sort) nss.sorts().lookup(new Name("aSort"));
216: Sort objectSort = serv.getJavaInfo().getJavaLangObjectAsSort();
217: Sort cloneableSort = serv.getJavaInfo()
218: .getJavaLangCloneableAsSort();
219: Sort serializableSort = serv.getJavaInfo()
220: .getJavaIoSerializableAsSort();
221: Sort aSortArr = ArraySortImpl.getArraySort(aSort, objectSort,
222: cloneableSort, serializableSort);
223: Sort aSortArr2 = ArraySortImpl.getArraySort(aSortArr,
224: objectSort, cloneableSort, serializableSort);
225: assertTrue("aSort[] should extend Cloneable ", aSortArr
226: .extendsSorts().contains(cloneableSort));
227: assertTrue("aSort[] should transitively extend Object ",
228: aSortArr.extendsTrans(objectSort));
229: assertTrue("aSort[][] should transitively extend Object ",
230: aSortArr2.extendsTrans(objectSort));
231: assertTrue("aSort[][] should transitively extend Cloneable ",
232: aSortArr2.extendsTrans(cloneableSort));
233: assertTrue("aSort[][] should extend Cloneable[] ", aSortArr2
234: .extendsSorts().contains(
235: ArraySortImpl.getArraySort(cloneableSort,
236: objectSort, cloneableSort,
237: serializableSort)));
238: assertTrue("Cloneable should extend Object ", cloneableSort
239: .extendsSorts().contains(objectSort));
240: }
241:
242: public void testFunctionDecl() {
243: parseDecls("\\sorts { elem; list; }\n" + "\\functions {\n"
244: + " elem head(list);\n" + " list tail(list);\n"
245: + " elem[] tailarray(elem[]);\n" + " list nil;\n"
246: + " list cons(elem,list);\n" + "}\n");
247:
248: Sort elem = (Sort) nss.sorts().lookup(new Name("elem"));
249: Sort list = (Sort) nss.sorts().lookup(new Name("list"));
250:
251: Sort objectSort = serv.getJavaInfo().getJavaLangObjectAsSort();
252: Sort cloneableSort = serv.getJavaInfo()
253: .getJavaLangCloneableAsSort();
254: Sort serializableSort = serv.getJavaInfo()
255: .getJavaIoSerializableAsSort();
256:
257: assertEquals("find head function", new Name("head"), nss
258: .functions().lookup(new Name("head")).name());
259: assertEquals("head arity", 1, ((Function) nss.functions()
260: .lookup(new Name("head"))).arity());
261: assertEquals("head arg sort 0", list, ((Function) nss
262: .functions().lookup(new Name("head"))).argSort(0));
263: assertEquals("head return sort", elem, ((Function) nss
264: .functions().lookup(new Name("head"))).sort());
265:
266: assertEquals("find tail function", new Name("tail"), nss
267: .functions().lookup(new Name("tail")).name());
268: assertEquals("tail arity", 1, ((Function) nss.functions()
269: .lookup(new Name("tail"))).arity());
270: assertEquals("tail arg sort 0", list, ((Function) nss
271: .functions().lookup(new Name("tail"))).argSort(0));
272: assertEquals("tail return sort", list, ((Function) nss
273: .functions().lookup(new Name("tail"))).sort());
274: assertEquals("tailarray arg sort 0", ArraySortImpl
275: .getArraySort(elem, objectSort, cloneableSort,
276: serializableSort),
277:
278: ((Function) nss.functions().lookup(new Name("tailarray")))
279: .argSort(0));
280: assertEquals("tailarray return sort", ArraySortImpl
281: .getArraySort(elem, objectSort, cloneableSort,
282: serializableSort), ((Function) nss.functions()
283: .lookup(new Name("tailarray"))).sort());
284:
285: assertEquals("find nil function", new Name("nil"), nss
286: .functions().lookup(new Name("nil")).name());
287: assertEquals("nil arity", 0, ((Function) nss.functions()
288: .lookup(new Name("nil"))).arity());
289: assertEquals("nil return sort", list, ((Function) nss
290: .functions().lookup(new Name("nil"))).sort());
291:
292: assertEquals("find cons function", new Name("cons"), nss
293: .functions().lookup(new Name("cons")).name());
294: assertEquals("cons arity", 2, ((Function) nss.functions()
295: .lookup(new Name("cons"))).arity());
296: assertEquals("cons arg sort 0", elem, ((Function) nss
297: .functions().lookup(new Name("cons"))).argSort(0));
298: assertEquals("cons arg sort 1", list, ((Function) nss
299: .functions().lookup(new Name("cons"))).argSort(1));
300: assertEquals("cons return sort", list, ((Function) nss
301: .functions().lookup(new Name("cons"))).sort());
302: }
303:
304: public void testPredicateDecl() {
305: parseDecls("\\sorts { elem; list; }\n" + "\\predicates {\n"
306: + " isEmpty(list);\n" + " contains(list,elem);\n"
307: + " maybe;\n" + "}\n");
308:
309: Sort elem = (Sort) nss.sorts().lookup(new Name("elem"));
310: Sort list = (Sort) nss.sorts().lookup(new Name("list"));
311:
312: assertEquals("find isEmpty predicate", new Name("isEmpty"), nss
313: .functions().lookup(new Name("isEmpty")).name());
314: assertEquals("isEmpty arity", 1, ((Function) nss.functions()
315: .lookup(new Name("isEmpty"))).arity());
316: assertEquals("isEmpty arg sort 0", list, ((Function) nss
317: .functions().lookup(new Name("isEmpty"))).argSort(0));
318: assertEquals(
319: "isEmpty return sort",
320: Sort.FORMULA,
321: ((Function) nss.functions().lookup(new Name("isEmpty")))
322: .sort());
323:
324: assertEquals("find contains predicate", new Name("contains"),
325: nss.functions().lookup(new Name("contains")).name());
326: assertEquals("contains arity", 2, ((Function) nss.functions()
327: .lookup(new Name("contains"))).arity());
328: assertEquals("contains arg sort 0", list, ((Function) nss
329: .functions().lookup(new Name("contains"))).argSort(0));
330: assertEquals("contains arg sort 1", elem, ((Function) nss
331: .functions().lookup(new Name("contains"))).argSort(1));
332: assertEquals("contains return sort", Sort.FORMULA,
333: ((Function) nss.functions()
334: .lookup(new Name("contains"))).sort());
335:
336: assertEquals("find maybe predicate", new Name("maybe"), nss
337: .functions().lookup(new Name("maybe")).name());
338: assertEquals("maybe arity", 0, ((Function) nss.functions()
339: .lookup(new Name("maybe"))).arity());
340: assertEquals("maybe return sort", Sort.FORMULA, ((Function) nss
341: .functions().lookup(new Name("maybe"))).sort());
342: }
343:
344: public void testSVDecl() {
345: parseDecls("\\sorts { elem; list; }\n"
346: + "\\schemaVariables {\n"
347: + " \\program Statement #s ; \n"
348: + " \\term elem x,y ;\n" + " \\variables list lv ;\n"
349: + " \\formula b;\n" + "}\n");
350:
351: Sort elem = (Sort) nss.sorts().lookup(new Name("elem"));
352: Sort list = (Sort) nss.sorts().lookup(new Name("list"));
353:
354: assertEquals("find SV x", new Name("x"), nss.variables()
355: .lookup(new Name("x")).name());
356: assertTermSV("SV x type", nss.variables().lookup(new Name("x")));
357: assertEquals("SV x sort", elem, ((SortedSchemaVariable) nss
358: .variables().lookup(new Name("x"))).sort());
359:
360: assertEquals("find SV ", new Name("y"), nss.variables().lookup(
361: new Name("y")).name());
362: assertTermSV("SV y type", nss.variables().lookup(new Name("y")));
363: assertEquals("SV y sort", elem, ((SortedSchemaVariable) nss
364: .variables().lookup(new Name("y"))).sort());
365:
366: assertEquals("find SV ", new Name("lv"), nss.variables()
367: .lookup(new Name("lv")).name());
368: assertVariableSV("SV lv type", nss.variables().lookup(
369: new Name("lv")));
370: assertEquals("SV lv sort", list, ((SortedSchemaVariable) nss
371: .variables().lookup(new Name("lv"))).sort());
372:
373: assertEquals("find SV ", new Name("b"), nss.variables().lookup(
374: new Name("b")).name());
375: assertFormulaSV("SV b type", nss.variables().lookup(
376: new Name("b")));
377: assertEquals("SV b sort", Sort.FORMULA,
378: ((SortedSchemaVariable) nss.variables().lookup(
379: new Name("b"))).sort());
380: }
381:
382: public void testAmbigiousDecls() {
383: try {
384: stringParser(
385: "\\sorts { elem; list; }\n" + "\\functions {"
386: + "elem x;" + "elem fn;" + "elem p;" + "}"
387: + "\\predicates {" + "fn(elem);" + "y;"
388: + "p;" + "}" + "\\schemaVariables {\n"
389: + " \\program Statement #s ; \n"
390: + " \\term elem x,y ;\n"
391: + " \\variables list lv ;\n"
392: + " \\formula b;\n" + "}\n").decls();
393: fail("Parsed in ambigious declaration");
394: } catch (AmbigiousDeclException ade) {
395: // everything ok
396: } catch (RuntimeException e) {
397: if (!(e.getCause() instanceof AmbigiousDeclException)) {
398: fail("Unexpected excpetion. Testcase failed." + e);
399: }
400: } catch (antlr.TokenStreamException tse) {
401: fail("Unexpected excpetion. Testcase failed." + tse);
402: } catch (antlr.RecognitionException re) {
403: fail("Unexpected excpetion. Testcase failed." + re);
404: }
405:
406: }
407:
408: public void testHeurDecl() {
409: parseDecls("\\heuristicsDecl { bool; shoot_foot; }");
410: assertEquals("find heuristic bool", new Name("bool"), nss
411: .ruleSets().lookup(new Name("bool")).name());
412: assertEquals("find heuristic shoot_foot",
413: new Name("shoot_foot"), nss.ruleSets().lookup(
414: new Name("shoot_foot")).name());
415: }
416:
417: }
|