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.Assert;
014: import junit.framework.TestCase;
015: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
016: import de.uka.ilkd.key.logic.op.*;
017: import de.uka.ilkd.key.logic.sort.ClassInstanceSortImpl;
018: import de.uka.ilkd.key.logic.sort.PrimitiveSort;
019: import de.uka.ilkd.key.logic.sort.SetAsListOfSort;
020: import de.uka.ilkd.key.logic.sort.Sort;
021:
022: /** class tests the term factory
023: */
024: public class TestTermFactory extends TestCase {
025:
026: private static final TermFactory tf = TermFactory.DEFAULT;
027: private Term et1;
028: private Sort sort1 = new PrimitiveSort(new Name("S1"));
029: private Sort sort2 = new PrimitiveSort(new Name("S2"));
030: private Sort sort3 = new PrimitiveSort(new Name("S3"));
031: private Sort osort1 = new ClassInstanceSortImpl(new Name("os1"),
032: false);
033: private Sort osort2 = new ClassInstanceSortImpl(new Name("os2"),
034: osort1, false);
035: private Sort osort3 = new ClassInstanceSortImpl(new Name("os3"),
036: osort1, false);
037: private Sort osort4 = new ClassInstanceSortImpl(new Name("os4"),
038: SetAsListOfSort.EMPTY_SET.add(osort2).add(osort3), false);
039:
040: Function p = new RigidFunction(new Name("p"), Sort.FORMULA,
041: new Sort[] { sort1 });
042: //p(:S1):BOOL
043: LogicVariable x = new LogicVariable(new Name("x"), sort1); //x:S1
044: Function q = new RigidFunction(new Name("q"), Sort.FORMULA,
045: new Sort[] { new PrimitiveSort(new Name("Whatever")) });
046: //q(:Whatever):BOOL
047: LogicVariable z = new LogicVariable(new Name("z"), sort1); //z:S1
048: Function r = new RigidFunction(new Name("r"), Sort.FORMULA,
049: new Sort[] { sort1, sort2 });
050: //r(:S1, :S2):BOOL
051: LogicVariable y = new LogicVariable(new Name("y"), sort3); //y:S3
052: LogicVariable w = new LogicVariable(new Name("w"), sort2); //w:S2
053: Function f = new RigidFunction(new Name("f"), sort1,
054: new Sort[] { sort3 });
055: // f(:S3):S1
056:
057: LogicVariable v1 = new LogicVariable(new Name("v1"), osort1);
058: LogicVariable v2 = new LogicVariable(new Name("v2"), osort2);
059: LogicVariable v3 = new LogicVariable(new Name("v3"), osort3);
060: LogicVariable v4 = new LogicVariable(new Name("v4"), osort4);
061:
062: Function g = new RigidFunction(new Name("g"), osort3, new Sort[] {
063: osort2, osort1 });
064:
065: public TestTermFactory(String name) {
066: super (name);
067: }
068:
069: public void setUp() {
070: Term et_x = new OpTerm(x, new Term[0]);
071: Term et_px = new OpTerm(p, new Term[] { et_x });
072: et1 = et_px;
073: }
074:
075: private ProgramVariable attribute(Term t) {
076: return (ProgramVariable) ((AttributeOp) t.op()).attribute();
077: }
078:
079: private Term t1() {
080: Term t_x = tf.createFunctionTerm(x, new Term[0]);
081: Term t_px = tf.createFunctionTerm(p, new Term[] { t_x });
082: return t_px;
083: }
084:
085: private Term t2() {
086: Term t_x = tf.createFunctionTerm(x, new Term[] {});
087: Term t_w = tf.createFunctionTerm(w, new Term[] {});
088: return tf.createFunctionTerm(r, new Term[] { t_x, t_w });
089: }
090:
091: private Term t3() {
092: Term t_y = tf.createFunctionTerm(y, new Term[] {});
093: return tf.createFunctionTerm(f, new Term[] { t_y });
094: }
095:
096: public void testWrongSorts() {
097:
098: Exception exc = new Exception();
099: try {
100: Term t_z = tf.createFunctionTerm(z, new Term[0]);
101: Term t_pz = tf.createFunctionTerm(q, new Term[] { t_z });
102: } catch (TermCreationException e) {
103: exc = e;
104:
105: }
106: assertTrue(exc instanceof TermCreationException);
107: }
108:
109: public void testSimplePredicate() {
110: Assert.assertEquals(t1(), et1);
111: }
112:
113: public void testWrongArity() {
114:
115: Exception exc = new Exception();
116: try {
117: Term t_x = tf.createFunctionTerm(x, new Term[0]);
118: Term t_rx = tf.createFunctionTerm(r, new Term[] { t_x });
119: } catch (TermCreationException e) {
120: exc = e;
121: }
122: assertTrue(exc instanceof TermCreationException);
123: }
124:
125: /**
126: * subformulae are invalid built, but the term shall be
127: * constructed anyway, as subformulae are not checked
128: */
129: public void testWithInvalidSubformulae() {
130: Term invalidBuilt = new OpTerm(p, new Term[] { new OpTerm(y,
131: new Term[0]) });
132: try {
133: Term t_px_or_py = tf.createJunctorTerm(Op.OR, new Term[] {
134: invalidBuilt, t1() });
135: } catch (Exception e) {
136: fail();
137: }
138: }
139:
140: public void testConstantTrue() {
141: Term t_true = tf.createJunctorTerm(Op.TRUE, new Term[0]);
142: Assert.assertEquals(t_true, new OpTerm(Op.TRUE, new Term[0]));
143: }
144:
145: public void testQuantifierTerm() {
146: Term t_forallx_px = tf.createQuantifierTerm(Op.ALL,
147: new LogicVariable[] { x }, t1());
148: Assert.assertEquals(t_forallx_px, new QuantifierTerm(Op.ALL,
149: new LogicVariable[] { x }, t1()));
150: }
151:
152: public void testJunctorTerm() {
153: Term t_px_imp_ryw = tf.createJunctorTerm(Op.IMP, t1(), t2());
154: Assert.assertEquals(t_px_imp_ryw, new OpTerm(Op.IMP,
155: new Term[] { t1(), t2() }));
156: }
157:
158: public void testNegationTerm() {
159: Term t_not_ryw = tf.createJunctorTerm(Op.NOT, t2());
160: Assert.assertEquals(t_not_ryw, new OpTerm(Op.NOT,
161: new Term[] { t2() }));
162: }
163:
164: public void testDiamondTerm() {
165: JavaBlock jb = JavaBlock.EMPTY_JAVABLOCK;
166: Term t_dia_ryw = tf.createDiamondTerm(jb, t2());
167: Assert.assertEquals(t_dia_ryw,
168: new ProgramTerm(Op.DIA, jb, t2()));
169: }
170:
171: public void testBoxTerm() {
172: JavaBlock jb = JavaBlock.EMPTY_JAVABLOCK;
173: Term t_dia_ryw = tf.createBoxTerm(jb, t2());
174: Assert.assertEquals(t_dia_ryw,
175: new ProgramTerm(Op.BOX, jb, t2()));
176: }
177:
178: public void testSubstitutionTerm() {
179: Term t_x_subst_fy_in_px = tf.createSubstitutionTerm(Op.SUBST,
180: x, t3(), t1());
181: Assert.assertEquals(t_x_subst_fy_in_px, new SubstitutionTerm(
182: Op.SUBST, x, new Term[] { t3(), t1() }));
183: }
184:
185: public void testWrongSubstTermForLogicVariable() {
186: Exception exc = new Exception();
187: try {
188: Term t_x_subst_fy_in_px = tf.createSubstitutionTerm(
189: Op.SUBST, x, new Term[] { t2(), t1() });
190: } catch (TermCreationException e) {
191: exc = e;
192: }
193: assertTrue(exc instanceof TermCreationException);
194: }
195:
196: public void testSubtermsForLogicVariable() {
197: Exception exc = new Exception();
198: try {
199: tf.createFunctionTerm(x, new Term[] { t3() });
200: } catch (TermCreationException e) {
201: exc = e;
202: }
203: assertTrue(exc instanceof TermCreationException);
204: }
205:
206: public void testQuantifierWithNoBoundSubTerms() {
207: Exception exc = new Exception();
208: try {
209: tf.createQuantifierTerm(Op.ALL, new LogicVariable[] {},
210: t1());
211: } catch (TermCreationException e) {
212: exc = e;
213: }
214: assertTrue(exc instanceof TermCreationException);
215: }
216:
217: public void testJunctorTermWithWrongArity() {
218: Exception exc = new Exception();
219: try {
220: tf.createJunctorTerm(Op.NOT, new Term[] { t1(), t2() });
221: } catch (TermCreationException e) {
222: exc = e;
223: }
224: assertTrue(exc instanceof TermCreationException);
225: }
226:
227: public void testMetavariable() {
228: Metavariable xx = new Metavariable(new Name("xx"), sort1);
229: Term t_mv = tf.createFunctionTerm(xx, new Term[0]);
230: Term t_pxx = tf.createFunctionTerm(p, new Term[] { t_mv });
231: Assert.assertEquals(t_pxx, new OpTerm(p,
232: new Term[] { new OpTerm(xx, new Term[0]) }));
233: }
234:
235: public void testAttributeTerm() {
236: Sort s_int = new PrimitiveSort(new Name("int"));
237: ProgramVariable attribute = new LocationVariable(
238: new ProgramElementName("size"), new KeYJavaType(s_int));
239: Sort s_list = new ClassInstanceSortImpl(new Name("list"),
240: osort4, false);
241: ProgramVariable prefix = new LocationVariable(
242: new ProgramElementName("persons"), new KeYJavaType(
243: s_list));
244: Term sub = tf.createVariableTerm(prefix);
245: Term t = tf.createAttributeTerm(attribute, sub);
246: assertTrue("Operator should be of type AttributeOp",
247: t.op() instanceof AttributeOp);
248: assertSame("Sub term should be " + sub + " but is " + t.sub(0),
249: t.sub(0), sub);
250: assertSame("Wrong attribute.", attribute(t), attribute);
251: prefix = new LocationVariable(
252: new ProgramElementName("persons"), new KeYJavaType(
253: osort3));
254: sub = tf.createVariableTerm(prefix);
255: t = tf.createAttributeTerm(attribute, sub);
256: Exception exc = new Exception();
257: try {
258: prefix = new LocationVariable(new ProgramElementName(
259: "persons"), new KeYJavaType(osort1));
260: sub = tf.createVariableTerm(prefix);
261: t = tf.createAttributeTerm(attribute, sub);
262: } catch (TermCreationException e) {
263: exc = e;
264: }
265: exc = new Exception();
266: try {
267: prefix = new LocationVariable(new ProgramElementName(
268: "persons"), new KeYJavaType(s_int));
269: sub = tf.createVariableTerm(prefix);
270: t = tf.createAttributeTerm(attribute, sub);
271: } catch (TermCreationException e) {
272: exc = e;
273: }
274: assertTrue(exc instanceof TermCreationException);
275:
276: // de.uka.ilkd.key.gui.PureSequentPrinter pseq =
277: // new de.uka.ilkd.key.gui.PureSequentPrinter
278: // (null, new de.uka.ilkd.key.gui.NotationInfo(),
279: // Sequent.createAnteSequent
280: // (Semisequent.EMPTY_SEMISEQUENT.insertFirst(new ConstrainedFormula
281: // (tf.createEqualityTerm(t,t)))));
282: // pseq.printSequent();
283: // System.out.println("Prettyprint:"+pseq);
284: // System.out.println("toString:"+t);
285: }
286:
287: public void testSubSorts1() {
288: tf.createFunctionTerm(g, tf.createVariableTerm(v4), tf
289: .createVariableTerm(v1));
290: tf.createFunctionTerm(g, tf.createVariableTerm(v4), tf
291: .createVariableTerm(v4));
292: tf.createFunctionTerm(g, tf.createVariableTerm(v2), tf
293: .createVariableTerm(v3));
294: Exception exc = new Exception();
295: try {
296: tf.createFunctionTerm(g, tf.createVariableTerm(v1), tf
297: .createVariableTerm(v1));
298: } catch (TermCreationException e) {
299: exc = e;
300: }
301: assertTrue(exc instanceof TermCreationException);
302: exc = new Exception();
303: try {
304: tf.createFunctionTerm(g, tf.createVariableTerm(y), tf
305: .createVariableTerm(y));
306: } catch (TermCreationException e) {
307: exc = e;
308: }
309: assertTrue(exc instanceof TermCreationException);
310: }
311:
312: public void testSubSortsEquals() {
313: tf.createEqualityTerm(tf.createVariableTerm(v4), tf
314: .createVariableTerm(v1));
315: tf.createEqualityTerm(tf.createVariableTerm(v4), tf
316: .createVariableTerm(v4));
317: tf.createEqualityTerm(tf.createVariableTerm(v2), tf
318: .createVariableTerm(v3));
319: tf.createEqualityTerm(tf.createVariableTerm(x), tf
320: .createVariableTerm(z));
321: Exception exc = new Exception();
322: try {
323: tf.createEqualityTerm(tf.createVariableTerm(v1), tf
324: .createVariableTerm(y));
325: } catch (TermCreationException e) {
326: exc = e;
327: }
328: assertTrue(exc instanceof TermCreationException);
329: exc = null;
330: try {
331: tf.createEqualityTerm(tf.createVariableTerm(x), tf
332: .createJunctorTerm(Op.TRUE));
333: } catch (TermCreationException e) {
334: exc = e;
335: }
336: assertTrue("Expected TermCreationException. But was:" + exc,
337: exc instanceof TermCreationException);
338: }
339:
340: public void testSubSortsSubst() {
341: Term t = tf.createFunctionTerm(g, tf.createVariableTerm(v2), tf
342: .createVariableTerm(v1));
343: Function c = new RigidFunction(new Name("c"), osort2,
344: new Sort[0]);
345: Term st = tf.createSubstitutionTerm(Op.SUBST, v2, tf
346: .createFunctionTerm(c), t);
347: c = new RigidFunction(new Name("c"), osort4, new Sort[0]);
348: st = tf.createSubstitutionTerm(Op.SUBST, v2, tf
349: .createFunctionTerm(c), t);
350: c = new RigidFunction(new Name("c"), osort3, new Sort[0]);
351: st = tf.createSubstitutionTerm(Op.SUBST, v1, tf
352: .createFunctionTerm(c), t);
353: Exception exc = new Exception();
354: try {
355: c = new RigidFunction(new Name("c"), osort1, new Sort[0]);
356: st = tf.createSubstitutionTerm(Op.SUBST, v2, tf
357: .createFunctionTerm(c), t);
358: } catch (TermCreationException e) {
359: exc = e;
360: }
361: assertTrue(exc instanceof TermCreationException);
362: exc = new Exception();
363: try {
364: c = new RigidFunction(new Name("c"), osort3, new Sort[0]);
365: st = tf.createSubstitutionTerm(Op.SUBST, v2, tf
366: .createFunctionTerm(c), t);
367:
368: } catch (TermCreationException e) {
369: exc = e;
370: }
371: assertTrue(exc instanceof TermCreationException);
372: }
373:
374: }
|