0001: // This file is part of KeY - Integrated Deductive Software Design
0002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
0003: // Universitaet Koblenz-Landau, Germany
0004: // Chalmers University of Technology, Sweden
0005: //
0006: // The KeY system is protected by the GNU General Public License.
0007: // See LICENSE.TXT for details.
0008: //
0009: //
0010:
0011: package de.uka.ilkd.key.rule;
0012:
0013: import java.io.File;
0014: import java.util.Arrays;
0015: import java.util.LinkedList;
0016:
0017: import junit.framework.TestCase;
0018: import de.uka.ilkd.key.java.Services;
0019: import de.uka.ilkd.key.java.StatementBlock;
0020: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
0021: import de.uka.ilkd.key.java.declaration.ClassDeclaration;
0022: import de.uka.ilkd.key.logic.*;
0023: import de.uka.ilkd.key.logic.op.*;
0024: import de.uka.ilkd.key.logic.sort.*;
0025: import de.uka.ilkd.key.proof.ProofAggregate;
0026: import de.uka.ilkd.key.rule.updatesimplifier.Update;
0027: import de.uka.ilkd.key.util.HelperClassForTests;
0028:
0029: /**
0030: * Class used for testing the simultaneous update simplifier. ATTENTION: If
0031: * <code>assertSame</code> is used, do not replace this test with
0032: * <code>assertEquals</code> without thinking, as we test here also if the
0033: * memory resources are wasted or not.
0034: */
0035: public class TestUpdateSimplifier extends TestCase {
0036:
0037: private Namespace variables;
0038:
0039: private Namespace functions;
0040:
0041: private Namespace sorts;
0042:
0043: private ProgramVariable[] pv;
0044:
0045: private ProgramVariable spv;
0046:
0047: private TermBuilder tb = TermBuilder.DF;
0048: private TermFactory tf = TermFactory.DEFAULT;
0049:
0050: private Sort testSort0;
0051:
0052: private Sort testSort1;
0053:
0054: private Sort testSort2;
0055:
0056: private Sort cloneable;
0057:
0058: private Sort serializable;
0059:
0060: private Sort integerSort;
0061:
0062: // t : testSort1
0063: private Term t;
0064:
0065: // i : testSort1
0066: private Term i;
0067:
0068: // o : testSort1
0069: private Term o;
0070:
0071: // u : testSort1
0072: private Term u;
0073:
0074: // r: testSort2
0075: private Term r;
0076:
0077: // o.a
0078: private Term oa;
0079:
0080: // u.a
0081: private Term ua;
0082:
0083: // r.a
0084: private Term ra;
0085:
0086: // o.spv (spv static attribute)
0087: private Term ospv;
0088:
0089: // u.spv (spv static attribute)
0090: private Term uspv;
0091:
0092: // arrays
0093: private ArraySort arraySort1;
0094:
0095: private ArraySort arraySort2;
0096:
0097: private Term a;
0098:
0099: private Term b;
0100:
0101: private Term c;
0102:
0103: // integers
0104: private Term idx;
0105:
0106: private Term jdx;
0107:
0108: private Term mdx;
0109:
0110: // a[idx] : array of testSort 1
0111: private Term ai;
0112:
0113: // a[jdx] : array of testSort 1
0114: private Term aj;
0115:
0116: // a[mdx] : array of testSort 1
0117: private Term am;
0118:
0119: // b[idx] : array of testSort 1
0120: private Term bi;
0121:
0122: // b[jdx] : array of testSort 1
0123: private Term bj;
0124:
0125: // c[idx] : array of testSort 2
0126: private Term ci;
0127:
0128: // c[jdx] : array of testSort 2
0129: private Term cj;
0130:
0131: // variables
0132:
0133: // variable of sort arraySort1
0134: private LogicVariable arrayVar1;
0135:
0136: // variables of sort integer
0137: private LogicVariable intVar;
0138:
0139: public TestUpdateSimplifier(String s) {
0140: super (s);
0141: }
0142:
0143: /**
0144: * creates an update term where the given locations are updated
0145: * this method requires detailed knowledge of the update structure as
0146: * the subterms must have the correct order.
0147: * @param locations the Location operators of the update
0148: * @param subs the array of Term with the subterms of the
0149: * locations to be updated, the values and the target term
0150: * @return the above described update term
0151: */
0152: public Term createUpdateTerm(Location[] locations, Term[] subs) {
0153: final boolean guards[] = new boolean[locations.length];
0154: Arrays.fill(guards, false);
0155:
0156: final QuanUpdateOperator op = QuanUpdateOperator
0157: .createUpdateOp(locations, guards);
0158:
0159: final ArrayOfQuantifiableVariable[] bv = new ArrayOfQuantifiableVariable[subs.length];
0160: Arrays.fill(bv, new ArrayOfQuantifiableVariable());
0161:
0162: return op.normalize(bv, subs);
0163: }
0164:
0165: private Term createUpdateTerm(Term[] subs) {
0166: Location[] loc = new Location[(subs.length - 1) / 2];
0167: LinkedList newSubs = new LinkedList();
0168: int count = 0;
0169: for (int i1 = 0; i1 < subs.length - 2; i1 += 2, count++) {
0170: loc[count] = (Location) subs[i1].op();
0171: for (int j = 0; j < subs[i1].arity(); j++) {
0172: newSubs.add(subs[i1].sub(j));
0173: }
0174: newSubs.add(subs[i1 + 1]);
0175: }
0176: newSubs.add(subs[subs.length - 1]);
0177: return createUpdateTerm(loc, (Term[]) newSubs
0178: .toArray(new Term[0]));
0179: }
0180:
0181: private void assertEqualsModRenaming(Term t1, Term expected) {
0182: assertTrue("Expected " + expected + ", but got " + t1, t1
0183: .equalsModRenaming(expected));
0184: }
0185:
0186: public void setUp() {
0187: variables = new Namespace();
0188: functions = new Namespace();
0189: sorts = new Namespace();
0190: AbstractSort intSort = new PrimitiveSort(new Name("int"));
0191: AbstractSort booleanSort = new PrimitiveSort(
0192: new Name("boolean"));
0193: sorts.add(intSort);
0194: sorts.add(booleanSort);
0195:
0196: intSort.addDefinedSymbols(functions, sorts);
0197: booleanSort.addDefinedSymbols(functions, sorts);
0198:
0199: testSort0 = new ClassInstanceSortImpl(new Name("testSort0"),
0200: false);
0201: testSort1 = new ClassInstanceSortImpl(new Name("testSort1"),
0202: testSort0, false);
0203: testSort2 = new ClassInstanceSortImpl(new Name("testSort2"),
0204: testSort0, false);
0205: cloneable = new ClassInstanceSortImpl(new Name("cloneable"),
0206: testSort1, true);
0207: serializable = new ClassInstanceSortImpl(new Name(
0208: "serializable"), testSort1, true);
0209:
0210: ((AbstractSort) testSort0).addDefinedSymbols(functions, sorts);
0211: ((AbstractSort) testSort1).addDefinedSymbols(functions, sorts);
0212: ((AbstractSort) testSort2).addDefinedSymbols(functions, sorts);
0213: ((AbstractSort) cloneable).addDefinedSymbols(functions, sorts);
0214: ((AbstractSort) serializable).addDefinedSymbols(functions,
0215: sorts);
0216:
0217: KeYJavaType kjt = new KeYJavaType(new ClassDeclaration(
0218: new ProgramElementName("Object"),
0219: new ProgramElementName("java.lang.Object")), testSort1);
0220: sorts.add(testSort0);
0221: sorts.add(testSort1);
0222: sorts.add(testSort2);
0223: sorts.add(cloneable);
0224: sorts.add(serializable);
0225:
0226: pv = new ProgramVariable[7];
0227: for (int i1 = 0; i1 < pv.length; i1++) {
0228: ProgramElementName name;
0229: switch (i1) {
0230: case 1:
0231: name = new ProgramElementName("t");
0232: break;
0233: case 2:
0234: name = new ProgramElementName("i");
0235: break;
0236: case 3:
0237: name = new ProgramElementName("o");
0238: break;
0239: case 4:
0240: name = new ProgramElementName("u");
0241: break;
0242: case 5:
0243: name = new ProgramElementName("a");
0244: break;
0245: default:
0246: name = new ProgramElementName("pv" + i1);
0247: break;
0248: }
0249: if (i1 == 5) {
0250: pv[i1] = new LocationVariable(name, kjt, kjt, false);
0251: } else {
0252: pv[i1] = new LocationVariable(name, kjt);
0253: }
0254: variables.add(pv[i1]);
0255: }
0256:
0257: spv = new LocationVariable(new ProgramElementName("spv"), kjt,
0258: kjt, true);
0259:
0260: // just initialize the parser
0261: parseTerm("{t:=i} o");
0262: // for the systematic tests
0263:
0264: t = tb.var(pv[1]);
0265: i = tb.var(pv[2]);
0266: o = tb.var(pv[3]);
0267: u = tb.var(pv[4]);
0268: ProgramVariable r_var = new LocationVariable(
0269: new ProgramElementName("r"), testSort2);
0270: r = tb.var(r_var);
0271:
0272: oa = tb.dot(o, pv[5]);
0273: ua = tb.dot(u, pv[5]);
0274: ra = tb.dot(r, pv[5]);
0275:
0276: ospv = tb.dot(o, spv);
0277: uspv = tb.dot(u, spv);
0278:
0279: arraySort1 = ArraySortImpl.getArraySort(testSort1, testSort0,
0280: cloneable, serializable);
0281: arraySort2 = ArraySortImpl.getArraySort(testSort2, testSort0,
0282: cloneable, serializable);
0283:
0284: final KeYJavaType kjt1 = new KeYJavaType(arraySort1);
0285: final KeYJavaType kjt2 = new KeYJavaType(arraySort2);
0286:
0287: ProgramVariable a_var = new LocationVariable(
0288: new ProgramElementName("_a"), kjt1);
0289: ProgramVariable b_var = new LocationVariable(
0290: new ProgramElementName("_b"), kjt1);
0291: ProgramVariable c_var = new LocationVariable(
0292: new ProgramElementName("_c"), kjt2);
0293:
0294: a = tb.var(a_var);
0295: b = tb.var(b_var);
0296: c = tb.var(c_var);
0297:
0298: integerSort = TacletForTests.services().getTypeConverter()
0299: .getIntegerLDT().targetSort();
0300: ProgramVariable idx_var = new LocationVariable(
0301: new ProgramElementName("i"), integerSort);
0302: ProgramVariable jdx_var = new LocationVariable(
0303: new ProgramElementName("j"), integerSort);
0304:
0305: ProgramVariable mdx_var = new LocationVariable(
0306: new ProgramElementName("m"), integerSort);
0307:
0308: idx = tb.var(idx_var);
0309: jdx = tb.var(jdx_var);
0310: mdx = tb.var(mdx_var);
0311:
0312: ai = tb.array(a, idx);
0313: aj = tb.array(a, jdx);
0314: am = tb.array(a, mdx);
0315:
0316: bi = tb.array(b, idx);
0317: bj = tb.array(b, jdx);
0318:
0319: ci = tb.array(c, idx);
0320: cj = tb.array(c, jdx);
0321:
0322: arrayVar1 = new LogicVariable(new Name("arrayVar1"), arraySort1);
0323: intVar = new LogicVariable(new Name("intVar"), integerSort);
0324: }
0325:
0326: public void tearDown() {
0327: variables = null;
0328: functions = null;
0329: sorts = null;
0330: }
0331:
0332: private Term parseTerm(String termstr) {
0333: return TacletForTests.parseTerm(termstr, new NamespaceSet(
0334: new Namespace(), functions, sorts, new Namespace(),
0335: new Namespace(), variables));
0336: }
0337:
0338: public void testBasicRules() {
0339: UpdateSimplifier simply = new UpdateSimplifier();
0340: Services services = TacletForTests.services();
0341:
0342: Term parsed = parseTerm("{t:=i} o");
0343: assertTrue(simply.simplify(parsed, services) == parsed
0344: .sub(parsed.arity() - 1));
0345:
0346: parsed = parseTerm("{t:=i} t");
0347: assertTrue(simply.simplify(parsed, services) == parsed
0348: .sub(parsed.arity() - 2));
0349:
0350: parsed = parseTerm("{t:=i || i:=o} t");
0351: assertTrue(simply.simplify(parsed, services).op() == pv[2]);
0352:
0353: Term[] subs = new Term[parsed.arity()];
0354: for (int i = 0; i < parsed.arity() - 1; i++) {
0355: subs[i] = parsed.sub(i);
0356: }
0357: subs[parsed.arity() - 1] = tb.dot(tb.var(pv[4]), pv[5]);
0358:
0359: // {t:=i, i:=o} u.a ~~~> u.a
0360: Term constr = createUpdateTerm(new Term[] { t, i, i, o, ua });
0361: Term simplified = simply.simplify(constr, services);
0362: Term expected = ua;
0363: assertEquals("Failed applying {t:=i, i:=o} u.a", expected,
0364: simplified);
0365: assertSame("Failed applying {t:=i, i:=o} u.a (wasted memory)",
0366: expected, simplified);
0367:
0368: // {i:=t, o.a:=i} u.a ~~~>(u?=o).a/->i
0369: constr = createUpdateTerm(new Term[] { i, t, oa, i, ua });
0370: simplified = simply.simplify(constr, services);
0371: // expected = tf.createIfElseTerm(u, o, i, ua);
0372: expected = tb.ife(tb.equals(u, o), i, ua);
0373:
0374: assertEquals("Failed applying {i:=t || o.a:=i} u.a", expected,
0375: simplified);
0376:
0377: assertSame(
0378: "Failed applying {i:=t || o.a:=i} u.a (memory wasted)",
0379: u, simplified.sub(0).sub(0));
0380: assertSame(
0381: "Failed applying {i:=t || o.a:=i} u.a (memory wasted)",
0382: o, simplified.sub(0).sub(1));
0383: assertSame(
0384: "Failed applying {i:=t || o.a:=i} u.a (memory wasted)",
0385: i, simplified.sub(1));
0386: assertSame(
0387: "Failed applying {i:=t || o.a:=i} u.a (memory wasted)",
0388: ua, simplified.sub(2));
0389:
0390: // {o.a:=u, u.a:=i} t.a ---> (t ?= u) i : (t ?= o) u : t.a
0391: Term ta = tb.dot(t, pv[5]);
0392: constr = createUpdateTerm(new Term[] { oa, u, ua, i, ta });
0393: simplified = simply.simplify(constr, services);
0394: // expected = tf.createIfElseTerm
0395: // (t, u, i, tf.createIfElseTerm(t, o, u, ta));
0396: expected = tb.ife(tb.equals(t, u), i, tb.ife(tb.equals(t, o),
0397: u, ta));
0398:
0399: assertEquals("Failed applying {o.a:=u, u.a:=i} t.a", expected,
0400: simplified);
0401: for (int i = 0; i < expected.arity(); i++) {
0402: assertSame("Memory waste detected", expected.sub(0).sub(0),
0403: simplified.sub(0).sub(0));
0404: assertSame("Memory waste detected", expected.sub(0).sub(1),
0405: simplified.sub(0).sub(1));
0406: assertSame("Memory waste detected", expected.sub(1),
0407: simplified.sub(1));
0408: assertSame("Memory waste detected", expected.sub(2).sub(0)
0409: .sub(0), simplified.sub(2).sub(0).sub(0));
0410: assertSame("Memory waste detected", expected.sub(2).sub(0)
0411: .sub(1), simplified.sub(2).sub(0).sub(1));
0412: assertSame("Memory waste detected", expected.sub(2).sub(1),
0413: simplified.sub(2).sub(1));
0414: assertSame("Memory waste detected", expected.sub(2).sub(2),
0415: simplified.sub(2).sub(2));
0416: }
0417:
0418: // {t:=i} {i:=o, o:=t}<>true ~~> {t:=i, i:=o, o:=i}<>true
0419: parsed = parseTerm("{t:=i} {i:=o || o:=t} \\<{}\\>true");
0420: expected = parseTerm("{t:=i || i:=o || o:=i} \\<{}\\>true");
0421: simplified = simply.simplify(parsed, services);
0422: assertEquals("Failed applying {t:=i} {i:=o, o:=t}<>true",
0423: expected, simplified);
0424:
0425: // {t:=i} {t:=o, o:=t}<>true ~~> {t:=o, o:=i}<>true
0426: parsed = parseTerm("{t:=i} {t:=o || o:=t} \\<{}\\>true");
0427: expected = parseTerm("{t:=o || o:=i} \\<{}\\>true");
0428: simplified = simply.simplify(parsed, services);
0429: assertEquals("Failed applying {t:=i} {t:=o, o:=t}<>true",
0430: expected, simplified);
0431:
0432: // {i.a:=t, t.a:=i, u.a:=o} t.a = t ~~>
0433: // ((t ?= u) o : i) = t
0434: subs = new Term[7];
0435: subs[0] = tb.dot(tb.var(pv[2]), pv[5]);
0436: subs[1] = tb.var(pv[1]);
0437: subs[2] = tb.dot(tb.var(pv[1]), pv[5]);
0438: subs[3] = tb.var(pv[2]);
0439: subs[4] = tb.dot(tb.var(pv[4]), pv[5]);
0440: subs[5] = tb.var(pv[3]);
0441: subs[6] = tb
0442: .equals(tb.dot(tb.var(pv[1]), pv[5]), tb.var(pv[1]));
0443:
0444: constr = createUpdateTerm(subs);
0445: expected = parseTerm("\\if (t = u) \\then (o) \\else (i)");
0446:
0447: Term[] e_subs = new Term[expected.arity()];
0448: for (int i = 0; i < expected.arity(); i++) {
0449: e_subs[i] = expected.sub(i);
0450: }
0451:
0452: expected = tb.equals(tb.ife(tb.equals(t, u), o, i), tb
0453: .var(pv[1]));
0454:
0455: simplified = simply.simplify(constr, services);
0456:
0457: assertTrue("Expected:" + expected + ", but is:" + simplified,
0458: simplified.equals(expected));
0459:
0460: }
0461:
0462: public void testApplyOnAttribute() {
0463: UpdateSimplifier simply = new UpdateSimplifier();
0464: // none-static
0465: // {o.a := pv6, t.a:=i} u.a ~~~>(u?=t) i : (u ?= o) pv6 : u.a
0466: // now:
0467: // {o.a := pv6, t.a:=i} u.a ~~~> if (u=t) (i) (if (u=o) (pv6) (u.a))
0468: Term ta = tb.dot(t, pv[5]);
0469: Term pv6 = tb.var(pv[6]);
0470: Term constr = createUpdateTerm(new Term[] { oa, pv6, ta, i, ua });
0471: Term simplified = simply.simplify(constr, TacletForTests
0472: .services());
0473:
0474: Term expected = tb.ife(tb.equals(u, t), i, tb.ife(tb.equals(u,
0475: o), pv6, ua));
0476:
0477: assertEquals(simplified, expected);
0478:
0479: }
0480:
0481: public void testDeletionStrategy() {
0482:
0483: UpdateSimplifier us = new UpdateSimplifier(true, false);
0484: Services services = TacletForTests.services();
0485:
0486: Term parsed = parseTerm("{t:=i} \\<{}\\> o=o");
0487: Term expected = parseTerm("\\<{}\\>o=o");
0488: Term result = us.simplify(parsed, services);
0489: assertTrue("Expected:" + expected + "\n Is:" + result,
0490: result == parsed.sub(parsed.arity() - 1));
0491:
0492: parsed = parseTerm("{t:=i || o:=a}\\<{}\\>t=t");
0493: result = us.simplify(parsed, services);
0494: expected = parseTerm("{t:=i}\\<{}\\> t=t");
0495: assertTrue("Expected: " + expected + "\n Is: " + result, result
0496: .equals(expected));
0497:
0498: parsed = parseTerm("{t:=i || o:=a || u:=u}\\<{}\\> t=t");
0499: result = us.simplify(parsed, services);
0500: expected = parseTerm("{t:=i}\\<{}\\>t=t");
0501: assertTrue("Expected: " + expected + "\n Is: " + result, result
0502: .equals(expected));
0503:
0504: parsed = parseTerm("{t:=i || o:=a || u:=u}\\<{}\\>u=u");
0505: result = us.simplify(parsed, services);
0506: expected = parseTerm("\\<{}\\>u=u");
0507: assertTrue("Expected: " + expected + "\n Is: " + result, result
0508: .equals(expected));
0509:
0510: // {t:=i, o:=a, u:=u}<{ o = o; }> t=t -->
0511: // {t:=i, o:=a} <{ o = o; }> t=t
0512: parsed = parseTerm("{t:=i || o:=a || u:=u}\\<{ o = o; }\\> t=t");
0513: result = us.simplify(parsed, services);
0514: expected = parseTerm("{t:=i || o:=a}\\<{ o = o; }\\> t=t");
0515:
0516: assertEquals(
0517: "Failed deletion of unused var (or simple updates) in "
0518: + "{t:=i || o:=a || u:=u}<{ o = o; }> t=t",
0519: expected, result);
0520:
0521: parsed = parseTerm("{t:=i || o:=a || u:=o} \\<{}\\> t=u");
0522: result = us.simplify(parsed, services);
0523: expected = parseTerm("{t:=i || u:=o}\\<{}\\> t=u");
0524: assertEquals("Failed deletion of unused var in "
0525: + "{t:=i || o:=a || u:=o} t=u", expected, result);
0526:
0527: }
0528:
0529: public void testSimultaneousUpdateEquality() {
0530: Term cmp1 = parseTerm("{t:=i || o:=a || u:=o} true");
0531: Term cmp2 = parseTerm("{o:=a || u:=o || t:=i} true");
0532:
0533: assertTrue("ProgramVariables commute.", cmp1.equals(cmp2));
0534: }
0535:
0536: public void testApplicationOnAttributeNoneSim() {
0537:
0538: UpdateSimplifier simply = new UpdateSimplifier();
0539:
0540: Term loc1 = tb.dot(tb.var(pv[4]), pv[5]);
0541: Term loc2 = tb.dot(tb.var(pv[3]), pv[5]);
0542: Term val = tb.var(pv[2]);
0543:
0544: // {p4.p5 := i} {p3.p5 := i} (p4.p5 = p3.p5)
0545:
0546: Term constr = createUpdateTerm(new Term[] {
0547: loc1,
0548: val,
0549: createUpdateTerm(new Term[] { loc2, val,
0550: tb.equals(loc2, loc1) }) });
0551: Term simplified = simply.simplify(constr, TacletForTests
0552: .services());
0553: Term expected = tf.createEqualityTerm(val, val);
0554: assertEquals(
0555: "Error applying non-simultaneous updates on attributes.",
0556: expected, simplified);
0557: }
0558:
0559: public void testApplicationOnAttributeSim() {
0560:
0561: UpdateSimplifier simply = new UpdateSimplifier();
0562:
0563: Term loc1 = tb.dot(tb.var(pv[4]), pv[5]);
0564: Term loc2 = tb.dot(tb.var(pv[3]), pv[5]);
0565: Term val = tb.var(pv[2]);
0566:
0567: // {u.a := i} {p3.a := i} (p4.p5 = p3.a)
0568:
0569: Term constr = createUpdateTerm(new Term[] { loc1, val, loc2,
0570: val, tb.equals(loc2, loc1) });
0571: Term simplified = simply.simplify(constr, TacletForTests
0572: .services());
0573: Term expected = tf.createEqualityTerm(val, val);
0574: assertEquals(
0575: "Error applying simultaneous update on attributes.",
0576: expected, simplified);
0577: }
0578:
0579: public void testBugInUStarComputation() {
0580: UpdateSimplifier simply = new UpdateSimplifier();
0581:
0582: Term p4p5 = tb.dot(tb.var(pv[4]), pv[5]);
0583: Term p1 = tb.var(pv[1]);
0584: Term p2 = tb.var(pv[2]);
0585:
0586: // {t:=u.a || u.a := i} {u.a := t} <>(i=i)
0587:
0588: Term constr = createUpdateTerm(new Term[] {
0589: p1,
0590: p4p5,
0591: p4p5,
0592: p2,
0593: createUpdateTerm(new Term[] {
0594: p4p5,
0595: p1,
0596: tb.dia(JavaBlock
0597: .createJavaBlock(new StatementBlock()),
0598: tb.equals(p2, p2)) }) });
0599: Term simplified = simply.simplify(constr, TacletForTests
0600: .services());
0601: Term expected = createUpdateTerm(new Term[] {
0602: p1,
0603: p4p5,
0604: p4p5,
0605: p4p5,
0606: tb.dia(JavaBlock.createJavaBlock(new StatementBlock()),
0607: tb.equals(p2, p2)) });
0608: assertEquals("Error when merging updates.", expected,
0609: simplified);
0610: }
0611:
0612: public void xtestBugInDeleteTrivialUpdates() {
0613: // deletion of updates has been wrong for the folowing case:
0614: // {o1.a:=c || o2.a:=o2.a} phi
0615: // previously o2.a:=o2.a has been deleted, but that is wrong, if o1=o2
0616:
0617: UpdateSimplifier simply = new UpdateSimplifier();
0618:
0619: Term p3p5 = tb.dot(tb.var(pv[3]), pv[5]);
0620: Term p4p5 = tb.dot(tb.var(pv[4]), pv[5]);
0621: Term p1 = tb.var(pv[1]);
0622: Term p2 = tb.var(pv[2]);
0623:
0624: // {o.a:=t || u.a := u.a} <>(t=i)
0625:
0626: Term constr = createUpdateTerm(new Term[] {
0627: p3p5,
0628: p1,
0629: p4p5,
0630: p4p5,
0631: tb.dia(JavaBlock.createJavaBlock(new StatementBlock()),
0632: tb.equals(p2, p2)) });
0633:
0634: Term simplified = simply.simplify(constr, TacletForTests
0635: .services());
0636: Term expected = constr;
0637: assertEquals(
0638: "Trivial updates may only be deleted if it is safe.",
0639: expected, simplified);
0640: }
0641:
0642: // more systematic tests
0643:
0644: /**
0645: * tests the application of
0646: * <ul>
0647: * <li> {o := t} o </li>
0648: * <li> {o := t} u </li>
0649: * <li> {o := t} o.a </li>
0650: * <li> {o := t} u.a </li>
0651: * <li> {o := t} r.a </li>
0652: * <li> {a := b} a[i] </li>
0653: * <li> {a := b} c[i] </li>
0654: * <li> {i := j} a[i] </li>
0655: * </ul>
0656: */
0657: public void testBaseLocalVariableApplications() {
0658: UpdateSimplifier simply = new UpdateSimplifier();
0659: Services services = TacletForTests.services();
0660:
0661: // {o:=t} o
0662: Term constr = createUpdateTerm(new Term[] { o, t, o });
0663: Term simplified = simply.simplify(constr, services);
0664: Term expected = t;
0665: assertEquals("Failed applying {o := t} o ", expected,
0666: simplified);
0667: // {o := t} u
0668: constr = createUpdateTerm(new Term[] { o, t, u });
0669: simplified = simply.simplify(constr, services);
0670: expected = u;
0671: assertEquals("Failed applying {o := t} u (o,u compatible) ",
0672: expected, simplified);
0673:
0674: // {o := t} r
0675: constr = createUpdateTerm(new Term[] { o, t, r });
0676: simplified = simply.simplify(constr, services);
0677: expected = r;
0678: assertEquals(
0679: "Failed applying {o := t} r (o, r not compatible) ",
0680: expected, simplified);
0681:
0682: // {o := t} o.a
0683: constr = createUpdateTerm(new Term[] { o, t, oa });
0684: simplified = simply.simplify(constr, services);
0685: expected = tb.dot(t, pv[5]);
0686: assertEquals("Failed applying {o := t} o.a", expected,
0687: simplified);
0688:
0689: // {o := t} u.a
0690: constr = createUpdateTerm(new Term[] { o, t, ua });
0691: simplified = simply.simplify(constr, services);
0692: expected = ua;
0693: assertEquals("Failed applying {o := t} u.a (o, u compatible) ",
0694: expected, simplified);
0695: // {o := t} r.a
0696: constr = createUpdateTerm(new Term[] { o, t, ra });
0697: simplified = simply.simplify(constr, services);
0698: expected = ra;
0699: assertEquals(
0700: "Failed applying {o := t} r.a (o, r not compatible) ",
0701: expected, simplified);
0702:
0703: // {a := b} a[i]
0704: constr = createUpdateTerm(new Term[] { a, b, ai });
0705: simplified = simply.simplify(constr, services);
0706: expected = bi;
0707: assertEquals("Failed applying {a := b} a[i] ", expected,
0708: simplified);
0709:
0710: // {a := b} b[i]
0711: constr = createUpdateTerm(new Term[] { a, b, ai });
0712: simplified = simply.simplify(constr, services);
0713: expected = bi;
0714: assertEquals("Failed applying {a := b} b[i] (a, b compatible)",
0715: expected, simplified);
0716:
0717: // {a := b} c[i]
0718: constr = createUpdateTerm(new Term[] { a, b, ci });
0719: simplified = simply.simplify(constr, services);
0720: expected = ci;
0721: assertEquals(
0722: "Failed applying {a := b} c[i] (a, c not compatible) ",
0723: expected, simplified);
0724:
0725: // {i := j} a[i]
0726: constr = createUpdateTerm(new Term[] { idx, jdx, ai });
0727: simplified = simply.simplify(constr, services);
0728: expected = aj;
0729: assertEquals(
0730: "Failed applying {i := j} a[i] (o, r not compatible) ",
0731: expected, simplified);
0732:
0733: }
0734:
0735: /**
0736: * tests the application of
0737: * <ul>
0738: * <li> {o.a := t} o.a </li>
0739: * <li> {o.a := t} u.a (u compatible to o) </li>
0740: * <li> {o.a := t} r.a (r not compatible to o) </li>
0741: * <li> {o.a := t} i </li>
0742: * <li> {o.a := t} a[i] </li>
0743: * </ul>
0744: */
0745: public void testBaseAttributeApplications() {
0746: UpdateSimplifier simply = new UpdateSimplifier();
0747: Services services = TacletForTests.services();
0748:
0749: // {o.a:=t} o.a
0750: Term constr = createUpdateTerm(new Term[] { oa, t, oa });
0751: Term simplified = simply.simplify(constr, services);
0752: Term expected = t;
0753: assertEquals("Failed applying {o.a := t} o.a ", expected,
0754: simplified);
0755:
0756: // {o.a:=t} u.a
0757: constr = createUpdateTerm(new Term[] { oa, t, ua });
0758: simplified = simply.simplify(constr, services);
0759: expected = tb.ife(tb.equals(u, o), t, ua);
0760: assertEquals(
0761: "Failed applying {o.a := t} u.a (o, u compatible) ",
0762: expected, simplified);
0763:
0764: // {o.a:=t} r.a
0765: constr = createUpdateTerm(new Term[] { oa, t, ra });
0766: simplified = simply.simplify(constr, services);
0767: expected = ra;
0768: assertEquals(
0769: "Failed applying {o.a := t} r.a (o, r not compatible) ",
0770: expected, simplified);
0771:
0772: // {o.a:=t} i
0773: constr = createUpdateTerm(new Term[] { oa, t, i });
0774: simplified = simply.simplify(constr, services);
0775: expected = i;
0776: assertEquals("Failed applying {o.a := t} i ", expected,
0777: simplified);
0778:
0779: // {o.a:=t} a[i]
0780: constr = createUpdateTerm(new Term[] { oa, t, ai });
0781: simplified = simply.simplify(constr, services);
0782: expected = ai;
0783: assertEquals("Failed applying {o.a := t} a[i] ", expected,
0784: simplified);
0785:
0786: // {o.a:=t} a[i]
0787: constr = createUpdateTerm(new Term[] { oa, t, ai });
0788: simplified = simply.simplify(constr, services);
0789: expected = ai;
0790: assertEquals("Failed applying {o.a := t} a[i] ", expected,
0791: simplified);
0792: }
0793:
0794: /**
0795: * tests the application of
0796: * <ul>
0797: * <li> {a[i] := t} a[i] </li>
0798: * <li> {a[i] := t} a[j] </li>
0799: * <li> {a[i] := t} b[i] (a compatible to b) </li>
0800: * <li> {a[i] := t} b[j] (a compatible to b) </li>
0801: * <li> {a[i] := t} c[j] (a not compatible to c) </li>
0802: * <li> {a[i] := t} o.a </li>
0803: * <li> {a[i] := t} i </li>
0804: * </ul>
0805: */
0806: public void testBaseArrayApplications() {
0807: UpdateSimplifier simply = new UpdateSimplifier();
0808: Services services = TacletForTests.services();
0809:
0810: // {a[i]:=t} a[i]
0811: Term constr = createUpdateTerm(new Term[] { ai, t, ai });
0812: Term simplified = simply.simplify(constr, services);
0813: Term expected = t;
0814: assertEquals("Failed applying {a[i] := t} a[i] ", expected,
0815: simplified);
0816:
0817: // {a[i]:=t} a[j]
0818: constr = createUpdateTerm(new Term[] { ai, t, aj });
0819: simplified = simply.simplify(constr, services);
0820: expected = tb.ife(tb.equals(jdx, idx), t, aj);
0821: assertEquals("Failed applying {a[i] := t} a[j] ", expected,
0822: simplified);
0823:
0824: // {a[i]:=t} b[i]
0825: constr = createUpdateTerm(new Term[] { ai, t, bi });
0826: simplified = simply.simplify(constr, services);
0827: expected = tb.ife(tb.equals(b, a), t, bi);
0828: assertEquals("Failed applying {a[i] := t} b[i] "
0829: + "(a, b compatible) ", expected, simplified);
0830:
0831: // {a[i]:=t} b[j]
0832: constr = createUpdateTerm(new Term[] { ai, t, bj });
0833: simplified = simply.simplify(constr, services);
0834: expected = tb.ife(tb.and(tb.equals(b, a), tb.equals(jdx, idx)),
0835: t, bj);
0836: assertEquals("Failed applying {a[i] := t} b[j] "
0837: + "(a, b compatible) ", expected, simplified);
0838:
0839: // {a[i]:=t} c[j]
0840: constr = createUpdateTerm(new Term[] { ai, t, cj });
0841: simplified = simply.simplify(constr, services);
0842: expected = cj;
0843: assertEquals("Failed applying {a[i] := t} c[j] "
0844: + "(a, c not compatible) ", expected, simplified);
0845:
0846: // {a[i]:=t} o.a
0847: constr = createUpdateTerm(new Term[] { ai, t, oa });
0848: simplified = simply.simplify(constr, services);
0849: expected = oa;
0850: assertEquals("Failed applying {a[i] := t} o.a ", expected,
0851: simplified);
0852:
0853: // {a[i]:=t} t
0854: constr = createUpdateTerm(new Term[] { ai, t, t });
0855: simplified = simply.simplify(constr, services);
0856: expected = t;
0857: assertEquals("Failed applying {a[i] := t} t ", expected,
0858: simplified);
0859:
0860: // {a[i]:=t} a
0861: constr = createUpdateTerm(new Term[] { ai, t, a });
0862: simplified = simply.simplify(constr, services);
0863: expected = a;
0864: assertEquals("Failed applying {a[i] := t} a ", expected,
0865: simplified);
0866: }
0867:
0868: /**
0869: * tests the application of
0870: * <ul>
0871: * <li> {a := b} {a[i] := o} <> true </li>
0872: * <li> {i := j} {a[i] := o} <> true </li>
0873: * <li> {a[i] := t} {a[i] := o} <> true </li>
0874: * <li> {a[i] := t} {b[i] := o} <> true (a, b compatible) </li>
0875: * <li> {a[i] := t} {c[i] := o} <> true (a, c not compatible)</li>
0876: * <li> {a[i] := t} {o := a[i]} <> true </li>
0877: * <li> {a[i] := t} {o := a[j]} <> true </li>
0878: * <li> {o.a := t} {o.a := o } <> true </li>
0879: * <li> {o.a := t} {o.a.a := o} <> true </li>
0880: * <li> {o.a := t} {o.a.a := o.a} <> true </li>
0881: * <li> {o.a := t} {u.a := u.a} <> true </li>
0882: * <li> {o.a := t} {r.a := r.a} <> true </li>
0883: * <li> {o.a := t} {r.a.a := o} <> true </li>
0884: * </ul>
0885: */
0886: public void testMergeSingleUpdates() {
0887: UpdateSimplifier simply = new UpdateSimplifier();
0888: Services services = TacletForTests.services();
0889: Term diaTrue = tb.dia(JavaBlock
0890: .createJavaBlock(new StatementBlock()), tb.tt());
0891:
0892: // {a := b} {a[i] := o} <> true
0893: Term constr = createUpdateTerm(new Term[] { a, b,
0894: createUpdateTerm(new Term[] { ai, o, diaTrue }) });
0895: Term simplified = simply.simplify(constr, services);
0896: Term expected = createUpdateTerm(new Term[] { a, b, bi, o,
0897: diaTrue });
0898:
0899: assertEquals("Failed applying {a := b} {a[i] := o} <> true",
0900: expected, simplified);
0901:
0902: // {i := j} {a[i] := o} <> true
0903: constr = createUpdateTerm(new Term[] { idx, jdx,
0904: createUpdateTerm(new Term[] { ai, o, diaTrue }) });
0905: simplified = simply.simplify(constr, services);
0906: expected = createUpdateTerm(new Term[] { idx, jdx, aj, o,
0907: diaTrue });
0908:
0909: assertEquals("Failed applying {i := j} {a[i] := o} <> true",
0910: expected, simplified);
0911:
0912: // {a[i] := t} {a[i] := o} <> true
0913: constr = createUpdateTerm(new Term[] { ai, t,
0914: createUpdateTerm(new Term[] { ai, o, diaTrue }) });
0915: simplified = simply.simplify(constr, services);
0916: expected = createUpdateTerm(new Term[] { ai, o, diaTrue });
0917:
0918: assertEquals("Failed applying {i := j} {a[i] := o} <> true",
0919: expected, simplified);
0920:
0921: // {a[i] := t} {b[i] := o} <> true (a, b compatible)
0922: constr = createUpdateTerm(new Term[] { ai, t,
0923: createUpdateTerm(new Term[] { bi, o, diaTrue }) });
0924: simplified = simply.simplify(constr, services);
0925: /*
0926: * expected = createUpdateTerm (new Term[]{ai, tf.createConjCondTerm(new
0927: * Term[]{a, idx, t, b, idx, ai}), bi, o, diaTrue});
0928: */// skipped this kind of improvement
0929: expected = createUpdateTerm(new Term[] { ai, t, bi, o, diaTrue });
0930:
0931: assertEquals("Failed applying {a[i] := t} {b[i] := o} <> true"
0932: + "(a,b compatible)", expected, simplified);
0933:
0934: // {a[i] := t} {c[i] := o} <> true (a, c not compatible)
0935: constr = createUpdateTerm(new Term[] { ai, t,
0936: createUpdateTerm(new Term[] { ci, o, diaTrue }) });
0937: simplified = simply.simplify(constr, services);
0938: expected = createUpdateTerm(new Term[] { ai, t, ci, o, diaTrue });
0939: assertEquals("Failed applying {a[i] := t} {c[i] := o} <> true"
0940: + "(a, c not compatible)", expected, simplified);
0941:
0942: // {a[i] := t} {o := a[i]} <> true
0943: constr = createUpdateTerm(new Term[] { ai, t,
0944: createUpdateTerm(new Term[] { o, ai, diaTrue }) });
0945: simplified = simply.simplify(constr, services);
0946: expected = createUpdateTerm(new Term[] { ai, t, o, t, diaTrue });
0947:
0948: assertEquals("Failed applying {a[i] := t} {o:=a[i]} <> true",
0949: expected, simplified);
0950:
0951: // {a[i] := t} {o := a[j]} <> true
0952: constr = createUpdateTerm(new Term[] { ai, t,
0953: createUpdateTerm(new Term[] { o, aj, diaTrue }) });
0954: simplified = simply.simplify(constr, services);
0955: expected = createUpdateTerm(new Term[] { ai, t, o,
0956: tb.ife(tb.equals(jdx, idx), t, aj), diaTrue });
0957: assertEquals("Failed applying {a[i] := t} {o:=a[j]} <> true",
0958: expected, simplified);
0959:
0960: // {o.a := t} {o.a := o} <> true
0961: constr = createUpdateTerm(new Term[] { oa, t,
0962: createUpdateTerm(new Term[] { oa, o, diaTrue }) });
0963: simplified = simply.simplify(constr, services);
0964: expected = createUpdateTerm(new Term[] { oa, o, diaTrue });
0965: assertEquals("Failed applying {o.a := t} {o.a := o}<> true",
0966: expected, simplified);
0967:
0968: // {o.a := t} {o.a.a := o} <> true
0969: Term oaa = tb.dot(oa, pv[5]);
0970: Term ta = tb.dot(t, pv[5]);
0971: constr = createUpdateTerm(new Term[] { oa, t,
0972: createUpdateTerm(new Term[] { oaa, o, diaTrue }) });
0973: simplified = simply.simplify(constr, services);
0974: /*
0975: * expected = createUpdateTerm (new Term[]{oa,
0976: * tf.createIfElseTerm(o,t,oa, t), ta, o, diaTrue});
0977: */// skipped this improvement
0978: expected = createUpdateTerm(new Term[] { oa, t, ta, o, diaTrue });
0979: assertEquals("Failed applying {o.a := t} {o.a.a := o}<> true ",
0980: expected, simplified);
0981:
0982: // {o.a := t} {o.a.a := o.a} <> true
0983: constr = createUpdateTerm(new Term[] { oa, t,
0984: createUpdateTerm(new Term[] { oaa, oa, diaTrue }) });
0985: simplified = simply.simplify(constr, services);
0986: /*
0987: * expected = createUpdateTerm (new Term[]{oa,
0988: * tf.createIfElseTerm(o,t,oa, t), ta, t, diaTrue});
0989: */// this "optimization" is no longer performed
0990: expected = createUpdateTerm(new Term[] { oa, t, ta, t, diaTrue });
0991: assertEquals(
0992: "Failed applying {o.a := t} {o.a.a := o.a} <> true",
0993: expected, simplified);
0994: // {o.a := t} {u.a := u.a} <> true
0995: constr = createUpdateTerm(new Term[] { oa, t,
0996: createUpdateTerm(new Term[] { ua, ua, diaTrue }) });
0997: simplified = simply.simplify(constr, services);
0998: /*
0999: * expected = createUpdateTerm (new Term[] { oa, tf.createIfElseTerm
1000: * (o,u,oa,t), ua, tf.createIfElseTerm (u,o,t,ua), diaTrue });
1001: */
1002: expected = createUpdateTerm(new Term[] { oa, t, diaTrue });
1003: assertEquals("Failed applying {o.a := t} {u.a := u.a} <> true"
1004: + "(o, u compatible)", expected, simplified);
1005:
1006: // {o.a := t} {r.a := r.a} <> true
1007: constr = createUpdateTerm(new Term[] { oa, t,
1008: createUpdateTerm(new Term[] { ra, ra, diaTrue }) });
1009: simplified = simply.simplify(constr, services);
1010: expected = createUpdateTerm(new Term[] { oa, t, diaTrue });
1011: assertEquals("Failed applying {o.a := t} {r.a := r.a} <> true"
1012: + "(o, r bot compatible)", expected, simplified);
1013:
1014: // {o.a := t} {r.a.a := o} <> true
1015: Term raa = tb.dot(ra, pv[5]);
1016: constr = createUpdateTerm(new Term[] { oa, t,
1017: createUpdateTerm(new Term[] { raa, o, diaTrue }) });
1018: simplified = simply.simplify(constr, services);
1019: /*
1020: * expected = createUpdateTerm (new Term[] { oa, tf.createIfElseTerm(o,
1021: * ra, oa, t), raa, o, diaTrue });
1022: */// this "optimisation" is no longer performed
1023: expected = createUpdateTerm(new Term[] { oa, t, raa, o, diaTrue });
1024: assertEquals("Failed applying {o.a := t} {r.a.a := o} <> true"
1025: + "(o, r not compatible)", expected, simplified);
1026:
1027: }
1028:
1029: /**
1030: * tests the application of
1031: * <ul>
1032: * <li> {o.spv:=u, t.spv:=i} u.spv </li>
1033: * </ul>
1034: */
1035: public void testStaticAttributes() {
1036: UpdateSimplifier simply = new UpdateSimplifier();
1037: // {o.spv:=u, t.spv:=i} u.spv ~~~> i
1038: Term tspv = tb.dot(t, spv);
1039: Term constr = createUpdateTerm(new Term[] { ospv, u, tspv, i,
1040: uspv });
1041: Term simplified = simply.simplify(constr, TacletForTests
1042: .services());
1043: Term expected = i;
1044: assertSame("Failed applying {o.spv:=pv6, t.spv:=i} u.spv",
1045: expected, simplified);
1046: }
1047:
1048: /**
1049: * tests the application of
1050: * <ul>
1051: * <li> {a[i] := t, a[j] :=u} a[i] </li>
1052: * <li> {a[j] := t, a[i] :=u} a[i] </li>
1053: * <li> {a[j] := t, a[i] := o, a[m] := u} a[i] </li>
1054: * <li> {a[i] := u, a[m] := u} a[i] </li>
1055: * </ul>
1056: */
1057: public void testSimultaneousArrayApplications() {
1058: UpdateSimplifier simply = new UpdateSimplifier();
1059: Services services = TacletForTests.services();
1060:
1061: // {a[i] := t, a[j] :=u} a[i]
1062: Term constr = createUpdateTerm(new Term[] { ai, t, aj, u, ai });
1063: Term simplified = simply.simplify(constr, services);
1064: Term expected = tb.ife(tb.equals(idx, jdx), u, t);
1065: assertEquals("Failed applying {a[i] := t, a[j] :=u} a[i]",
1066: expected, simplified);
1067:
1068: // {a[j] := t, a[i] := u} a[i]
1069: constr = createUpdateTerm(new Term[] { aj, t, ai, u, ai });
1070: simplified = simply.simplify(constr, services);
1071: expected = u;
1072: assertEquals("Failed applying {a[j] := t, a[i] := u} a[i]",
1073: expected, simplified);
1074:
1075: // {a[j] := t, a[m] := u} a[i]
1076: constr = createUpdateTerm(new Term[] { aj, t, am, u, ai });
1077: simplified = simply.simplify(constr, services);
1078: expected = tb.ife(tb.equals(idx, mdx), u, tb.ife(tb.equals(idx,
1079: jdx), t, ai));
1080: assertEquals("Failed applying {a[j] := t, a[m] := u} a[i]",
1081: expected, simplified);
1082:
1083: // {a[I] := u, a[m] := u} a[i]
1084: // important to check simplification of conj cond
1085: constr = createUpdateTerm(new Term[] { ai, u, am, u, ai });
1086: simplified = simply.simplify(constr, services);
1087: expected = u;
1088: assertEquals("Failed applying {a[i] := u, a[m] := u} a[i]",
1089: expected, simplified);
1090:
1091: }
1092:
1093: /**
1094: * tests the application of updates on more complex terms. In particular it
1095: * is tested if conditional terms are simplified as far as possible.
1096: * <ul>
1097: * <li> {a[i] := u, c[j] :=u} (a * j : a[i] ?= b * m : c[j]) </li>
1098: * <li> {a[i] := u, c[j] :=u} (a * j : a[i] ?= b * m : c[j]) </li>
1099: * <li> {i := j} (a * j : a[i] ?= a * i : c[j]) </li>
1100: * <li> {o.a := u, r.a :=u} (o ?= u) o.a : r.a </li>
1101: * <li> {o := u} (o ?= u) u.a : o.a </li>
1102: * </ul>
1103: */
1104: // public void testSimultaneousUpdateApplicationOnComposedTerms() {
1105: // UpdateSimplifier simply=new UpdateSimplifier();
1106: //
1107: //
1108: // Term constr = createUpdateTerm(new Term[]
1109: // {ai, u, cj, u, tf.createConjCondTerm
1110: // (new Term[]{a, jdx, ai, b, mdx, cj})});
1111: // Term simplified = simply.simplify(constr);
1112: // Term expected = u;
1113: // assertEquals("Failed applying {a[i] := u, c[j] :=u}" +
1114: // "(a * j : a[i] ?= b * m : c[j]) ",
1115: // expected, simplified);
1116: //
1117: // // {a[i] := u, c[j] :=t} (a * j : a[i] ?= b * m : c[j])
1118: // constr = createUpdateTerm(new Term[]
1119: // {ai, u, cj, t, tf.createConjCondTerm
1120: // (new Term[]{a, jdx, ai, b, mdx, cj})});
1121: // simplified = simply.simplify(constr);
1122: // expected = tf.createConjCondTerm
1123: // (new Term[]{a, jdx, u, b, mdx, t});
1124: // assertEquals("Failed applying {a[i] := u, c[j] :=t}" +
1125: // "(a * j : a[i] ?= b * m : c[j]) ",
1126: // expected, simplified);
1127: //
1128: // // {i := j} (a * j : a[i] ?= a * i : c[j])
1129: // constr = createUpdateTerm(new Term[]
1130: // {idx, jdx, tf.createConjCondTerm
1131: // (new Term[]{a, jdx, ai, a, jdx, cj})});
1132: // simplified = simply.simplify(constr);
1133: // expected = cj;
1134: // assertSame("Failed applying {i := j} (a * j : a[i] ?= a * i : c[j]) ",
1135: // expected, simplified);
1136: //
1137: // // {o.a := u, r.a :=u} (o ?= u) o.a : r.a
1138: // constr = createUpdateTerm(new Term[]
1139: // {oa, u, ra, u, tf.createIfElseTerm
1140: // (o, u, oa, ra)});
1141: // simplified = simply.simplify(constr);
1142: // expected = u;
1143: // assertSame("Failed applying {o.a := u, r.a :=u} (o ?= u) o.a : r.a ",
1144: // expected, simplified);
1145: // // {o := u} (o ?= u) u.a : o.a
1146: // constr = createUpdateTerm(new Term[]
1147: // {o, u, tf.createIfElseTerm
1148: // (o, u, ua, oa)});
1149: // simplified = simply.simplify(constr);
1150: // expected = ua;
1151: // assertSame("Failed applying {o := u} (o ?= u) u.a : o.a ",
1152: // expected, simplified);
1153: //
1154: // // {o := t} (o ?= u) u.a : o.a
1155: // Term ta = tf.dot(pv[5], t);
1156: // constr = createUpdateTerm(new Term[]
1157: // {o, t, tf.createIfElseTerm
1158: // (o, u, ua, oa)});
1159: // simplified = simply.simplify(constr);
1160: // expected = tf.createIfElseTerm(t, u, ua, ta);
1161: // assertEquals("Failed applying {o := t} (o ?= u) u.a : o.a ",
1162: // expected, simplified);
1163: //
1164: //
1165: // // {r := t} (o ?= u) u.a : o.a
1166: // constr = createUpdateTerm(new Term[]
1167: // {r, t, tf.createIfElseTerm(o, u, ua, oa)});
1168: // simplified = simply.simplify(constr);
1169: // expected = constr.sub(1);
1170: // assertSame("Failed applying {r := t} (o ?= u) u.a : o.a " +
1171: // "(r incompatible to o,u", expected, simplified);
1172: //
1173: // }
1174: // new testing style here
1175: private final HelperClassForTests helper = new HelperClassForTests();
1176:
1177: public static final String testRules = System
1178: .getProperty("key.home")
1179: + File.separator
1180: + "examples"
1181: + File.separator
1182: + "_testcase" + File.separator + "updatesimplification";
1183:
1184: public void testAttributeEvaluateSubsFirst() {
1185: ProofAggregate proofList = helper.parse(new File(testRules
1186: + File.separator + "testAttributeRule1.key"));
1187: Term t1 = helper.extractProblemTerm(proofList.getFirstProof());
1188: UpdateSimplifier us = new UpdateSimplifier();
1189: assertEquals(
1190: "Evaluate attribute references under the update first",
1191: t1.sub(1), us.simplify(t1.sub(0), proofList
1192: .getFirstProof().getServices()));
1193: }
1194:
1195: public void testAttributeRule3() {
1196: ProofAggregate proofList = helper.parse(new File(testRules
1197: + File.separator + "testAttributeRule3.key"));
1198: Term t1 = helper.extractProblemTerm(proofList.getFirstProof());
1199: UpdateSimplifier us = new UpdateSimplifier();
1200: assertEquals(t1.sub(1), us.simplify(t1.sub(0), proofList
1201: .getFirstProof().getServices()));
1202: }
1203:
1204: public void testAttributeRule4() {
1205: ProofAggregate proofList = helper.parse(new File(testRules
1206: + File.separator + "testAttributeRule4.key"));
1207: Term t1 = helper.extractProblemTerm(proofList.getFirstProof());
1208: UpdateSimplifier us = new UpdateSimplifier();
1209: assertEquals(t1.sub(1), us.simplify(t1.sub(0), proofList
1210: .getFirstProof().getServices()));
1211: }
1212:
1213: public void testShadowedArraySimplificationRule() {
1214: ProofAggregate proofList = helper.parse(new File(testRules
1215: + File.separator + "testShadowedArrayRule1.key"));
1216: Term t1 = helper.extractProblemTerm(proofList.getFirstProof());
1217: UpdateSimplifier us = new UpdateSimplifier();
1218: assertEquals("Shadowed array are not aliased to "
1219: + "their unshadowed version", t1.sub(1), us.simplify(t1
1220: .sub(0), proofList.getFirstProof().getServices()));
1221: }
1222:
1223: public void testApplyArrayAccessOnShadowedArray() {
1224: ProofAggregate proofList = helper.parse(new File(testRules
1225: + File.separator + "testShadowedArrayRule2.key"));
1226: Term t1 = helper.extractProblemTerm(proofList.getFirstProof());
1227: UpdateSimplifier us = new UpdateSimplifier(true, false);
1228: assertEquals(
1229: "An array is aliased to " + "its shadowed version", t1
1230: .sub(1), us.simplify(t1.sub(0), proofList
1231: .getFirstProof().getServices()));
1232: }
1233:
1234: public void testApplyShadowedAttributeOnAttribute() {
1235: ProofAggregate proofList = helper.parse(new File(testRules
1236: + File.separator + "testShadowedAttributeRule1.key"));
1237: Term t1 = helper.extractProblemTerm(proofList.getFirstProof());
1238: UpdateSimplifier us = new UpdateSimplifier();
1239: assertEquals("Shadowed attributes are not aliased to "
1240: + "their unshadowed version", t1.sub(1), us.simplify(t1
1241: .sub(0), proofList.getFirstProof().getServices()));
1242: }
1243:
1244: public void testApplyAttributeOnShadowedAttribute() {
1245: ProofAggregate proofList = helper.parse(new File(testRules
1246: + File.separator + "testShadowedAttributeRule2.key"));
1247: Term t1 = helper.extractProblemTerm(proofList.getFirstProof());
1248: UpdateSimplifier us = new UpdateSimplifier(true, false);
1249: assertEquals("An attribute is aliased to "
1250: + "its shadowed version", t1.sub(1), us.simplify(t1
1251: .sub(0), proofList.getFirstProof().getServices()));
1252: }
1253:
1254: public void testShadowOnShadowSameTransactionNr() {
1255: ProofAggregate proofList = helper.parse(new File(testRules
1256: + File.separator + "testShadowOnShadowSameNr.key"));
1257: Term t1 = helper.extractProblemTerm(proofList.getFirstProof());
1258: UpdateSimplifier us = new UpdateSimplifier(true, false);
1259: assertEquals("Same number means shadows are aliased.", t1
1260: .sub(1), us.simplify(t1.sub(0), proofList
1261: .getFirstProof().getServices()));
1262: }
1263:
1264: public void testDeletion() {
1265: ProofAggregate proofList = helper.parse(new File(testRules
1266: + File.separator + "testDeletion.key"));
1267: Term t1 = helper.extractProblemTerm(proofList.getFirstProof());
1268: UpdateSimplifier us = new UpdateSimplifier(true, false);
1269: assertEquals("Deletion is broken.", t1.sub(1), us.simplify(t1
1270: .sub(0), proofList.getFirstProof().getServices()));
1271: }
1272:
1273: public void testNoDeletionIfAppliedOnNonRigidFunction() {
1274: ProofAggregate proofList = helper.parse(new File(testRules
1275: + File.separator + "testDeletion2.key"));
1276: Term t1 = helper.extractProblemTerm(proofList.getFirstProof());
1277: UpdateSimplifier us = new UpdateSimplifier(true, false);
1278: assertEquals("Deletion is broken.", t1.sub(1), us.simplify(t1
1279: .sub(0), proofList.getFirstProof().getServices()));
1280: }
1281:
1282: public void testDeletion3() {
1283: ProofAggregate proofList = helper.parse(new File(testRules
1284: + File.separator + "testDeletion3.key"));
1285: Term t1 = helper.extractProblemTerm(proofList.getFirstProof());
1286: UpdateSimplifier us = new UpdateSimplifier(true, false);
1287: assertEqualsModRenaming(t1.sub(1), us.simplify(t1.sub(0),
1288: proofList.getFirstProof().getServices()));
1289: assertEquals(Update.createUpdate(t1.sub(1))
1290: .getAllAssignmentPairs().size(), 2);
1291: }
1292:
1293: public void testDeletion4() {
1294: ProofAggregate proofList = helper.parse(new File(testRules
1295: + File.separator + "testDeletion4.key"));
1296: Term t1 = helper.extractProblemTerm(proofList.getFirstProof());
1297: UpdateSimplifier us = new UpdateSimplifier(true, false);
1298: assertEqualsModRenaming(t1.sub(1), us.simplify(t1.sub(0),
1299: proofList.getFirstProof().getServices()));
1300: assertEquals(Update.createUpdate(t1.sub(1))
1301: .getAllAssignmentPairs().size(), 1);
1302: }
1303:
1304: public void testDeletion5() {
1305: ProofAggregate proofList = helper.parse(new File(testRules
1306: + File.separator + "testDeletion5.key"));
1307: Term t1 = helper.extractProblemTerm(proofList.getFirstProof());
1308: UpdateSimplifier us = new UpdateSimplifier(true, false);
1309: assertEqualsModRenaming(t1.sub(1), us.simplify(t1.sub(0),
1310: proofList.getFirstProof().getServices()));
1311: assertEquals(Update.createUpdate(t1.sub(1))
1312: .getAllAssignmentPairs().size(), 1);
1313: }
1314:
1315: public void testDeletion6() {
1316: ProofAggregate proofList = helper.parse(new File(testRules
1317: + File.separator + "testDeletion6.key"));
1318: Term t1 = helper.extractProblemTerm(proofList.getFirstProof());
1319: UpdateSimplifier us = new UpdateSimplifier(true, false);
1320: assertEqualsModRenaming(t1.sub(1), us.simplify(t1.sub(0),
1321: proofList.getFirstProof().getServices()));
1322: assertEquals(Update.createUpdate(t1.sub(1))
1323: .getAllAssignmentPairs().size(), 1);
1324: }
1325:
1326: public void testDeletion7() {
1327: ProofAggregate proofList = helper.parse(new File(testRules
1328: + File.separator + "testDeletion7.key"));
1329: Term t1 = helper.extractProblemTerm(proofList.getFirstProof());
1330: UpdateSimplifier us = new UpdateSimplifier(true, false);
1331: assertEqualsModRenaming(t1, us.simplify(t1, proofList
1332: .getFirstProof().getServices()));
1333: assertEquals(Update.createUpdate(t1).getAllAssignmentPairs()
1334: .size(), 2);
1335: }
1336:
1337: public void testDeletion8() {
1338: ProofAggregate proofList = helper.parse(new File(testRules
1339: + File.separator + "testDeletion8.key"));
1340: Term t1 = helper.extractProblemTerm(proofList.getFirstProof());
1341: UpdateSimplifier us = new UpdateSimplifier(true, false);
1342: assertEqualsModRenaming(t1, us.simplify(t1, proofList
1343: .getFirstProof().getServices()));
1344: assertEquals(Update.createUpdate(t1).getAllAssignmentPairs()
1345: .size(), 2);
1346: }
1347:
1348: public void testDeletion9() {
1349: ProofAggregate proofList = helper.parse(new File(testRules
1350: + File.separator + "testDeletion9.key"));
1351: Term t1 = helper.extractProblemTerm(proofList.getFirstProof());
1352: UpdateSimplifier us = new UpdateSimplifier(true, false);
1353: assertEqualsModRenaming(t1.sub(1), us.simplify(t1.sub(0),
1354: proofList.getFirstProof().getServices()));
1355: assertEquals(Update.createUpdate(t1.sub(1))
1356: .getAllAssignmentPairs().size(), 2);
1357: }
1358:
1359: public void testDeletion10() {
1360: ProofAggregate proofList = helper.parse(new File(testRules
1361: + File.separator + "testDeletion10.key"));
1362: Term t1 = helper.extractProblemTerm(proofList.getFirstProof());
1363: UpdateSimplifier us = new UpdateSimplifier(true, false);
1364: assertEqualsModRenaming(t1.sub(1), us.simplify(t1.sub(0),
1365: proofList.getFirstProof().getServices()));
1366: assertEquals(Update.createUpdate(t1.sub(1))
1367: .getAllAssignmentPairs().size(), 2);
1368: }
1369:
1370: public void testDeletion11() {
1371: ProofAggregate proofList = helper.parse(new File(testRules
1372: + File.separator + "testDeletion11.key"));
1373: Term t1 = helper.extractProblemTerm(proofList.getFirstProof());
1374: UpdateSimplifier us = new UpdateSimplifier(true, false);
1375: assertEqualsModRenaming(t1, us.simplify(t1, proofList
1376: .getFirstProof().getServices()));
1377: assertEquals(Update.createUpdate(t1).getAllAssignmentPairs()
1378: .size(), 3);
1379: }
1380:
1381: public void testDeletion12() {
1382: final Services services = TacletForTests.services();
1383:
1384: final UpdateFactory uf = new UpdateFactory(services,
1385: new UpdateSimplifier(true, false));
1386:
1387: final Term zeroAccess = tb.array(tb.var(arrayVar1), tb.zTerm(
1388: services, "0"));
1389: final Term intVarAccess = tb.array(tb.var(arrayVar1), tb
1390: .var(intVar));
1391:
1392: final Update parUpd = uf.parallel(uf.quantify(arrayVar1, uf
1393: .elementaryUpdate(zeroAccess, o)), uf.quantify(intVar,
1394: uf.elementaryUpdate(intVarAccess, u)));
1395:
1396: assertEquals(parUpd.getAllAssignmentPairs().size(), 2);
1397: assertSame(parUpd.getAssignmentPair(0).boundVars()
1398: .lastQuantifiableVariable(), arrayVar1);
1399: assertSame(parUpd.getAssignmentPair(1).boundVars()
1400: .lastQuantifiableVariable(), intVar);
1401:
1402: final Term updateTerm = uf.apply(parUpd, tb
1403: .dia(JavaBlock.createJavaBlock(new StatementBlock()),
1404: tb.equals(o, o)));
1405:
1406: assertEquals(Update.createUpdate(updateTerm)
1407: .getAllAssignmentPairs().size(), 2);
1408: }
1409:
1410: public void testAnonymous1() {
1411: ProofAggregate proofList = helper.parse(new File(testRules
1412: + File.separator + "testAnonymous1.key"));
1413: Term t1 = helper.extractProblemTerm(proofList.getFirstProof());
1414: UpdateSimplifier us = new UpdateSimplifier(true, false);
1415: assertEquals("Anonymous updates are broken.", t1.sub(1), us
1416: .simplify(t1.sub(0), proofList.getFirstProof()
1417: .getServices()));
1418: }
1419:
1420: public void testAnonymous2() {
1421: ProofAggregate proofList = helper.parse(new File(testRules
1422: + File.separator + "testAnonymous2.key"));
1423: Term t1 = helper.extractProblemTerm(proofList.getFirstProof());
1424: UpdateSimplifier us = new UpdateSimplifier(true, false);
1425: assertEquals("Anonymous updates are broken.", t1.sub(1), us
1426: .simplify(t1.sub(0), proofList.getFirstProof()
1427: .getServices()));
1428: }
1429:
1430: public void testHeapDependentFunctions1() {
1431: ProofAggregate proofList = helper.parse(new File(testRules
1432: + File.separator + "testHeapDependent1.key"));
1433: Term t1 = helper.extractProblemTerm(proofList.getFirstProof());
1434: UpdateSimplifier us = new UpdateSimplifier(true, false);
1435: assertEquals("Update simplification rule for heap dependent "
1436: + "function symbols broken.", t1.sub(1), us.simplify(t1
1437: .sub(0), proofList.getFirstProof().getServices()));
1438: }
1439:
1440: public void testHeapDependentFunctions2() {
1441: ProofAggregate proofList = helper.parse(new File(testRules
1442: + File.separator + "testHeapDependent1.key"));
1443: Term t1 = helper.extractProblemTerm(proofList.getFirstProof());
1444: UpdateSimplifier us = new UpdateSimplifier(true, false);
1445: assertEquals("Update simplification rule for heap dependent "
1446: + "function symbols broken.", t1.sub(1), us.simplify(t1
1447: .sub(0), proofList.getFirstProof().getServices()));
1448: }
1449:
1450: public void testQuantified1() {
1451: ProofAggregate proofList = helper.parse(new File(testRules
1452: + File.separator + "testQuantified1.key"));
1453: Term t1 = helper.extractProblemTerm(proofList.getFirstProof());
1454: UpdateSimplifier us = new UpdateSimplifier(true, false);
1455: assertEqualsModRenaming(us.simplify(t1.sub(0), proofList
1456: .getFirstProof().getServices()), t1.sub(1));
1457: }
1458:
1459: public void testQuantified2() {
1460: ProofAggregate proofList = helper.parse(new File(testRules
1461: + File.separator + "testQuantified2.key"));
1462: Term t1 = helper.extractProblemTerm(proofList.getFirstProof());
1463: UpdateSimplifier us = new UpdateSimplifier(true, false);
1464: assertEqualsModRenaming(us.simplify(t1.sub(0), proofList
1465: .getFirstProof().getServices()), t1.sub(1));
1466: }
1467:
1468: public void testQuantified3() {
1469: ProofAggregate proofList = helper.parse(new File(testRules
1470: + File.separator + "testQuantified3.key"));
1471: Term t1 = helper.extractProblemTerm(proofList.getFirstProof());
1472: UpdateSimplifier us = new UpdateSimplifier(true, false);
1473: assertEqualsModRenaming(us.simplify(t1.sub(0), proofList
1474: .getFirstProof().getServices()), t1.sub(1));
1475: }
1476:
1477: public void testQuantified4() {
1478: ProofAggregate proofList = helper.parse(new File(testRules
1479: + File.separator + "testQuantified4.key"));
1480: Term t1 = helper.extractProblemTerm(proofList.getFirstProof());
1481: UpdateSimplifier us = new UpdateSimplifier(true, false);
1482: assertEqualsModRenaming(us.simplify(t1.sub(0), proofList
1483: .getFirstProof().getServices()), t1.sub(1));
1484: }
1485:
1486: public void testQuantified5() {
1487: ProofAggregate proofList = helper.parse(new File(testRules
1488: + File.separator + "testQuantified5.key"));
1489: Term t1 = helper.extractProblemTerm(proofList.getFirstProof());
1490: UpdateSimplifier us = new UpdateSimplifier(true, false);
1491: assertEqualsModRenaming(us.simplify(t1.sub(0), proofList
1492: .getFirstProof().getServices()), t1.sub(1));
1493: }
1494:
1495: public static void main(String[] args) {
1496: TestUpdateSimplifier tsus = new TestUpdateSimplifier("t");
1497: tsus.setUp();
1498: tsus.testDeletion();
1499: // tsus.testBasicRules();
1500: // tsus.testDeletionStrategy();
1501: // tsus.testSimultaneousUpdateEquality();
1502: // tsus.testApplyOnAttribute();
1503: }
1504: }
|