001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.logic;
012:
013: import junit.framework.TestCase;
014: import de.uka.ilkd.key.logic.op.Function;
015: import de.uka.ilkd.key.logic.op.Metavariable;
016: import de.uka.ilkd.key.logic.op.RigidFunction;
017: import de.uka.ilkd.key.logic.sort.PrimitiveSort;
018: import de.uka.ilkd.key.logic.sort.Sort;
019:
020: public class TestSemisequent extends TestCase {
021:
022: private ConstrainedFormula[] con;
023:
024: public TestSemisequent(String name) {
025: super (name);
026: }
027:
028: public void setUp() {
029: TermFactory tf = TermFactory.DEFAULT;
030:
031: Function p = new RigidFunction(new Name("p"), Sort.FORMULA,
032: new Sort[] {});
033: Function q = new RigidFunction(new Name("q"), Sort.FORMULA,
034: new Sort[] {});
035: Function r = new RigidFunction(new Name("r"), Sort.FORMULA,
036: new Sort[] {});
037:
038: Function a = new RigidFunction(new Name("a"), Sort.FORMULA,
039: new Sort[] {});
040: Function b = new RigidFunction(new Name("b"), Sort.FORMULA,
041: new Sort[] {});
042: Function c = new RigidFunction(new Name("c"), Sort.FORMULA,
043: new Sort[] {});
044:
045: Term t_p = tf.createFunctionTerm(p, new Term[] {});
046: Term t_q = tf.createFunctionTerm(q, new Term[] {});
047: Term t_r = tf.createFunctionTerm(r, new Term[] {});
048:
049: Term t_a = tf.createFunctionTerm(a, new Term[] {});
050: Term t_b = tf.createFunctionTerm(b, new Term[] {});
051: Term t_c = tf.createFunctionTerm(c, new Term[] {});
052:
053: con = new ConstrainedFormula[8];
054: con[0] = new ConstrainedFormula(t_p, Constraint.BOTTOM);
055: con[1] = new ConstrainedFormula(t_q, Constraint.BOTTOM);
056: con[2] = new ConstrainedFormula(t_r, Constraint.BOTTOM);
057: con[3] = new ConstrainedFormula(t_r, Constraint.BOTTOM);
058: con[4] = new ConstrainedFormula(t_a, Constraint.BOTTOM);
059: con[5] = new ConstrainedFormula(t_b, Constraint.BOTTOM);
060: con[6] = new ConstrainedFormula(t_c, Constraint.BOTTOM);
061:
062: Sort s = new PrimitiveSort(new Name("test"));
063: Function f = new RigidFunction(new Name("f"), s, new Sort[] {});
064: Term t_f = tf.createFunctionTerm(f, new Term[] {});
065: Metavariable mv = new Metavariable(new Name("mv"), s);
066: Term t_mv = tf.createFunctionTerm(mv, new Term[] {});
067: Constraint cons = Constraint.BOTTOM.unify(t_mv, t_f, null);
068: assertTrue(cons.isSatisfiable());
069: con[7] = new ConstrainedFormula(t_c, cons);
070: }
071:
072: public void tearDown() {
073: con = null;
074: }
075:
076: private Semisequent extract(SemisequentChangeInfo semiCI) {
077: return semiCI.semisequent();
078: }
079:
080: public void testContains() {
081: Semisequent seq = Semisequent.EMPTY_SEMISEQUENT;
082: seq = extract(seq.insert(0, con[0]));
083: seq = extract(seq.insert(1, con[1]));
084: ConstrainedFormula eq2con0 = new ConstrainedFormula(con[0]
085: .formula(), Constraint.BOTTOM);
086: assertTrue(
087: "Contains should test of identity and not equality.",
088: !seq.contains(eq2con0));
089: }
090:
091: public void testContainsEquals() {
092: Semisequent seq = Semisequent.EMPTY_SEMISEQUENT;
093: seq = extract(seq.insert(0, con[0]));
094: seq = extract(seq.insert(1, con[1]));
095: ConstrainedFormula eq2con0 = new ConstrainedFormula(con[0]
096: .formula(), Constraint.BOTTOM);
097: assertTrue(
098: "Contains tests of equality and should find the formula.",
099: seq.containsEqual(eq2con0));
100: }
101:
102: public void testGet() {
103: Semisequent seq = Semisequent.EMPTY_SEMISEQUENT;
104: seq = extract(seq.insert(0, con[0]));
105: seq = extract(seq.insert(1, con[1]));
106: assertSame(seq.get(0), con[0]);
107: assertSame(seq.get(1), con[1]);
108:
109: try {
110: seq.get(2);
111: } catch (IndexOutOfBoundsException iob) {
112: return;
113: }
114: fail();
115: }
116:
117: public void testindexOf() {
118: Semisequent seq = Semisequent.EMPTY_SEMISEQUENT;
119: seq = extract(seq.insert(0, con[0]));
120: seq = extract(seq.insert(1, con[1]));
121: seq = extract(seq.insert(2, con[2]));
122: assertTrue("Semisequent has wrong size.", seq.size() == 3);
123: assertTrue("con[0] has wrong index in semisequent. Expected 0"
124: + " has " + seq.indexOf(con[0]),
125: seq.indexOf(con[0]) == 0);
126: assertTrue("con[1] has wrong index in semisequent. Expected 1"
127: + " has " + seq.indexOf(con[1]),
128: seq.indexOf(con[1]) == 1);
129: assertTrue("con[2] has wrong index in semisequent. Expected 2"
130: + " has " + seq.indexOf(con[2]),
131: seq.indexOf(con[2]) == 2);
132: }
133:
134: public void testRemove() {
135:
136: Semisequent seq = Semisequent.EMPTY_SEMISEQUENT;
137: seq = extract(seq.insert(0, con[0]));
138: seq = extract(seq.insert(1, con[1]));
139: seq = extract(seq.insert(2, con[2]));
140: seq = extract(seq.remove(1));
141:
142: assertTrue("Semisequent has wrong size.", seq.size() == 2);
143: assertTrue("Semisequent contains deleted element.", !seq
144: .contains(con[1]));
145: assertTrue("con[1] has wrong index in semisequent", seq
146: .indexOf(con[1]) == -1);
147: assertTrue("con[0] has wrong index in semisequent", seq
148: .indexOf(con[0]) == 0);
149: assertTrue("con[2] has wrong index in semisequent", seq
150: .indexOf(con[2]) == 1);
151: }
152:
153: public void testReplace() {
154: Semisequent seq = Semisequent.EMPTY_SEMISEQUENT;
155: seq = extract(seq.insert(0, con[0]));
156: seq = extract(seq.insert(1, con[1]));
157: seq = extract(seq.replace(1, con[2]));
158:
159: assertTrue("Semisequent has wrong size.", seq.size() == 2);
160: assertTrue("Semisequent contains deleted element.", !seq
161: .contains(con[1]));
162: assertTrue("con[1] has wrong index in semisequent", seq
163: .indexOf(con[1]) == -1);
164: assertTrue("con[0] has wrong index in semisequent", seq
165: .indexOf(con[0]) == 0);
166: assertTrue("con[2] has wrong index in semisequent", seq
167: .indexOf(con[2]) == 1);
168: }
169:
170: public void testNoDuplicates() {
171: Semisequent seq = Semisequent.EMPTY_SEMISEQUENT;
172: seq = extract(seq.insert(0, con[0]));
173: seq = extract(seq.insert(1, con[1]));
174: seq = extract(seq.insert(2, con[1]));
175:
176: assertTrue("Semisequent has duplicate", seq.size() == 2);
177: }
178:
179: public void testImmutable() {
180: Semisequent seq = Semisequent.EMPTY_SEMISEQUENT;
181: Semisequent old = Semisequent.EMPTY_SEMISEQUENT;
182: seq = extract(seq.insert(0, con[0]));
183: seq = extract(seq.insert(1, con[1]));
184: old = seq;
185: seq = extract(seq.insert(2, con[2]));
186:
187: assertTrue("Semisequent seems not to be immutable.",
188: old.size() == 2);
189: }
190:
191: public void testUniqueEmpty() {
192: Semisequent seq = Semisequent.EMPTY_SEMISEQUENT;
193: seq = extract(seq.insert(0, con[0]));
194: seq = extract(seq.remove(0));
195: assertSame(
196: "Semisequent is empty but not the EMPTY_SEMISEQUENT.",
197: seq, Semisequent.EMPTY_SEMISEQUENT);
198:
199: }
200:
201: public void testEquals() {
202: Semisequent seq1 = Semisequent.EMPTY_SEMISEQUENT;
203: seq1 = extract(seq1.insert(0, con[0]));
204: seq1 = extract(seq1.insert(0, con[1]));
205: seq1 = extract(seq1.insert(0, con[2]));
206: Semisequent seq2 = Semisequent.EMPTY_SEMISEQUENT;
207: seq2 = extract(seq2.insert(0, con[0]));
208: seq2 = extract(seq2.insert(0, con[1]));
209: seq2 = extract(seq2.insert(0, con[2]));
210: Semisequent seq3 = Semisequent.EMPTY_SEMISEQUENT;
211: seq3 = extract(seq3.insert(0, con[0]));
212: seq3 = extract(seq3.insert(0, con[1]));
213: seq3 = extract(seq3.insert(0, con[3]));
214: Semisequent seq4 = Semisequent.EMPTY_SEMISEQUENT;
215: seq4 = extract(seq4.insert(0, con[0]));
216: seq4 = extract(seq4.insert(0, con[2]));
217: seq4 = extract(seq4.insert(0, con[1]));
218:
219: assertEquals("seq1=seq1", seq1, seq1);
220: assertEquals("seq1=seq2", seq1, seq2);
221: assertEquals("seq1=seq3", seq1, seq3);
222: assertTrue("seq1!=seq4", !seq1.equals(seq4));
223: }
224:
225: public void testListInsert() {
226: Semisequent origin = extract(extract(
227: extract(
228: Semisequent.EMPTY_SEMISEQUENT
229: .insertLast(con[0])).insertLast(con[1]))
230: .insertLast(con[2]));
231:
232: Semisequent expected = extract(extract(
233: extract(origin.insertLast(con[4])).insertLast(con[5]))
234: .insertLast(con[6]));
235: ListOfConstrainedFormula insertionList = SLListOfConstrainedFormula.EMPTY_LIST
236: .prepend(con[0]).prepend(con[1]).prepend(con[6])
237: .prepend(con[5]).prepend(con[4]);
238: Semisequent result = extract(origin.insert(origin.size(),
239: insertionList));
240: assertEquals("Both semisequents should be equal.", expected,
241: result);
242:
243: }
244:
245: public void testListInsertInMid() {
246: Semisequent origin = extract(extract(
247: extract(
248: Semisequent.EMPTY_SEMISEQUENT
249: .insertLast(con[0])).insertLast(con[1]))
250: .insertLast(con[2]));
251: Semisequent expected = extract(extract(
252: extract(origin.insert(2, con[4])).insert(3, con[5]))
253: .insert(4, con[6]));
254: ListOfConstrainedFormula insertionList = SLListOfConstrainedFormula.EMPTY_LIST
255: .prepend(con[0]).prepend(con[1]).prepend(con[6])
256: .prepend(con[5]).prepend(con[4]);
257: Semisequent result = extract(origin.insert(origin.size() - 1,
258: insertionList));
259: assertEquals("Both semisequents should be equal.", expected,
260: result);
261:
262: }
263:
264: public void testListReplace() {
265: // [p,q,r]
266: Semisequent origin = extract(extract(
267: extract(
268: Semisequent.EMPTY_SEMISEQUENT
269: .insertLast(con[0])).insertLast(con[1]))
270: .insertLast(con[2]));
271: // [p,q,a,b,c]
272: Semisequent expected = extract(extract(
273: extract(extract(origin.remove(2)).insertLast(con[4]))
274: .insertLast(con[5])).insertLast(con[6]));
275: // insert: [a,b,c,q,p]
276: ListOfConstrainedFormula insertionList = SLListOfConstrainedFormula.EMPTY_LIST
277: .prepend(con[0]).prepend(con[1]).prepend(con[6])
278: .prepend(con[5]).prepend(con[4]);
279:
280: SemisequentChangeInfo result = origin.replace(
281: origin.size() - 1, insertionList);
282:
283: assertEquals(
284: "SemisequentChangeInfo is corrupt due to wrong added formula list:",
285: SLListOfConstrainedFormula.EMPTY_LIST.prepend(con[4])
286: .prepend(con[5]).prepend(con[6]), result
287: .addedFormulas());
288: assertEquals(
289: "SemisequentChangeInfo is corrupt due to wrong removed formula list:",
290: SLListOfConstrainedFormula.EMPTY_LIST.prepend(con[2]),
291: result.removedFormulas());
292: assertEquals("Both semisequents should be equal.", expected,
293: extract(result));
294:
295: }
296:
297: public void testRemoveRedundantFormulaOfSequent() {
298: //[p,q,c<<mv=f]
299: Semisequent origin = extract(extract(
300: extract(
301: Semisequent.EMPTY_SEMISEQUENT
302: .insertLast(con[0])).insertLast(con[1]))
303: .insertLast(con[7]));
304: //exp.:[p,q,a,c]
305: Semisequent expected = extract(extract(
306: extract(origin.remove(2)).insertLast(con[4]))
307: .insertLast(con[6]));
308: //insert: [a,c,q,p]
309: ListOfConstrainedFormula insertionList = SLListOfConstrainedFormula.EMPTY_LIST
310: .prepend(con[0]).prepend(con[1]).prepend(con[6])
311: .prepend(con[4]);
312:
313: SemisequentChangeInfo sci = origin.insert(origin.size(),
314: insertionList);
315: assertEquals(
316: "SemisequentChangeInfo is corrupt due to wrong added formula list:",
317: SLListOfConstrainedFormula.EMPTY_LIST.prepend(con[4])
318: .prepend(con[6]), sci.addedFormulas());
319: assertEquals(
320: "SemisequentChangeInfo is corrupt due to wrong removed formula list:",
321: SLListOfConstrainedFormula.EMPTY_LIST.prepend(con[7]),
322: sci.removedFormulas());
323: assertEquals("Both semisequents should be equal.", expected,
324: extract(sci));
325:
326: }
327:
328: public void testListReplaceAddRedundantList() {
329: //[p,q]
330: Semisequent origin = extract(extract(
331: Semisequent.EMPTY_SEMISEQUENT.insertLast(con[0]))
332: .insertLast(con[1]));
333: //[exp.: p,q,a,b,c,r]
334: Semisequent expected = extract(extract(
335: extract(
336: extract(origin.insertLast(con[4])).insertLast(
337: con[5])).insertLast(con[6]))
338: .insertLast(con[2]));
339: // insert:[a,b,c,r,r,q,p]
340: ListOfConstrainedFormula insertionList = SLListOfConstrainedFormula.EMPTY_LIST
341: .prepend(con[0]).prepend(con[1]).prepend(con[2])
342: .prepend(con[3]).prepend(con[6]).prepend(con[5])
343: .prepend(con[4]);
344:
345: SemisequentChangeInfo sci = origin.replace(origin.size(),
346: insertionList);
347: assertEquals(
348: "SemisequentChangeInfo is corrupt due to wrong added formula list:",
349: SLListOfConstrainedFormula.EMPTY_LIST.prepend(con[4])
350: .prepend(con[5]).prepend(con[6])
351: .prepend(con[3]), sci.addedFormulas());
352: assertEquals(
353: "SemisequentChangeInfo is corrupt due to wrong removed formula list:",
354: SLListOfConstrainedFormula.EMPTY_LIST, sci
355: .removedFormulas());
356: assertEquals("Both semisequents should be equal.", expected,
357: extract(sci));
358: }
359:
360: }
|