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.*;
015: import de.uka.ilkd.key.logic.sort.PrimitiveSort;
016: import de.uka.ilkd.key.logic.sort.Sort;
017: import de.uka.ilkd.key.rule.TacletForTests;
018:
019: /** class tests the term factory
020: */
021:
022: public class TestTerm extends TestCase {
023:
024: private TermFactory tf = TermFactory.DEFAULT;
025:
026: private Term et1;
027: private Sort sort1 = new PrimitiveSort(new Name("S1"));
028: private Sort sort2 = new PrimitiveSort(new Name("S2"));
029: private Sort sort3 = new PrimitiveSort(new Name("S3"));
030: private String invalidTermMessage = "Term not valid with given subterms";
031:
032: Function p = new RigidFunction(new Name("p"), Sort.FORMULA,
033: new Sort[] { sort1 });
034: //p(:S1):BOOL
035: LogicVariable x = new LogicVariable(new Name("x"), sort1); //x:S1
036: Function q = new RigidFunction(new Name("q"), Sort.FORMULA,
037: new Sort[] { new PrimitiveSort(new Name("Whatever")) });
038: //q(:Whatever):BOOL
039: LogicVariable z = new LogicVariable(new Name("z"), sort1); //z:S1
040: LogicVariable zz = new LogicVariable(new Name("zz"), sort1); //zz:S1
041: Function r = new RigidFunction(new Name("r"), Sort.FORMULA,
042: new Sort[] { sort1, sort2 });
043: //r(:S1, :S2):BOOL
044: LogicVariable y = new LogicVariable(new Name("y"), sort3); //y:S3
045: LogicVariable w = new LogicVariable(new Name("w"), sort2); //w:S2
046: Function f = new RigidFunction(new Name("f"), sort1,
047: new Sort[] { sort3 });
048: // f(:S3):S1
049:
050: ProgramVariable pv0 = new LocationVariable(new ProgramElementName(
051: "pv0"), sort1); //pv0:S1
052:
053: public TestTerm(String name) {
054: super (name);
055: }
056:
057: public void setUp() {
058:
059: Term et_x = new OpTerm(x, new Term[0]);
060: Term et_px = new OpTerm(p, new Term[] { et_x });
061: et1 = et_px;
062:
063: }
064:
065: private Term t1() {
066: Term t_x = tf.createFunctionTerm(x, new Term[0]);
067: Term t_px = tf.createFunctionTerm(p, new Term[] { t_x });
068: return t_px;
069: }
070:
071: private Term t2() {
072: Term t_x = tf.createFunctionTerm(x, new Term[] {});
073: Term t_w = tf.createFunctionTerm(w, new Term[] {});
074: return tf.createFunctionTerm(r, new Term[] { t_x, t_w });
075: }
076:
077: private Term t3() {
078: Term t_y = tf.createFunctionTerm(y, new Term[] {});
079: return tf.createFunctionTerm(f, new Term[] { t_y });
080: }
081:
082: private Term t4() {
083: Term t_pv0 = tf.createVariableTerm(pv0);
084: Term t_ppv0 = tf.createFunctionTerm(p, new Term[] { t_pv0 });
085: return t_ppv0;
086: }
087:
088: public void testFreeVars1() {
089: Term t_allxt2 = tf.createQuantifierTerm(Op.ALL,
090: new LogicVariable[] { x }, t2());
091: Term t_allxt2_andt1 = tf.createJunctorTerm(Op.AND, t_allxt2,
092: t1());
093: assertTrue(t_allxt2_andt1.freeVars().contains(w)
094: && t_allxt2_andt1.freeVars().contains(x));
095: }
096:
097: public void testFreeVars2() {
098: Term t_allxt2 = tf.createQuantifierTerm(Op.ALL,
099: new LogicVariable[] { w }, t2());
100: Term t_allxt2_andt1 = tf.createJunctorTerm(Op.AND, t_allxt2,
101: t1());
102: assertTrue(!t_allxt2_andt1.freeVars().contains(w)
103: && t_allxt2_andt1.freeVars().contains(x));
104: }
105:
106: public void testFreeVars3() {
107: Term t_allxt1 = tf.createQuantifierTerm(Op.ALL,
108: new LogicVariable[] { x }, t2());
109: Term t_allxt1_andt2 = tf.createJunctorTerm(Op.AND, t_allxt1,
110: t1());
111: Term t_exw_allxt1_andt2 = tf.createQuantifierTerm(Op.EX,
112: new LogicVariable[] { w }, t_allxt1_andt2);
113: assertTrue(!t_exw_allxt1_andt2.freeVars().contains(w)
114: && t_exw_allxt1_andt2.freeVars().contains(x));
115: }
116:
117: public void testFreeVars4() {
118: Term t_allxt1 = tf.createQuantifierTerm(Op.ALL,
119: new LogicVariable[] { x }, t2());
120: Term t_allxt1_andt2 = tf.createJunctorTerm(Op.AND, t_allxt1,
121: t1());
122: Term t_exw_allxt1_andt2 = tf.createQuantifierTerm(Op.EX,
123: new LogicVariable[] { w, x }, t_allxt1_andt2);
124: assertTrue(!t_exw_allxt1_andt2.freeVars().contains(w)
125: && !t_exw_allxt1_andt2.freeVars().contains(x));
126: }
127:
128: public void testProgramElementEqualsModRenaming() {
129:
130: Term match1 = TacletForTests
131: .parseTerm("\\<{ int i; }\\>true & \\<{ int i; }\\>true");
132: Term match2 = TacletForTests.parseTerm("\\<{ int i; }\\>true ");
133: assertTrue("Terms should be equalModRenaming (0).", match1.sub(
134: 0).equalsModRenaming(match2));
135: assertTrue("Terms should be equalModRenaming (1).", match1.sub(
136: 0).equalsModRenaming(match1.sub(1)));
137: Term match3 = TacletForTests
138: .parseTerm("\\<{ int j = 0; }\\>true ");
139: assertTrue("Terms should not be equal.", !match1.equals(match3));
140:
141: }
142:
143: public void testEqualsModRenamingWithLabels() {
144: Term match1 = TacletForTests
145: .parseTerm("\\<{ label0:{ label1:{ } } }\\>true");
146: Term match2 = TacletForTests
147: .parseTerm("\\<{ label0:{ label1:{ } } }\\>true");
148: assertTrue("Terms should be equalModRenaming.", match1
149: .equalsModRenaming(match2));
150: Term match3 = TacletForTests
151: .parseTerm("\\<{ label0:{ label1:{ int i = 0; } } }\\>true");
152: Term match4 = TacletForTests
153: .parseTerm("\\<{ label0:{ label1:{ int j = 0; } } }\\>true");
154: assertTrue("Terms should be equalModRenaming.", match3
155: .equalsModRenaming(match4));
156: Term match5 = TacletForTests
157: .parseTerm("\\<{ label0:{ label1:{ int i = 0; } } }\\>true");
158: Term match6 = TacletForTests
159: .parseTerm("\\<{ label0:{ label1:{ int i = 0; } } }\\>true");
160: assertTrue("Terms should be equalModRenaming.", match5
161: .equalsModRenaming(match6));
162: }
163:
164: public void testEqualsModRenaming() {
165:
166: final Term px = tf.createFunctionTerm(p, tf
167: .createVariableTerm(x));
168: final Term quant1 = tf.createQuantifierTerm(Op.ALL, z, tf
169: .createQuantifierTerm(Op.ALL, zz, tf
170: .createQuantifierTerm(Op.ALL, x, px)));
171:
172: final Term pz = tf.createFunctionTerm(p, tf
173: .createVariableTerm(z));
174: final Term quant2 = tf.createQuantifierTerm(Op.ALL, z, tf
175: .createQuantifierTerm(Op.ALL, z, tf
176: .createQuantifierTerm(Op.ALL, z, pz)));
177:
178: assertTrue("Terms " + quant1 + " and " + quant2
179: + " should be equal mod renaming", quant1
180: .equalsModRenaming(quant2));
181:
182: }
183:
184: /* public void testProgramElementEquals() {
185:
186: Term match1 = TacletForTests.parseTerm("<{ int i = 0; }>true ");
187: Term match2 = TacletForTests.parseTerm("<{ int i = 0; }>true ");
188: assertEquals("Terms should be equal.", match1, match2);
189:
190: Term match3 = TacletForTests.parseTerm("<{ int j = 0; }>true ");
191: assertTrue("Terms should not be equal.", !match1.equals(match3));
192:
193: }
194: */
195: // public void testsimpleUpdate() {
196: // Term t1 = TacletForTests.parseTerm("<{int j,k,l;}>{k:=l}"
197: // +"{l:=l}{j:=j}<{ int i = 0;k=0; }>true ");
198: // Term t2 = TacletForTests.parseTerm("<{int j,l,k;}>{j:=j}"
199: // +"{l:=k}{j:=k}{j:=j}{j:=j}<{ int i = 0;l=0; }>true ");
200: // assertTrue("Terms should be equalModRenaming and mod \"simple\" updates.",
201: // t1.equalsModRenamingModsU(t2));
202: // Term t3 = TacletForTests.parseTerm("<{int j,k,l;}>{k:=k}"
203: // +"{j:=Z(3(#))}<{ int i = 0; }>true ");
204: // Term t4 = TacletForTests.parseTerm("<{int j,l,k;}>{j:=j}"
205: // +"{l:=Z(3(#))}{j:=l}<{ int i = 0;l=0; }>true ");
206: // assertTrue("Terms should not be equalModRenaming and mod \"simple\" updates.",
207: // !t1.equalsModRenamingModsU(t3));
208: // assertTrue("Terms should not be equalModRenaming and mod \"simple\" updates.",
209: // !t2.equalsModRenamingModsU(t4));
210: // }
211:
212: public void testRigidness0() {
213: assertTrue("Term t1 should be rigid", t1().isRigid());
214: assertTrue("Term t2 should be rigid", t2().isRigid());
215: assertTrue("Term t3 should be rigid", t3().isRigid());
216: assertFalse("Term t4 should not be rigid", t4().isRigid());
217: }
218:
219: }
|