01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: //
10:
11: package de.uka.ilkd.key.logic;
12:
13: import java.io.File;
14:
15: import junit.framework.TestCase;
16: import de.uka.ilkd.key.proof.Proof;
17: import de.uka.ilkd.key.proof.ProofAggregate;
18: import de.uka.ilkd.key.util.HelperClassForTests;
19:
20: /**
21: * class tests the term factory
22: */
23: public class TestUpdatetermNormalisation extends TestCase {
24:
25: public static final String testRules = System
26: .getProperty("key.home")
27: + File.separator
28: + "examples"
29: + File.separator
30: + "_testcase" + File.separator + "updateterm";
31:
32: private final HelperClassForTests helper = new HelperClassForTests();
33:
34: public ProofAggregate parse(File file) {
35: return helper.parse(file);
36: }
37:
38: public TestUpdatetermNormalisation(String name) {
39: super (name);
40: }
41:
42: public void setUp() {
43: }
44:
45: private Term extractProblemTerm(Proof p) {
46: return helper.extractProblemTerm(p);
47: }
48:
49: public void testLocalVariableSort() {
50: ProofAggregate proofList = parse(new File(testRules
51: + File.separator + "updatetermTest0.key"));
52: Term t = extractProblemTerm(proofList.getFirstProof());
53: assertTrue("Expected " + t.sub(1) + " but is " + t.sub(0), t
54: .sub(0).equals(t.sub(1)));
55: }
56:
57: public void testLocalVariableAttributeSort() {
58: ProofAggregate proofList = parse(new File(testRules
59: + File.separator + "updatetermTest1.key"));
60: Term t = extractProblemTerm(proofList.getFirstProof());
61: assertTrue("Expected " + t.sub(1) + " but is " + t.sub(0), t
62: .sub(0).equals(t.sub(1)));
63: }
64:
65: public void testLocalVariableAttributeArraySort() {
66: ProofAggregate proofList = parse(new File(testRules
67: + File.separator + "updatetermTest2.key"));
68: Term t = extractProblemTerm(proofList.getFirstProof());
69: assertTrue("Expected " + t.sub(1) + " but is " + t.sub(0), t
70: .sub(0).equals(t.sub(1)));
71: }
72:
73: public void testLocalVariableAttributeArrayShadowSort() {
74: ProofAggregate proofList = parse(new File(testRules
75: + File.separator + "updatetermTest3.key"));
76: Term t = extractProblemTerm(proofList.getFirstProof());
77: assertTrue("Expected " + t.sub(1) + " but is " + t.sub(0), t
78: .sub(0).equals(t.sub(1)));
79: }
80:
81: public void testNoOrdering() {
82: ProofAggregate proofList = parse(new File(testRules
83: + File.separator + "updatetermTest4.key"));
84: Term t = extractProblemTerm(proofList.getFirstProof());
85: assertTrue("Expected " + t.sub(1) + " and " + t.sub(0)
86: + " to be different", !t.sub(0).equals(t.sub(1)));
87: }
88:
89: }
|