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: /**
018: * Tests matching and application of some OCL taclets (for OCL simplification).
019: */package de.uka.ilkd.key.rule;
020:
021: import java.io.PrintWriter;
022: import java.io.StringReader;
023: import java.io.StringWriter;
024:
025: import junit.framework.TestCase;
026: import de.uka.ilkd.key.java.Recoder2KeY;
027: import de.uka.ilkd.key.java.Services;
028: import de.uka.ilkd.key.logic.*;
029: import de.uka.ilkd.key.logic.op.*;
030: import de.uka.ilkd.key.logic.sort.GenericSort;
031: import de.uka.ilkd.key.logic.sort.oclsort.OclSort;
032: import de.uka.ilkd.key.parser.KeYLexer;
033: import de.uka.ilkd.key.parser.KeYParser;
034: import de.uka.ilkd.key.parser.ParserMode;
035: import de.uka.ilkd.key.pp.AbbrevMap;
036: import de.uka.ilkd.key.proof.*;
037: import de.uka.ilkd.key.proof.init.InitConfig;
038: import de.uka.ilkd.key.proof.init.OCLInvSimplPO;
039: import de.uka.ilkd.key.util.Debug;
040:
041: public class TestOCLTaclets extends TestCase {
042:
043: private InitConfig initConf;
044: private NamespaceSet nss;
045: private TermFactory tf = TermFactory.DEFAULT;
046: private SortedSchemaVariable x, acc, nonGenX, nonGenAcc, setSV, e1,
047: g1, g2;
048: private RuleAppIndex index;
049: private Goal goal;
050:
051: private RewriteTaclet ocl_iterateSet_step;
052: private RewriteTaclet ocl_iterateSet_empty;
053: private RewriteTaclet ocl_if_true;
054: private RewriteTaclet ocl_equals;
055:
056: public TestOCLTaclets(String name) {
057: super (name);
058: }
059:
060: public TestOCLTaclets(String name, boolean b) {
061: super (name);
062: Debug.ENABLE_DEBUG = b;
063: }
064:
065: public void setUp() {
066: initConf = new InitConfig();
067: OCLInvSimplPO.createNamespaceSetForTests(initConf);
068:
069: x = (SortedSchemaVariable) SchemaVariableFactory
070: .createVariableSV(new Name("x"), new GenericSort(
071: new Name("AnySV")), false);
072: initConf.varNS().add(x);
073: acc = (SortedSchemaVariable) SchemaVariableFactory
074: .createVariableSV(new Name("acc"), new GenericSort(
075: new Name("AnyCollSV")), false);
076: initConf.varNS().add(acc);
077: nonGenX = (SortedSchemaVariable) SchemaVariableFactory
078: .createVariableSV(new Name("nonGenX"), OclSort.OCLANY,
079: false);
080: initConf.varNS().add(nonGenX);
081: nonGenAcc = (SortedSchemaVariable) SchemaVariableFactory
082: .createVariableSV(new Name("nonGenAcc"),
083: OclSort.OCLGENERIC, false);
084: initConf.varNS().add(nonGenAcc);
085: e1 = (SortedSchemaVariable) SchemaVariableFactory.createTermSV(
086: new Name("e1"), OclSort.OCLANY, false, true, false);
087: initConf.varNS().add(e1);
088: setSV = (SortedSchemaVariable) SchemaVariableFactory
089: .createTermSV(new Name("setSV"), OclSort.SET_OF_OCLANY,
090: false, true, false);
091: initConf.varNS().add(setSV);
092: g1 = (SortedSchemaVariable) SchemaVariableFactory.createTermSV(
093: new Name("g1"), OclSort.OCLGENERIC, false, true, false);
094: initConf.varNS().add(g1);
095: g2 = (SortedSchemaVariable) SchemaVariableFactory.createTermSV(
096: new Name("g2"), OclSort.OCLGENERIC, false, true, false);
097: initConf.varNS().add(g2);
098: nss = initConf.namespaces();
099:
100: ocl_iterateSet_step = (RewriteTaclet) parseTaclet("ocl_iterateSet_step{\\find($iterate($insert_set(e1,setSV), g1, \\bind( x; acc) g2)) "
101: + "\\varcond(\\notFreeIn(x, setSV),\\notFreeIn(x, g1),\\notFreeIn(acc, setSV),\\notFreeIn(acc, g1))"
102: + "\\replacewith({\\subst x; e1}({\\subst acc; $iterate(setSV, g1, \\bind( x; acc) g2)}g2))};");
103:
104: ocl_iterateSet_empty = (RewriteTaclet) parseTaclet("ocl_iterateSet_empty{\\find($iterate($empty_set, g1, \\bind( x; acc) g2)) "
105: + "\\replacewith(g1)}");
106:
107: ocl_equals = (RewriteTaclet) parseTaclet("ocl_equals{\\find($equals(g1, g1)) \\replacewith($true)};");
108:
109: ocl_if_true = (RewriteTaclet) parseTaclet("ocl_if_true{\\find($if($true, g1, g2)) \\replacewith(g1)};");
110:
111: SetOfTaclet tacletSet = SetAsListOfTaclet.EMPTY_SET;
112: tacletSet = tacletSet.add(ocl_iterateSet_step);
113: tacletSet = tacletSet.add(ocl_iterateSet_empty);
114: tacletSet = tacletSet.add(ocl_equals);
115: tacletSet = tacletSet.add(ocl_if_true);
116: TacletIndex tacletIndex = new TacletIndex(tacletSet);
117: TacletAppIndex tacletAppIndex = new TacletAppIndex(tacletIndex);
118: BuiltInRuleIndex biri = new BuiltInRuleIndex();
119: BuiltInRuleAppIndex birai = new BuiltInRuleAppIndex(biri);
120: index = new RuleAppIndex(tacletAppIndex, birai);
121: }
122:
123: public void tearDown() {
124: initConf = null;
125: nss = null;
126: x = null;
127: acc = null;
128: nonGenX = null;
129: nonGenAcc = null;
130: setSV = null;
131: e1 = null;
132: g1 = null;
133: g2 = null;
134: index = null;
135: goal = null;
136:
137: ocl_iterateSet_step = null;
138: ocl_iterateSet_empty = null;
139: ocl_if_true = null;
140: ocl_equals = null;
141: }
142:
143: private KeYParser stringTermParser(String s) {
144: return new KeYParser(
145: ParserMode.TERM,
146: new KeYLexer(new StringReader(s), null),
147: "No file. Call of parser from parser/TestTermParser.java",
148: tf, new Recoder2KeY(TacletForTests.services(), nss),
149: TacletForTests.services(), nss, new AbbrevMap());
150: }
151:
152: public Term parseTerm(String s) {
153: try {
154: KeYParser p = stringTermParser(s);
155: return p.term();
156: } catch (Exception e) {
157: StringWriter sw = new StringWriter();
158: PrintWriter pw = new PrintWriter(sw);
159: e.printStackTrace(pw);
160: throw new RuntimeException("Exc while Parsing:\n" + sw);
161: }
162: }
163:
164: private KeYParser stringTacletParser(String s) {
165: return new KeYParser(ParserMode.TACLET, new KeYLexer(
166: new StringReader(s), null),
167: "No file. parser/TestTacletParser.stringTacletParser("
168: + s + ")", tf, TacletForTests.services(), nss);
169: }
170:
171: public Taclet parseTaclet(String s) {
172: try {
173: KeYParser p = stringTacletParser(s);
174: return p.taclet(SetAsListOfChoice.EMPTY_SET.add(new Choice(
175: new Name("Default"))));
176: } catch (Exception e) {
177: StringWriter sw = new StringWriter();
178: PrintWriter pw = new PrintWriter(sw);
179: e.printStackTrace(pw);
180: throw new RuntimeException("Exc while Parsing:\n" + sw);
181: }
182: }
183:
184: public void test1() {
185: Term t = parseTerm("$equals(\"set\", \"set\")");
186: ListOfTacletApp list = findMatchingTaclets(t);
187: TacletApp tacletApp = list.head();
188: assertNotNull("Find ocl_equals", tacletApp);
189: ListOfGoal goalList = tacletApp.execute(goal, TacletForTests
190: .services());
191: goal = goalList.head();
192: assertNotNull("Successfully apply ocl_equals", goal);
193: Term result = goal.sequent().succedent().getFirst().formula()
194: .sub(0);
195: Term expected = parseTerm("$true");
196: assertEquals(
197: "ocl_equals applied to: $equals(\"set\", \"set\")",
198: result, expected);
199: }
200:
201: public void test2() {
202: Term t = parseTerm("$if($true, $false, $true)");
203: ListOfTacletApp list = findMatchingTaclets(t);
204: TacletApp tacletApp = list.head();
205: assertNotNull("Find ocl_if", tacletApp);
206: ListOfGoal goalList = tacletApp.execute(goal, TacletForTests
207: .services());
208: goal = goalList.head();
209: assertNotNull("Successfully apply ocl_if", goal);
210: Term result = goal.sequent().succedent().getFirst().formula()
211: .sub(0);
212: Term expected = parseTerm("$false");
213: assertEquals("ocl_if applied to: $if($true, $false, $true)",
214: result, expected);
215: }
216:
217: public void test3() {
218: Term t = parseTerm("$iterate($insert_set($true, $empty_set), $false, "
219: + "\\bind(OclBoolean elem; OclBoolean accum) $and(elem, accum))");
220:
221: LogicVariable this _elem = (LogicVariable) t.varsBoundHere(2)
222: .getQuantifiableVariable(0);
223: LogicVariable this _acc = (LogicVariable) t.varsBoundHere(2)
224: .getQuantifiableVariable(1);
225:
226: ListOfTacletApp list = findMatchingTaclets(t);
227: TacletApp tacletApp = list.head();
228: assertNotNull("Find ocl_iterateSet_step", tacletApp);
229: ListOfGoal goalList = tacletApp.execute(goal, TacletForTests
230: .services());
231: goal = goalList.head();
232: assertNotNull("Successfully apply ocl_iterate_step", goal);
233: Term result = goal.sequent().succedent().getFirst().formula()
234: .sub(0);
235:
236: //Build the expected result term:
237: //$and($true,
238: // $iterate($empty_set,
239: // $false,
240: // \elem:OclBoolean\accum:OclBoolean/ $and(elem, accum)))
241: Term nilT = parseTerm("$empty_set");
242: Term falseT = parseTerm("$false");
243: Term trueT = parseTerm("$true");
244: Term elemT = TermFactory.DEFAULT.createVariableTerm(this _elem);
245: Term accT = TermFactory.DEFAULT.createVariableTerm(this _acc);
246: //TermSymbol and = TacletForTests.funcLookup("$and");
247: TermSymbol and = (TermSymbol) initConf.funcNS().lookup(
248: new Name("$and"));
249: Term andTerm2 = TermFactory.DEFAULT.createFunctionTerm(and,
250: new Term[] { elemT, accT });
251: //TermSymbol iterate = TacletForTests.funcLookup("$iterate");
252: TermSymbol iterate = (TermSymbol) initConf.funcNS().lookup(
253: new Name("$iterate"));
254: ArrayOfQuantifiableVariable[] var = new ArrayOfQuantifiableVariable[3];
255: var[0] = new ArrayOfQuantifiableVariable(
256: new QuantifiableVariable[0]);
257: var[1] = new ArrayOfQuantifiableVariable(
258: new QuantifiableVariable[0]);
259: var[2] = new ArrayOfQuantifiableVariable(new LogicVariable[] {
260: this _elem, this _acc });
261: Term iterateTerm = TermFactory.DEFAULT
262: .createFunctionWithBoundVarsTerm(iterate, new Term[] {
263: nilT, falseT, andTerm2 }, var);
264: Term expected = TermFactory.DEFAULT.createFunctionTerm(and,
265: new Term[] { trueT, iterateTerm });
266:
267: assertEquals(
268: "ocl_iterate_step applied to: $iterate($insert_set($true, $empty_set), $false, "
269: + "\\bind(OclBoolean elem; OclBoolean accum) $and(elem, accum)",
270: result, expected);
271: }
272:
273: public void test4() {
274: Term t = parseTerm("$iterate($empty_set, $false, "
275: + "\\bind(OclBoolean elem; OclBoolean accum) $and(elem, accum))");
276: ListOfTacletApp list = findMatchingTaclets(t);
277: TacletApp tacletApp = list.head();
278: assertNotNull("Find ocl_iterateSet_empty", tacletApp);
279: ListOfGoal goalList = tacletApp.execute(goal, TacletForTests
280: .services());
281: goal = goalList.head();
282: assertNotNull("Successfully apply ocl_iterateSet_empty", goal);
283: Term result = goal.sequent().succedent().getFirst().formula()
284: .sub(0);
285: Term expected = parseTerm("$false");
286: assertEquals(
287: "ocl_iterateSet_empty applied to: $iterate($empty_set, $false, "
288: + "\\bind( OclBoolean elem; OclBoolean acc) $and(elem, acc)",
289: result, expected);
290: }
291:
292: //To ensure that variable SVs of a sort A cannot match a logic variable
293: //of a sort B, if A is a supersort of B.
294: public void test5() {
295: index.tacletIndex().remove(
296: index.tacletIndex().lookup("ocl_iterateSet_step"));
297: ocl_iterateSet_step = (RewriteTaclet) parseTaclet("ocl_iterateSet_step{\\find($iterate($insert_set(e1,setSV), "
298: + "g1, \\bind(nonGenX; nonGenAcc) g2)) "
299: + "\\varcond(\\notFreeIn(nonGenX, setSV),\\notFreeIn(nonGenX, g1),\\notFreeIn(nonGenAcc, setSV),\\notFreeIn(nonGenAcc, g1))"
300: + "\\replacewith({\\subst nonGenX; e1}({\\subst nonGenAcc; $iterate(setSV, g1, \\bind( nonGenX; nonGenAcc) g2)}g2))};");
301: index.tacletIndex().add(ocl_iterateSet_step);
302: Term t = parseTerm("$iterate($insert_set($true, $empty_set), $false, "
303: + "\\bind(OclBoolean elem; OclBoolean accum) $and(elem, accum))");
304:
305: ListOfTacletApp list = findMatchingTaclets(t);
306: TacletApp tacletApp = list.head();
307: assertNull("Find ocl_iterateSet_step", tacletApp);
308: }
309:
310: private ListOfTacletApp findMatchingTaclets(Term t) {
311: TermSymbol oclWrapper = (TermSymbol) initConf.funcNS().lookup(
312: new Name("$OclWrapper"));
313: //TermSymbol oclWrapper = TacletForTests.funcLookup("$OclWrapper");
314: Term term = TermFactory.DEFAULT.createFunctionTerm(oclWrapper,
315: t);
316: ConstrainedFormula cf = new ConstrainedFormula(term);
317: Semisequent succ = Semisequent.EMPTY_SEMISEQUENT;
318: SemisequentChangeInfo info = succ.insertFirst(cf);
319: succ = info.semisequent();
320: Sequent seq = Sequent.createSuccSequent(succ);
321: Proof proof = new Proof(new Services());
322: Node node = new Node(proof, seq);
323: proof.setRoot(node);
324: proof.setSimplifier(new UpdateSimplifier());
325: goal = new Goal(node, index);
326:
327: //Matching of taclets
328: PosInOccurrence pos = new PosInOccurrence(cf,
329: PosInTerm.TOP_LEVEL.down(0), false);
330: ListOfTacletApp list = index.getTacletAppAt(TacletFilter.TRUE,
331: pos, TacletForTests.services(), Constraint.BOTTOM);
332: return list;
333: }
334: }
|