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;
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.LogicVariable;
017: import de.uka.ilkd.key.logic.sort.PrimitiveSort;
018: import de.uka.ilkd.key.logic.sort.Sort;
019:
020: /** class tests the tree of proof
021: */
022:
023: public class TestProofTree extends TestCase {
024: Proof p;
025: Node n1;
026: Node n2;
027: Node n3;
028: Node n4;
029: Node n5;
030: Node n6;
031: Node n7;
032: final static TermFactory tf = TermFactory.DEFAULT;
033:
034: public TestProofTree(String name) {
035: super (name);
036: }
037:
038: public void setUp() {
039: Sort s = new PrimitiveSort(new Name("s"));
040: LogicVariable b1 = new LogicVariable(new Name("b1"), s);
041: LogicVariable b2 = new LogicVariable(new Name("b2"), s);
042: LogicVariable b3 = new LogicVariable(new Name("b3"), s);
043: LogicVariable b4 = new LogicVariable(new Name("b4"), s);
044: LogicVariable b5 = new LogicVariable(new Name("b5"), s);
045: LogicVariable b6 = new LogicVariable(new Name("b6"), s);
046: LogicVariable b7 = new LogicVariable(new Name("b7"), s);
047:
048: Term t_b1 = tf.createEqualityTerm(tf.createVariableTerm(b1), tf
049: .createVariableTerm(b1));
050: Term t_b2 = tf.createEqualityTerm(tf.createVariableTerm(b2), tf
051: .createVariableTerm(b2));
052: Term t_b3 = tf.createEqualityTerm(tf.createVariableTerm(b3), tf
053: .createVariableTerm(b3));
054: Term t_b4 = tf.createEqualityTerm(tf.createVariableTerm(b4), tf
055: .createVariableTerm(b4));
056: Term t_b5 = tf.createEqualityTerm(tf.createVariableTerm(b5), tf
057: .createVariableTerm(b5));
058: Term t_b6 = tf.createEqualityTerm(tf.createVariableTerm(b6), tf
059: .createVariableTerm(b6));
060: Term t_b7 = tf.createEqualityTerm(tf.createVariableTerm(b7), tf
061: .createVariableTerm(b7));
062:
063: Sequent s1 = Sequent.createSequent(
064: Semisequent.EMPTY_SEMISEQUENT
065: .insert(
066: 0,
067: new ConstrainedFormula(t_b1,
068: Constraint.BOTTOM))
069: .semisequent(), Semisequent.EMPTY_SEMISEQUENT);
070: Sequent s2 = Sequent.createSequent(
071: Semisequent.EMPTY_SEMISEQUENT
072: .insert(
073: 0,
074: new ConstrainedFormula(t_b2,
075: Constraint.BOTTOM))
076: .semisequent(), Semisequent.EMPTY_SEMISEQUENT);
077: Sequent s3 = Sequent.createSequent(
078: Semisequent.EMPTY_SEMISEQUENT
079: .insert(
080: 0,
081: new ConstrainedFormula(t_b3,
082: Constraint.BOTTOM))
083: .semisequent(), Semisequent.EMPTY_SEMISEQUENT);
084: Sequent s4 = Sequent.createSequent(
085: Semisequent.EMPTY_SEMISEQUENT
086: .insert(
087: 0,
088: new ConstrainedFormula(t_b4,
089: Constraint.BOTTOM))
090: .semisequent(), Semisequent.EMPTY_SEMISEQUENT);
091: Sequent s5 = Sequent.createSequent(
092: Semisequent.EMPTY_SEMISEQUENT
093: .insert(
094: 0,
095: new ConstrainedFormula(t_b5,
096: Constraint.BOTTOM))
097: .semisequent(), Semisequent.EMPTY_SEMISEQUENT);
098: Sequent s6 = Sequent.createSequent(
099: Semisequent.EMPTY_SEMISEQUENT
100: .insert(
101: 0,
102: new ConstrainedFormula(t_b6,
103: Constraint.BOTTOM))
104: .semisequent(), Semisequent.EMPTY_SEMISEQUENT);
105: Sequent s7 = Sequent.createSequent(
106: Semisequent.EMPTY_SEMISEQUENT
107: .insert(
108: 0,
109: new ConstrainedFormula(t_b7,
110: Constraint.BOTTOM))
111: .semisequent(), Semisequent.EMPTY_SEMISEQUENT);
112:
113: p = new Proof(new Services());
114:
115: n1 = new Node(p, s1);
116: n2 = new Node(p, s2);
117: n3 = new Node(p, s3);
118: n4 = new Node(p, s4);
119: n5 = new Node(p, s5);
120: n6 = new Node(p, s6);
121: n7 = new Node(p, s7);
122:
123: n1.add(n2);
124: n1.add(n3);
125: n1.add(n4);
126: n3.add(n5);
127: n5.add(n6);
128: n5.add(n7);
129:
130: p.setRoot(n1);
131: }
132:
133: public void tearDown() {
134: p = null;
135: n1 = null;
136: n2 = null;
137: n3 = null;
138: n4 = null;
139: n5 = null;
140: n6 = null;
141: n7 = null;
142: }
143:
144: public static ListOfGoal emptyGoalList() {
145: return SLListOfGoal.EMPTY_LIST;
146: }
147:
148: public void testLeaves() {
149:
150: //test sanityCheck
151: assertTrue("tree should have good sanity", p.root()
152: .sanityCheckDoubleLinks());
153:
154: assertTrue("Root has sibling nr -1", n1.siblingNr() == -1);
155: assertTrue("n2 should have sibling nr 0", n2.siblingNr() == 0);
156: assertTrue("n3 should have sibling nr 1", n3.siblingNr() == 1);
157: assertTrue("n4 should have sibling nr 2", n4.siblingNr() == 2);
158: assertTrue("n5 should have sibling nr 0", n5.siblingNr() == 0);
159:
160: IteratorOfNode it = p.root().leavesIterator();
161: int i = 0;
162: while (it.hasNext()) {
163: assertEquals(it.next().toString(), (new Node[] { n2, n6,
164: n7, n4 })[i].toString());
165: i++;
166: }
167: it = p.root().childrenIterator();
168:
169: i = 0;
170: while (it.hasNext()) {
171: assertEquals(it.next().toString(),
172: (new Node[] { n2, n3, n4 })[i].toString());
173: i++;
174: }
175:
176: n3.remove();
177: assertTrue(
178: "n3 is no longer a sibling and should have sibling nr -1",
179: n3.siblingNr() == -1);
180: assertTrue("n2 should have sibling nr 0", n2.siblingNr() == 0);
181: assertTrue("n4 should have sibling nr 1", n4.siblingNr() == 1);
182:
183: it = p.root().childrenIterator();
184: i = 0;
185: while (it.hasNext()) {
186: assertEquals(it.next().toString(),
187: (new Node[] { n2, n4 })[i].toString());
188: i++;
189: }
190:
191: n1.remove(n2);
192: assertTrue(
193: "n2 is no longer a sibling and should have sibling nr -1",
194: n2.siblingNr() == -1);
195: assertTrue("n4 should have sibling nr 0", n4.siblingNr() == 0);
196:
197: it = p.root().childrenIterator();
198: i = 0;
199: while (it.hasNext()) {
200: assertEquals(it.next().toString(), (new Node[] { n4 })[i]
201: .toString());
202: i++;
203: }
204:
205: n1.remove(n4);
206: assertTrue(
207: "n4 is no longer a sibling and should have sibling nr -1",
208: n4.siblingNr() == -1);
209: assertTrue(n1.childrenCount() == 0);
210:
211: }
212:
213: }
|