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:
018: /**
019: * Tests for the term ordering classes
020: */
021:
022: public class TestTermOrdering extends TestCase {
023:
024: TermFactory tf = TermFactory.DEFAULT;
025:
026: private Sort sort1 = new PrimitiveSort(new Name("S1"));
027:
028: Function f = new RigidFunction(new Name("f"), sort1,
029: new Sort[] { sort1 });
030: // f(:S1):S1
031: Function h = new RigidFunction(new Name("h"), sort1,
032: new Sort[] { sort1 });
033: // h(:S1):S1
034: Function g = new RigidFunction(new Name("g"), sort1, new Sort[] {
035: sort1, sort1 });
036: // g(:S1,S1):S1
037: Function c = new RigidFunction(new Name("c"), sort1, new Sort[] {});
038: // c:S1
039: Function z = new RigidFunction(new Name("z"), sort1, new Sort[] {});
040: // z:S1
041:
042: ProgramVariable pv = new LocationVariable(new ProgramElementName(
043: "pv"), sort1);
044:
045: Metavariable x = new Metavariable(new Name("x"), sort1); //x:S1
046: Metavariable y = new Metavariable(new Name("y"), sort1); //y:S1
047:
048: TermOrdering depthO = new DepthTermOrdering();
049: TermOrdering nameO = new NameTermOrdering();
050: TermOrdering depthnameO = new CascadeDepthTermOrdering(
051: new NameTermOrdering());
052:
053: public TestTermOrdering(String name) {
054: super (name);
055: }
056:
057: // f(op)
058: private Term term_f(Operator op) {
059: Term t_c = term_const(op);
060: return term_f(t_c);
061: }
062:
063: private Term term_const(Operator op) {
064: if (op instanceof TermSymbol)
065: return tf.createFunctionTerm((TermSymbol) op);
066: return null;
067: }
068:
069: // f(t)
070: private Term term_f(Term t) {
071: Term t_ft = tf.createFunctionTerm(f, t);
072: return t_ft;
073: }
074:
075: // g(t, t2)
076: private Term term_g(Term t, Term t2) {
077: Term t_g = tf.createFunctionTerm(g, new Term[] { t, t2 });
078: return t_g;
079: }
080:
081: public void testEqual() {
082: // !( f(c) < f(c) )
083: Term t = term_f(c);
084: assertTrue(depthO.compare(t, t) == 0);
085: assertTrue(nameO.compare(t, t) == 0);
086: assertTrue(depthnameO.compare(t, t) == 0);
087:
088: // !( f(x) < f(x) )
089: t = term_f(x);
090: assertTrue(depthO.compare(t, t) == 0);
091: assertTrue(nameO.compare(t, t) == 0);
092: assertTrue(depthnameO.compare(t, t) == 0);
093: }
094:
095: public void testNameOrdering() {
096: // c < f(c)
097: Term t = term_const(c);
098: Term t2 = term_f(c);
099: assertTrue(nameO.compare(t, t2) < 0);
100: assertTrue(nameO.compare(t2, t) > 0);
101:
102: // f(c) < f(f(c))
103: t = term_f(c);
104: t2 = term_f(term_f(c));
105: assertTrue(nameO.compare(t, t2) < 0);
106: assertTrue(nameO.compare(t2, t) > 0);
107:
108: // f(c) < f(f(x))
109: t2 = term_f(term_f(x));
110: assertTrue(nameO.compare(t, t2) < 0);
111: assertTrue(nameO.compare(t2, t) > 0);
112:
113: // f(z) <> f(f(x))
114: t = term_f(z);
115: assertTrue(nameO.compare(t, t2) == 0);
116:
117: // f(z) > f(f(c))
118: t2 = term_f(term_f(c));
119: assertTrue(nameO.compare(t, t2) > 0);
120: assertTrue(nameO.compare(t2, t) < 0);
121:
122: // f(z) <> f(x)
123: t2 = term_f(x);
124: assertTrue(nameO.compare(t, t2) == 0);
125:
126: // f(pv) <> f(x)
127: t = term_f(pv);
128: assertTrue(nameO.compare(t, t2) == 0);
129:
130: // f(pv) > f(c)
131: t2 = term_f(c);
132: assertTrue(nameO.compare(t, t2) > 0);
133: assertTrue(nameO.compare(t2, t) < 0);
134:
135: // f(pv) > f(z)
136: t2 = term_f(z);
137: assertTrue(nameO.compare(t, t2) > 0);
138: assertTrue(nameO.compare(t2, t) < 0);
139: }
140:
141: public void testDepthOrdering() {
142: // f(c) < f(f(c))
143: Term t = term_f(c);
144: Term t2 = term_f(term_f(c));
145: assertTrue(depthO.compare(t, t2) < 0);
146: assertTrue(depthO.compare(t2, t) > 0);
147:
148: assertTrue(depthnameO.compare(t, t2) < 0);
149: assertTrue(depthnameO.compare(t2, t) > 0);
150:
151: // f(c) < f(f(x))
152: t2 = term_f(term_f(x));
153: assertTrue(depthO.compare(t, t2) < 0);
154: assertTrue(depthO.compare(t2, t) > 0);
155:
156: assertTrue(depthnameO.compare(t, t2) < 0);
157: assertTrue(depthnameO.compare(t2, t) > 0);
158:
159: // f(c) <> f(z)
160: t2 = term_f(z);
161: assertTrue(depthO.compare(t, t2) == 0);
162:
163: // g(x,y) <> f(g(x,x))
164: t = term_g(term_const(x), term_const(y));
165: t2 = term_f(term_g(term_const(x), term_const(x)));
166: assertTrue(depthO.compare(t, t2) == 0);
167:
168: assertTrue(depthnameO.compare(t, t2) == 0);
169: }
170:
171: public void testDepthNameOrdering() {
172: // f(z) < f(f(c))
173: Term t = term_f(z);
174: Term t2 = term_f(term_f(c));
175: assertTrue(depthnameO.compare(t, t2) < 0);
176: assertTrue(depthnameO.compare(t2, t) > 0);
177:
178: // f(z) <> f(x)
179: t2 = term_f(x);
180: assertTrue(depthnameO.compare(t, t2) == 0);
181:
182: // f(c) < f(z)
183: t = term_f(c);
184: t2 = term_f(z);
185: assertTrue(depthnameO.compare(t, t2) < 0);
186: assertTrue(depthnameO.compare(t2, t) > 0);
187: }
188:
189: // The examples from the script "Automatisches Beweisen"
190: public void testDepthScript() {
191: // g(x,f(c)) <> g(x,f(x))
192: Term t = term_g(term_const(x), term_f(c));
193: Term t2 = term_g(term_const(x), term_f(x));
194: assertTrue(depthO.compare(t, t2) == 0);
195:
196: // g(x,y) < f(g(x,y))
197: t = term_g(term_const(x), term_const(y));
198: t2 = term_f(t);
199: assertTrue(depthO.compare(t, t2) < 0);
200: assertTrue(depthO.compare(t2, t) > 0);
201:
202: // g(x,c) <> g(f(c),x)
203: t = term_g(term_const(x), term_const(c));
204: t2 = term_g(term_f(c), term_const(x));
205: assertTrue(depthO.compare(t, t2) == 0);
206: }
207:
208: }
|