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: /** these tests are used to control if the collision mechanisms work
012: * correct. Collisions may be: collisions between variablesv, with the
013: * context or or inside formula- and termsvs
014: */package de.uka.ilkd.key.rule;
015:
016: import junit.framework.TestCase;
017: import de.uka.ilkd.key.java.Services;
018: import de.uka.ilkd.key.logic.*;
019: import de.uka.ilkd.key.logic.op.*;
020: import de.uka.ilkd.key.logic.sort.Sort;
021: import de.uka.ilkd.key.proof.*;
022: import de.uka.ilkd.key.rule.inst.SVInstantiations;
023:
024: public class TestCollisionResolving extends TestCase {
025:
026: Sort s;
027: Goal goal;
028: Services services;
029:
030: public TestCollisionResolving(String name) {
031: super (name);
032: }
033:
034: public void setUp() {
035: TacletForTests.setStandardFile(TacletForTests.testRules);
036: TacletForTests.parse();
037: s = (Sort) TacletForTests.getSorts().lookup(new Name("s"));
038:
039: services = new Services();
040:
041: //build a goal (needed for creating TacletInstantiationsTableModel)
042: Proof proof = new Proof(services);
043: Semisequent empty = Semisequent.EMPTY_SEMISEQUENT;
044: Sequent seq = Sequent.createSequent(empty, empty);
045:
046: Node node = new Node(proof, seq);
047: TacletIndex tacletIndex = new TacletIndex();
048: BuiltInRuleAppIndex builtInRuleAppIndex = new BuiltInRuleAppIndex(
049: null);
050: RuleAppIndex ruleAppIndex = new RuleAppIndex(tacletIndex,
051: builtInRuleAppIndex);
052: goal = new Goal(node, ruleAppIndex);
053: }
054:
055: public void tearDown() {
056: s = null;
057: goal = null;
058: services = null;
059: }
060:
061: public void testCollisionResolvingOfSchemaVariable() {
062: // the term has to be built manually because we have to ensure
063: // object equality of the LogicVariable x
064: LogicVariable x = new LogicVariable(new Name("x"), s);
065: Function p = new RigidFunction(new Name("p"), Sort.FORMULA,
066: new Sort[] { s });
067: Function q = new RigidFunction(new Name("q"), Sort.FORMULA,
068: new Sort[] { s });
069:
070: Term t_x = TermFactory.DEFAULT.createVariableTerm(x);
071: Term t_p_x = TermFactory.DEFAULT.createFunctionTerm(p, t_x);
072: Term t_q_x = TermFactory.DEFAULT.createFunctionTerm(q, t_x);
073:
074: Term t_all_p_x = TermFactory.DEFAULT.createQuantifierTerm(
075: Op.ALL, x, t_p_x);
076: Term t_ex_q_x = TermFactory.DEFAULT.createQuantifierTerm(Op.EX,
077: x, t_q_x);
078: Term term = TermFactory.DEFAULT.createJunctorTerm(Op.AND,
079: t_all_p_x, t_ex_q_x);
080: FindTaclet coll_varSV = (FindTaclet) TacletForTests.getTaclet(
081: "TestCollisionResolving_coll_varSV").taclet();
082:
083: TacletApp result = NoPosTacletApp.createNoPosTacletApp(
084: coll_varSV, coll_varSV.match(term, coll_varSV.find(),
085: MatchConditions.EMPTY_MATCHCONDITIONS, null,
086: Constraint.BOTTOM));
087:
088: SchemaVariable b = (SchemaVariable) TacletForTests
089: .getVariables().lookup(new Name("b"));
090: SchemaVariable c = (SchemaVariable) TacletForTests
091: .getVariables().lookup(new Name("c"));
092: SchemaVariable u = (SchemaVariable) TacletForTests
093: .getVariables().lookup(new Name("u"));
094: SchemaVariable v = (SchemaVariable) TacletForTests
095: .getVariables().lookup(new Name("v"));
096:
097: SVInstantiations insts = result.instantiations();
098: assertTrue(
099: "Same object for different conceptual variables",
100: ((Term) insts.getInstantiation(b)).sub(0).op() != ((Term) insts
101: .getInstantiation(c)).sub(0).op());
102: assertSame(((Term) insts.getInstantiation(u)).op(),
103: ((Term) insts.getInstantiation(b)).sub(0).op());
104: assertSame(((Term) insts.getInstantiation(v)).op(),
105: ((Term) insts.getInstantiation(c)).sub(0).op());
106: }
107:
108: public void testCollisionResolvingWithContext() {
109: // the term has to be built manually because we have to ensure
110: // object equality of the LogicVariable x
111: LogicVariable x = new LogicVariable(new Name("x"), s);
112: Function p = new RigidFunction(new Name("p"), Sort.FORMULA,
113: new Sort[] { s });
114: Function q = new RigidFunction(new Name("q"), Sort.FORMULA,
115: new Sort[] { s });
116:
117: Term t_x = TermFactory.DEFAULT.createVariableTerm(x);
118: Term t_p_x = TermFactory.DEFAULT.createFunctionTerm(p, t_x);
119: Term t_q_x = TermFactory.DEFAULT.createFunctionTerm(q, t_x);
120:
121: Term t_ex_q_x = TermFactory.DEFAULT.createQuantifierTerm(Op.EX,
122: x, t_q_x);
123:
124: Term t_px_and_exxqx = TermFactory.DEFAULT.createJunctorTerm(
125: Op.AND, t_p_x, t_ex_q_x);
126: Term term = TermFactory.DEFAULT.createQuantifierTerm(Op.ALL, x,
127: t_px_and_exxqx);
128:
129: FindTaclet coll_varSV = (FindTaclet) TacletForTests.getTaclet(
130: "TestCollisionResolving_coll_context").taclet();
131:
132: PosInOccurrence pos = new PosInOccurrence(
133: new ConstrainedFormula(term), PosInTerm.TOP_LEVEL
134: .down(0), true);
135:
136: TacletApp result = PosTacletApp.createPosTacletApp(coll_varSV,
137: coll_varSV.match(term.sub(0), coll_varSV.find(),
138: MatchConditions.EMPTY_MATCHCONDITIONS, null,
139: Constraint.BOTTOM), pos);
140:
141: SchemaVariable b = (SchemaVariable) TacletForTests
142: .getVariables().lookup(new Name("b"));
143: SchemaVariable c = (SchemaVariable) TacletForTests
144: .getVariables().lookup(new Name("c"));
145: SchemaVariable u = (SchemaVariable) TacletForTests
146: .getVariables().lookup(new Name("u"));
147:
148: SVInstantiations insts = result.instantiations();
149: assertTrue(
150: "Same object for different conceptual variables",
151: ((Term) insts.getInstantiation(b)).sub(0).op() != ((Term) insts
152: .getInstantiation(c)).sub(0).op());
153: assertSame(((Term) insts.getInstantiation(u)).op(),
154: ((Term) insts.getInstantiation(c)).sub(0).op());
155: }
156:
157: public void testVarNamespaceCreationWithContext() {
158: Term term = TacletForTests.parseTerm("\\forall s x; p(x)");
159:
160: FindTaclet taclet = (FindTaclet) TacletForTests.getTaclet(
161: "TestCollisionResolving_ns1").taclet();
162: PosInOccurrence pos = new PosInOccurrence(
163: new ConstrainedFormula(term), PosInTerm.TOP_LEVEL
164: .down(0), true);
165: TacletApp app = PosTacletApp.createPosTacletApp(taclet, taclet
166: .match(term.sub(0), taclet.find(),
167: MatchConditions.EMPTY_MATCHCONDITIONS, null,
168: Constraint.BOTTOM), pos);
169: TacletApp app1 = app.prepareUserInstantiation();
170: assertSame(app, app1);
171: TacletInstantiationsTableModel instModel = new TacletInstantiationsTableModel(
172: app, TacletForTests.services(), TacletForTests
173: .getNamespaces(), TacletForTests.getAbbrevs(),
174: goal);
175:
176: boolean exceptionthrown = false;
177: try {
178: app = instModel.createTacletAppFromVarInsts();
179: } catch (IllegalStateException e) {
180: exceptionthrown = true;
181: } catch (SVInstantiationException ipe) {
182: exceptionthrown = true;
183: }
184: assertTrue(
185: "Calling the creation of TacletApps before Input should "
186: + "throw exception", exceptionthrown);
187:
188: instModel.setValueAt("x", 1, 1);
189:
190: try {
191: app = instModel.createTacletAppFromVarInsts();
192: } catch (Exception e) {
193: fail("The exception " + e + "has not been expected.");
194: }
195:
196: assertNotNull(app);
197: }
198:
199: public void testVarNamespaceCreationWithPrefix() {
200: TacletApp app = (NoPosTacletApp) TacletForTests
201: .getTaclet("TestCollisionResolving_ns2");
202: TacletApp app1 = app.prepareUserInstantiation();
203: assertSame(app, app1);
204:
205: TacletInstantiationsTableModel instModel = new TacletInstantiationsTableModel(
206: app, services, TacletForTests.getNamespaces(),
207: TacletForTests.getAbbrevs(), goal);
208: boolean exceptionthrown = false;
209: try {
210: app = instModel.createTacletAppFromVarInsts();
211: } catch (IllegalStateException e) {
212: exceptionthrown = true;
213: } catch (SVInstantiationException ipe) {
214: exceptionthrown = true;
215: }
216: assertTrue(
217: "Calling the creation of TacletApps before Input should "
218: + "throw exception", exceptionthrown);
219: SchemaVariable u = (SchemaVariable) TacletForTests
220: .getVariables().lookup(new Name("u"));
221: if (instModel.getValueAt(0, 0) == u) {
222: instModel.setValueAt("x", 0, 1);
223: instModel.setValueAt("f(x)", 1, 1);
224: } else {
225: instModel.setValueAt("f(x)", 0, 1);
226: instModel.setValueAt("x", 1, 1);
227: }
228: try {
229: app = instModel.createTacletAppFromVarInsts();
230: } catch (Exception e) {
231: fail("The exception " + e + "has not been expected.");
232: }
233: assertNotNull(app);
234:
235: }
236:
237: public void testNameConflict1() {
238: Services services = new Services();
239: SchemaVariable u = (SchemaVariable) TacletForTests
240: .getVariables().lookup(new Name("u"));
241: SchemaVariable v = (SchemaVariable) TacletForTests
242: .getVariables().lookup(new Name("v"));
243: FindTaclet taclet = (FindTaclet) TacletForTests.getTaclet(
244: "TestCollisionResolving_name_conflict").taclet();
245: Semisequent semiseq = Semisequent.EMPTY_SEMISEQUENT.insert(
246: 0,
247: new ConstrainedFormula(TacletForTests
248: .parseTerm("\\forall s x; p(x)")))
249: .semisequent().insert(
250: 1,
251: new ConstrainedFormula(TacletForTests
252: .parseTerm("\\exists s x; p(x)")))
253: .semisequent();
254: Sequent seq = Sequent.createSuccSequent(semiseq);
255: PosInOccurrence pos = new PosInOccurrence(semiseq.get(0),
256: PosInTerm.TOP_LEVEL, false);
257:
258: NoPosTacletApp app0 = NoPosTacletApp
259: .createNoPosTacletApp(taclet);
260: app0 = app0.matchFind(pos, semiseq.get(0).constraint(),
261: services, Constraint.BOTTOM);
262: app0 = (NoPosTacletApp) app0.findIfFormulaInstantiations(seq,
263: services, Constraint.BOTTOM).head();
264: TacletApp app = app0.setPosInOccurrence(pos);
265: /*
266: ListOfSVInstantiations sviList=taclet.matchIf
267: (seq, taclet.match(semiseq.get(0).formula(), taclet.find(),
268: MatchConditions.EMPTY_MATCHCONDITIONS,
269: null, Constraint.BOTTOM), null);
270: TacletApp app
271: = PosTacletApp.createPosTacletApp(taclet, sviList.head(), pos);
272: */
273: TacletApp app1 = app.prepareUserInstantiation();
274: assertTrue(
275: "A different TacletApp should have been created to resolve"
276: + " name conflicts", app != app1);
277:
278: assertTrue(
279: "The names of the instantiations of u and v should be different",
280: !(((Term) app1.instantiations().getInstantiation(u))
281: .op().name().equals(((Term) app1
282: .instantiations().getInstantiation(v)).op()
283: .name())));
284: }
285:
286: public void testNameConflictAfterInput() {
287:
288: TacletApp app = (NoPosTacletApp) TacletForTests
289: .getTaclet("TestCollisionResolving_name_conflict2");
290: TacletApp app1 = app.prepareUserInstantiation();
291: assertSame(app, app1);
292:
293: TacletInstantiationsTableModel instModel = new TacletInstantiationsTableModel(
294: app, services, TacletForTests.getNamespaces(),
295: TacletForTests.getAbbrevs(), goal);
296: boolean exceptionthrown = false;
297: try {
298: app = instModel.createTacletAppFromVarInsts();
299: } catch (IllegalStateException e) {
300: exceptionthrown = true;
301: } catch (SVInstantiationException ipe) {
302: exceptionthrown = true;
303: }
304: assertTrue(
305: "Calling the creation of TacletApps before Input should "
306: + "throw exception", exceptionthrown);
307: SchemaVariable u = (SchemaVariable) TacletForTests
308: .getVariables().lookup(new Name("u"));
309: SchemaVariable v = (SchemaVariable) TacletForTests
310: .getVariables().lookup(new Name("v"));
311: SchemaVariable w0 = (SchemaVariable) TacletForTests
312: .getVariables().lookup(new Name("w0"));
313: for (int i = 0; i < 3; i++) {
314: if (instModel.getValueAt(i, 0) == u) {
315: instModel.setValueAt("x", i, 1);
316: }
317: if (instModel.getValueAt(i, 0) == v) {
318: instModel.setValueAt("x", i, 1);
319: }
320: if (instModel.getValueAt(i, 0) == w0) {
321: instModel.setValueAt("f(x)", i, 1);
322: }
323: }
324: exceptionthrown = false;
325: try {
326: app = instModel.createTacletAppFromVarInsts();
327: } catch (IllegalStateException e) {
328: exceptionthrown = true;
329: } catch (SVInstantiationException ipe) {
330: exceptionthrown = true;
331: }
332: assertTrue(
333: "As names of instantiations of VarSVs u and v in prefix of w0"
334: + "are equal, an exception should be thrown.",
335: exceptionthrown);
336: // next attempt
337: for (int i = 0; i < 3; i++) {
338: if (instModel.getValueAt(i, 0) == u) {
339: instModel.setValueAt("y", i, 1);
340: }
341: if (instModel.getValueAt(i, 0) == v) {
342: instModel.setValueAt("x", i, 1);
343: }
344: if (instModel.getValueAt(i, 0) == w0) {
345: instModel.setValueAt("f(x)", i, 1);
346: }
347: }
348: try {
349: app = instModel.createTacletAppFromVarInsts();
350: } catch (Exception e) {
351: fail("The exception " + e + "has not been expected.");
352: }
353:
354: assertNotNull("Correct instantiation input should be honored!",
355: app);
356: }
357:
358: /* COMMENTED OUT! It has to be checked if the instantiation checking is to restrictive.
359: public void testNameConflictWithContext() {
360:
361: SchemaVariable v
362: = (SchemaVariable) TacletForTests.getVariables().lookup(new Name("v"));
363: FindTaclet taclet = (FindTaclet) TacletForTests.getTaclet
364: ("TestCollisionResolving_name_conflict_with_context").taclet();
365: Semisequent semiseq
366: = Semisequent.EMPTY_SEMISEQUENT
367: .insert(0, new ConstrainedFormula(TacletForTests.parseTerm("ex x:s"
368: +".p(x)")))
369: .insert(1, new ConstrainedFormula(TacletForTests.parseTerm("all x:s"
370: +".p(x)")));
371: Sequent seq=Sequent.createSuccSequent(semiseq);
372: PosInOccurrence pos=new PosInOccurrence(semiseq.get(1),
373: PosInTerm.TOP_LEVEL.down(0),
374: seq);
375: ListOfSVInstantiations sviList=taclet.matchIf
376: (seq, taclet.match(semiseq.get(1).formula().sub(0), taclet.find(),
377: taclet.createInitialInstantiation()));
378: TacletApp app
379: = PosTacletApp.createPosTacletApp(taclet, sviList.head(), pos);
380: TacletApp app1=app.prepareUserInstantiation();
381: assertTue("A different TacletApp should have been created to resolve"
382: +" name conflicts", app!=app1);
383: assertTrue("The names of x and the instantiations of v should be different",
384: !(new Name("x")).equals
385: (((Term)app1.instantiations().getInstantiation(v)).op().name()));
386:
387: }
388:
389: */
390:
391: public void testNameConflictWithContextAfterInput() {
392:
393: FindTaclet taclet = (FindTaclet) TacletForTests.getTaclet(
394: "TestCollisionResolving_name_conflict_with_context2")
395: .taclet();
396: Term term = TacletForTests.parseTerm("\\forall s x; p(x)");
397: PosInOccurrence pos = new PosInOccurrence(
398: new ConstrainedFormula(term), PosInTerm.TOP_LEVEL
399: .down(0), true);
400: MatchConditions mc = taclet.match(term.sub(0), taclet.find(),
401: MatchConditions.EMPTY_MATCHCONDITIONS, null,
402: Constraint.BOTTOM);
403: TacletApp app = PosTacletApp
404: .createPosTacletApp(taclet, mc, pos);
405: TacletApp app1 = app.prepareUserInstantiation();
406: assertSame("Actually there are no conflicts yet.", app, app1);
407: TacletInstantiationsTableModel instModel = new TacletInstantiationsTableModel(
408: app, services, TacletForTests.getNamespaces(),
409: TacletForTests.getAbbrevs(), goal);
410: boolean exceptionthrown = false;
411: try {
412: app = instModel.createTacletAppFromVarInsts();
413: } catch (IllegalStateException e) {
414: exceptionthrown = true;
415: } catch (SVInstantiationException ipe) {
416: exceptionthrown = true;
417: }
418: assertTrue(
419: "Calling the creation of TacletApps before Input should "
420: + "throw exception", exceptionthrown);
421: SchemaVariable v = (SchemaVariable) TacletForTests
422: .getVariables().lookup(new Name("v"));
423: SchemaVariable w0 = (SchemaVariable) TacletForTests
424: .getVariables().lookup(new Name("w0"));
425: for (int i = 1; i < 3; i++) {
426: if (instModel.getValueAt(i, 0) == v) {
427: instModel.setValueAt("x", i, 1);
428: }
429: if (instModel.getValueAt(i, 0) == w0) {
430: instModel.setValueAt("f(x)", i, 1);
431: }
432: }
433: exceptionthrown = false;
434: try {
435: app = instModel.createTacletAppFromVarInsts();
436: } catch (IllegalStateException e) {
437: exceptionthrown = true;
438: } catch (SVInstantiationException ipe) {
439: exceptionthrown = true;
440: }
441: assertTrue(
442: "As names of x and instantiations of VarSV v in prefix of w0"
443: + "are equal, an exception should be thrown.",
444: exceptionthrown);
445: // next attempt
446: for (int i = 1; i < 3; i++) {
447: if (instModel.getValueAt(i, 0) == v) {
448: instModel.setValueAt("y", i, 1);
449: }
450: if (instModel.getValueAt(i, 0) == w0) {
451: instModel.setValueAt("f(x)", i, 1);
452: }
453: }
454: try {
455: app = instModel.createTacletAppFromVarInsts();
456: } catch (Exception e) {
457: fail("The exception " + e + "has not been expected.");
458: }
459: assertNotNull("Correct instantiation input should be honored!",
460: app);
461:
462: }
463:
464: }
|