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.proof.incclosure;
012:
013: import junit.framework.TestCase;
014: import de.uka.ilkd.key.java.Services;
015: import de.uka.ilkd.key.logic.*;
016: import de.uka.ilkd.key.logic.op.Function;
017: import de.uka.ilkd.key.logic.op.Metavariable;
018: import de.uka.ilkd.key.logic.op.RigidFunction;
019: import de.uka.ilkd.key.logic.op.TermSymbol;
020: import de.uka.ilkd.key.logic.sort.PrimitiveSort;
021: import de.uka.ilkd.key.logic.sort.Sort;
022:
023: public class TestMerger extends TestCase {
024:
025: // Taken from TestConstraint.java
026:
027: private final static TermFactory tf = TermFactory.DEFAULT;
028: private Services services;
029: private Sort sort1;
030: private Function f;
031: private Constraint constraint_b;
032: private Constraint constraint_a;
033: private Function con;
034: private Metavariable x;
035: private Metavariable z;
036: private Metavariable y;
037:
038: private Term term_f(TermSymbol var) {
039: Term t_x = tf.createFunctionTerm(var, new Term[] {});
040: return term_f(t_x);
041: }
042:
043: private Term term_f(Term t) {
044: Term t_fx = tf.createFunctionTerm(f, t);
045: return t_fx;
046: }
047:
048: public TestMerger(String name) {
049: super (name);
050: }
051:
052: public void setUp() {
053: sort1 = new PrimitiveSort(new Name("S1"));
054: f = new RigidFunction(new Name("f"), sort1,
055: new Sort[] { sort1 });
056: // f(:S1):S1
057: con = new RigidFunction(new Name("c"), sort1,
058: new PrimitiveSort[0]);
059: x = new Metavariable(new Name("x"), sort1); //x:S1
060: z = new Metavariable(new Name("z"), sort1); //z:S1
061: y = new Metavariable(new Name("y"), sort1); //y:S1
062:
063: constraint_a = Constraint.BOTTOM.unify(term_f(x), term_f(con),
064: null).unify(term_f(y), term_f(x), null);
065:
066: constraint_b = Constraint.BOTTOM.unify(term_f(x), term_f(con),
067: null).unify(term_f(z), term_f(term_f(con)), null);
068:
069: if (constraint_a == Constraint.TOP
070: || constraint_b == Constraint.TOP)
071: throw new RuntimeException(
072: "Error setting up tests for Merger.");
073:
074: services = new Services();
075:
076: services.getNamespaces().sorts().add(sort1);
077: }
078:
079: public void tearDown() {
080: services = null;
081: sort1 = null;
082: f = null;
083: constraint_a = null;
084: constraint_b = null;
085: con = null;
086: x = y = z = null;
087: }
088:
089: public void doBufferSinkTests(BufferSink s) {
090: assertTrue(!s.isSatisfiable()
091: && s.getConstraint() == Constraint.TOP);
092:
093: s.put(constraint_a);
094: assertTrue(s.isSatisfiable()
095: && s.getConstraint().equals(constraint_a));
096:
097: s.put(constraint_a);
098: assertTrue(s.isSatisfiable()
099: && s.getConstraint().equals(constraint_a));
100:
101: s.reset(constraint_a);
102: assertTrue(s.isSatisfiable()
103: && s.getConstraint().equals(constraint_a));
104:
105: s.put(Constraint.TOP);
106: assertTrue(s.isSatisfiable()
107: && s.getConstraint().equals(constraint_a));
108:
109: s.put(Constraint.BOTTOM);
110: assertTrue(s.isSatisfiable()
111: && s.getConstraint() == Constraint.BOTTOM);
112:
113: s.reset(Constraint.TOP);
114: assertTrue(!s.isSatisfiable()
115: && s.getConstraint() == Constraint.TOP);
116:
117: s.put(constraint_a);
118: s.put(constraint_b);
119: assertTrue(s.isSatisfiable()
120: && s.getConstraint().isAsWeakAs(constraint_a)
121: && s.getConstraint().isAsWeakAs(constraint_b));
122:
123: s.put(Constraint.BOTTOM);
124: assertTrue(s.isSatisfiable()
125: && s.getConstraint() == Constraint.BOTTOM);
126: }
127:
128: public void testBufferSink() {
129: {
130: BufferSink s = new BufferSink(null);
131: doBufferSinkTests(s);
132: }
133:
134: {
135: BufferSink r = new BufferSink(null);
136: BufferSink s = new BufferSink(r);
137: doBufferSinkTests(s);
138: }
139: }
140:
141: public void testMultiMerger() {
142: BufferSink root = new BufferSink(null);
143: MultiMerger merger = new MultiMerger(root, 3, services);
144:
145: BufferSink[] sinks = new BufferSink[5];
146: IteratorOfSink it = merger.getSinks();
147: sinks[0] = new BufferSink(it.next());
148: sinks[1] = new BufferSink(it.next());
149: sinks[2] = new BufferSink(it.next());
150:
151: doBufferSinkTests(sinks[0]);
152: sinks[0].reset(Constraint.TOP);
153:
154: doBufferSinkTests(sinks[1]);
155: sinks[1].reset(Constraint.TOP);
156:
157: sinks[0].put(constraint_b);
158: sinks[1].put(constraint_b);
159: sinks[2].put(constraint_a);
160: assertTrue(root.getConstraint().isSatisfiable()
161: && root.getConstraint().equals(
162: constraint_a.join(constraint_b, services)));
163:
164: sinks[0].put(constraint_a);
165: assertTrue(root.getConstraint().isSatisfiable()
166: && root.getConstraint().equals(
167: constraint_a.join(constraint_b, services)));
168:
169: sinks[1].put(constraint_a);
170: assertTrue(root.getConstraint().isSatisfiable()
171: && root.getConstraint().equals(constraint_a));
172:
173: sinks[2].put(constraint_b);
174: assertTrue(root.getConstraint().isSatisfiable()
175: && root.getConstraint().equals(
176: IntersectionConstraint.intersect(constraint_a,
177: constraint_b)));
178:
179: sinks[2].put(Constraint.BOTTOM);
180: assertTrue(root.getConstraint().isSatisfiable()
181: && root.getConstraint().equals(
182: IntersectionConstraint.intersect(constraint_a,
183: constraint_b)));
184:
185: sinks[0].reset(Constraint.TOP);
186: assertTrue(!root.getConstraint().isSatisfiable()
187: && root.getConstraint() == Constraint.TOP);
188:
189: merger.expand(5);
190: it = merger.getSinks();
191: it.next();
192: it.next();
193: it.next();
194: sinks[3] = new BufferSink(it.next());
195: sinks[4] = new BufferSink(it.next());
196:
197: sinks[0].put(constraint_b);
198: sinks[1].put(constraint_b);
199: sinks[2].put(constraint_a);
200: sinks[3].put(constraint_b);
201: sinks[4].put(constraint_a);
202: assertTrue(root.getConstraint().isSatisfiable()
203: && root.getConstraint().equals(
204: constraint_a.join(constraint_b, services)));
205:
206: sinks[3].put(Constraint.BOTTOM);
207: assertTrue(root.getConstraint().isSatisfiable()
208: && root.getConstraint().equals(
209: constraint_a.join(constraint_b, services)));
210:
211: sinks[4].put(Constraint.TOP);
212: assertTrue(root.getConstraint().isSatisfiable()
213: && root.getConstraint().equals(
214: constraint_a.join(constraint_b, services)));
215:
216: sinks[4].reset(Constraint.TOP);
217: assertTrue(!root.getConstraint().isSatisfiable()
218: && root.getConstraint() == Constraint.TOP);
219:
220: assertTrue(
221: "No intersection sorts should have been introduced",
222: services.getNamespaces().sorts().allElements().size() == 1);
223: }
224:
225: }
|