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: // This file is part of KeY - Integrated Deductive Software Design
010: // Copyright (C) 2001-2003 Universitaet Karlsruhe, Germany
011: // and Chalmers University of Technology, Sweden
012: //
013: // The KeY system is protected by the GNU General Public License.
014: // See LICENSE.TXT for details.
015: //
016:
017: package de.uka.ilkd.key.parser;
018:
019: import java.io.PrintWriter;
020: import java.io.StringReader;
021: import java.io.StringWriter;
022:
023: import junit.framework.TestCase;
024: import de.uka.ilkd.key.java.Services;
025: import de.uka.ilkd.key.logic.Name;
026: import de.uka.ilkd.key.logic.NamespaceSet;
027: import de.uka.ilkd.key.logic.Term;
028: import de.uka.ilkd.key.logic.TermFactory;
029: import de.uka.ilkd.key.logic.op.*;
030: import de.uka.ilkd.key.logic.sort.Sort;
031: import de.uka.ilkd.key.logic.sort.oclsort.OclSort;
032: import de.uka.ilkd.key.proof.init.InitConfig;
033: import de.uka.ilkd.key.proof.init.OCLInvSimplPO;
034: import de.uka.ilkd.key.rule.TacletForTests;
035:
036: /** class tests the parser for Taclets
037: */
038:
039: public class TestTacletParserOCL extends TestCase {
040:
041: private NamespaceSet nss;
042: private Services services;
043: private TermFactory tf = TermFactory.DEFAULT;
044: private Sort ocl_sort;
045: private TermSymbol forAll, iterate, and, true_, nil;
046: private SortedSchemaVariable x, g, coll, expr, init, e1, genExpr;
047: private Term nilTerm, trueTerm;
048:
049: public TestTacletParserOCL(String name) {
050: super (name);
051: }
052:
053: //
054: // set up
055: //
056:
057: public void setUp() {
058: services = TacletForTests.services();
059: InitConfig initConf = new InitConfig();
060: OCLInvSimplPO.createNamespaceSetForTests(initConf);
061:
062: x = (SortedSchemaVariable) SchemaVariableFactory
063: .createVariableSV(new Name("x"), OclSort.OCLANY, false);
064: initConf.varNS().add(x);
065:
066: g = (SortedSchemaVariable) SchemaVariableFactory
067: .createVariableSV(new Name("g"), OclSort.OCLGENERIC,
068: false);
069: initConf.varNS().add(g);
070:
071: genExpr = (SortedSchemaVariable) SchemaVariableFactory
072: .createTermSV(new Name("genExpr"), OclSort.OCLGENERIC,
073: false, true, false);
074: initConf.varNS().add(genExpr);
075:
076: coll = (SortedSchemaVariable) SchemaVariableFactory
077: .createTermSV(new Name("coll"),
078: OclSort.COLLECTION_OF_OCLANY, false, true,
079: false);
080: initConf.varNS().add(coll);
081:
082: expr = (SortedSchemaVariable) SchemaVariableFactory
083: .createTermSV(new Name("expr"), OclSort.BOOLEAN, false,
084: true, false);
085: initConf.varNS().add(expr);
086:
087: init = (SortedSchemaVariable) SchemaVariableFactory
088: .createTermSV(new Name("init"), OclSort.OCLGENERIC,
089: false, true, false);
090: initConf.varNS().add(init);
091:
092: e1 = (SortedSchemaVariable) SchemaVariableFactory.createTermSV(
093: new Name("e1"), OclSort.OCLANY, false, true, false);
094: initConf.varNS().add(e1);
095:
096: forAll = (TermSymbol) initConf.funcNS().lookup(
097: new Name("$forAll"));
098: and = (TermSymbol) initConf.funcNS().lookup(new Name("$and"));
099: nil = (TermSymbol) initConf.funcNS().lookup(
100: new Name("$empty_set"));
101: iterate = (TermSymbol) initConf.funcNS().lookup(
102: new Name("$iterate"));
103: true_ = (TermSymbol) initConf.funcNS()
104: .lookup(new Name("$true"));
105:
106: nss = initConf.namespaces();
107:
108: nilTerm = tf.createFunctionTerm(nil);
109: trueTerm = tf.createFunctionTerm(true_);
110: }
111:
112: //
113: // Utility Methods for test cases.
114: //
115: private KeYParser stringTacletParser(String s) {
116: return new KeYParser(ParserMode.TACLET, new KeYLexer(
117: new StringReader(s), null),
118: "No file. parser/TestTacletParser.stringTacletParser("
119: + s + ")", tf, services, nss);
120: }
121:
122: public Term parseTerm(String s) {
123: try {
124: KeYParser p = stringTacletParser(s);
125: return p.term();
126: } catch (Exception e) {
127: StringWriter sw = new StringWriter();
128: PrintWriter pw = new PrintWriter(sw);
129: e.printStackTrace(pw);
130: throw new RuntimeException("Exc while Parsing:\n" + sw);
131: }
132: }
133:
134: //
135: // Test cases.
136: //
137:
138: //Tests OCL operations where one variable gets bound (forAll, exists, select, ...)
139: //Only for the problem clause of the .key file, where bound vars are treated as
140: //logical vars (not schema vars)
141: /*
142: // WATCHOUT Daniel - this test is wrong
143: public void test1() {
144: Term tParse = parseTerm("$forAll($empty_set, \\bind OclBoolean s; $and($true, s))");
145: LogicVariable this_s
146: = (LogicVariable)tParse.varsBoundHere(1).getQuantifiableVariable(0);
147: ArrayOfQuantifiableVariable[] var = new ArrayOfQuantifiableVariable[2];
148: var[0] = new ArrayOfQuantifiableVariable(new QuantifiableVariable[0]);
149: var[1] = new ArrayOfQuantifiableVariable(new LogicVariable[]{this_s});
150: Term tS = tf.createVariableTerm(this_s);
151: Term tAnd = tf.createFunctionTerm(and, trueTerm, tS);
152: Term term = tf.createFunctionWithBoundVarsTerm(forAll, new Term[]{nilTerm, tAnd}, var);
153: assertEquals("parse $forAll($empty_set, \\bind OclBoolean s; $and($true, s))",
154: term,
155: tParse);
156: assertTrue(!services.getExceptionHandler().error());
157: }
158: */
159:
160: //Tests the OCL operation where two variables get bound -- iterate
161: //Only for the problem clause of the .key file, where bound vars are treated as
162: //logical vars (not schema vars)
163: /*
164: // WATCHOUT Daniel - this test is wrong
165: public void test2() {
166: Term tParse = parseTerm("$iterate($empty_set," +
167: "$true, \\bind(OclBoolean s; OclBoolean acc) $and(s, acc))");
168: LogicVariable this_s
169: = (LogicVariable)tParse.varsBoundHere(2).getQuantifiableVariable(0);
170: LogicVariable this_acc
171: = (LogicVariable)tParse.varsBoundHere(2).getQuantifiableVariable(1);
172: ArrayOfQuantifiableVariable[] var = new ArrayOfQuantifiableVariable[3];
173: var[0] = new ArrayOfQuantifiableVariable(new QuantifiableVariable[0]);
174: var[1] = new ArrayOfQuantifiableVariable(new QuantifiableVariable[0]);
175: var[2] = new ArrayOfQuantifiableVariable(new LogicVariable[]{this_s, this_acc});
176: Term tS = tf.createVariableTerm(this_s);
177: Term tAcc = tf.createVariableTerm(this_acc);
178: Term tAnd = tf.createFunctionTerm(and, tS, tAcc);
179: Term term = tf.createFunctionWithBoundVarsTerm(iterate,
180: new Term[]{nilTerm, trueTerm, tAnd},
181: var);
182: assertEquals("parse $iterate($empty_set," +
183: "$true, \\bind( OclBoolean s; OclBoolean acc) $and(s, acc))",
184: term,
185: tParse);
186: }
187: */
188: //Tests OCL operations where one variable gets bound (forAll, exists, select, ...)
189: //Only for the rules clause of the .key file, where bound vars are treated as
190: //schema vars (not logical vars)
191: public void test3() {
192: ArrayOfQuantifiableVariable[] var = new ArrayOfQuantifiableVariable[2];
193: var[0] = new ArrayOfQuantifiableVariable(
194: new QuantifiableVariable[0]);
195: var[1] = new ArrayOfQuantifiableVariable(
196: new SortedSchemaVariable[] { x });
197: Term tExpr = tf.createVariableTerm(expr);
198: Term tColl = tf.createVariableTerm(coll);
199: Term term = tf.createFunctionWithBoundVarsTerm(forAll,
200: new Term[] { tColl, tExpr }, var);
201: assertEquals("parse $forAll(coll, \\bind x; expr)", term,
202: parseTerm("$forAll(coll, \\bind x; expr)"));
203: }
204:
205: //Tests the OCL operation where two variables get bound -- iterate
206: //Only for the rules clause of the .key file, where bound vars are treated as
207: //schema vars (not logical vars)
208: public void test4() {
209: ArrayOfQuantifiableVariable[] var = new ArrayOfQuantifiableVariable[3];
210: var[0] = new ArrayOfQuantifiableVariable(
211: new QuantifiableVariable[0]);
212: var[1] = new ArrayOfQuantifiableVariable(
213: new QuantifiableVariable[0]);
214: var[2] = new ArrayOfQuantifiableVariable(
215: new SortedSchemaVariable[] { x, g });
216: Term tExpr = tf.createVariableTerm(genExpr);
217: Term tColl = tf.createVariableTerm(coll);
218: Term tInit = tf.createVariableTerm(init);
219: Term term = tf.createFunctionWithBoundVarsTerm(iterate,
220: new Term[] { tColl, tInit, tExpr }, var);
221: assertEquals(
222: "parse $iterate(coll, init, \\bind( x; g) genExpr)",
223: term,
224: parseTerm("$iterate(coll, init, \\bind( x; g) genExpr)"));
225: }
226:
227: //Tests the syntax of the substitution operator (one substitution)
228: public void test5() {
229: Term tExpr = tf.createVariableTerm(expr);
230: Term tE1 = tf.createVariableTerm(e1);
231: Term term = tf.createSubstitutionTerm(Op.SUBST, x, new Term[] {
232: tE1, tExpr });
233: assertEquals("parse {x e1}expr", term,
234: parseTerm("{\\subst x; e1}expr"));
235: }
236: }
|