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 junit.framework.TestCase;
14: import de.uka.ilkd.key.logic.op.LogicVariable;
15: import de.uka.ilkd.key.logic.sort.PrimitiveSort;
16: import de.uka.ilkd.key.logic.sort.Sort;
17:
18: /** class tests the namespace
19: */
20:
21: public class TestNamespace extends TestCase {
22:
23: Namespace ns1;
24: Namespace ns2;
25: Namespace ns3;
26:
27: Sort s1;
28: LogicVariable va;
29: LogicVariable vb;
30: LogicVariable vc;
31: LogicVariable vd;
32: LogicVariable ve;
33:
34: public TestNamespace(String name) {
35: super (name);
36: }
37:
38: public void setUp() {
39: this .s1 = new PrimitiveSort(new Name("S1"));
40: this .va = new LogicVariable(new Name("A"), s1);
41: this .vb = new LogicVariable(new Name("B"), s1);
42: this .vc = new LogicVariable(new Name("C"), s1);
43: this .vd = new LogicVariable(new Name("D"), s1);
44: this .ve = new LogicVariable(new Name("E"), s1);
45:
46: ns1 = new Namespace();
47: ns1.add(va);
48: ns1.add(vb);
49: ns2 = ns1.extended(vc);
50: ns3 = ns2.extended(vd);
51: ns3.add(ve);
52: }
53:
54: public void tearDown() {
55: ns1 = null;
56: ns2 = null;
57: ns3 = null;
58:
59: this .s1 = null;
60: this .va = null;
61: this .vb = null;
62: this .vc = null;
63: this .vd = null;
64: this .ve = null;
65: }
66:
67: public void testNamespace1() {
68: assertEquals(va, ns1.lookup(new Name("A")));
69: assertEquals(vb, ns1.lookup(new Name("B")));
70: }
71:
72: public void testNamespace2() {
73: assertEquals(va, ns2.lookup(new Name("A")));
74: assertEquals(vb, ns2.lookup(new Name("B")));
75: assertEquals(vc, ns2.lookup(new Name("C")));
76: assertNull(ns2.lookup(new Name("D")));
77: }
78:
79: public void testNamespace3() {
80: assertEquals(va, ns3.lookup(new Name("A")));
81: assertEquals(vb, ns3.lookup(new Name("B")));
82: assertEquals(vc, ns3.lookup(new Name("C")));
83: assertEquals(vd, ns3.lookup(new Name("D")));
84: assertEquals(ve, ns3.lookup(new Name("E")));
85: assertNull(ns3.lookup(new Name("F")));
86: }
87:
88: public void testEmpty() {
89: assertNull(new Namespace().lookup(new Name("A")));
90: }
91:
92: }
|