Class Name:
kiasan.examples.aatree.AATree Report Rendered: Mon May 04 11:28:33 CDT 2009, by Sireum/Kiasan for Java v0.1.20090504
| Branches Covered For Tests: 48/48 (100%) | |
| Instructions Covered For Tests: 415/415 (100%) |
| Branches Covered For Class: 95/148 (64%) | |
| Instructions Covered For Class: 524/685 (76%) |
Methods Covered:
| Class / Method | T | E | Instruction Coverage | Branch Coverage | Time |
| 84 | 0 |
31/31
100%
|
6/6
100%
|
0.055s | |
| 9 | 1 |
37/37
100%
|
6/6
100%
|
0.239s | |
| 9 | 1 |
37/37
100%
|
6/6
100%
|
0.241s | |
| 84 | 0 |
127/127
100%
|
10/10
100%
|
0.421s | |
| 84 | 0 |
183/183
100%
|
20/20
100%
|
0.338s | |
|
Total
|
270 | 2 |
415/415
100%
|
48/48
100%
|
1.294s |
Source Code:
1 package kiasan.examples.aatree;
2
3 import kiasan.examples.common.Range;
4 import kiasan.examples.common.Underflow;
5
6 // AATree class
7 //
8 // CONSTRUCTION: with no initializer
9 //
10 // ******************PUBLIC OPERATIONS*********************
11 // void insert( x ) --> Insert x
12 // void remove( x ) --> Remove x
13 // boolean contains( x ) --> Return true if x is found
14 // Comparable findMin( ) --> Return smallest item
15 // Comparable findMax( ) --> Return largest item
16 // boolean isEmpty( ) --> Return true if empty; else false
17 // void makeEmpty( ) --> Remove all items
18 // ******************ERRORS********************************
19 // Throws UnderflowException as appropriate
20
21 /**
22 * Implements an AA-tree. Note that all "matching" is based on the compareTo
23 * method.
24 *
25 * @author Mark Allen Weiss
26 */
27 public class AATree {
28 private static class AANode {
29 int element; // The data in the node
30
31 AANode left; // Left child
32 AANode right; // Right child
33 int level; // Level
34
35 // Constructors
36 AANode(final int theElement, final AANode lt, final AANode rt) {
37 this.element = theElement;
38 this.left = lt;
39 this.right = rt;
40 this.level = 1;
41 }
42 }
43
44 // Test program; should print min and max and nothing else
45 public static void main(final String[] args) {
46 final AATree t = new AATree();
47 final int NUMS = 40000;
48 final int GAP = 307;
49
50 System.out.println("Checking... (no bad output means success)");
51
52 t.insert(NUMS * 2);
53 t.insert(NUMS * 3);
54 for (int i = GAP; i != 0; i = (i + GAP) % NUMS) {
55 t.insert(i);
56 }
57 System.out.println("Inserts complete");
58 assert t.wellFormed();
59 t.remove(t.findMax());
60 for (int i = 1; i < NUMS; i += 2) {
61 t.remove(i);
62 }
63 t.remove(t.findMax());
64 System.out.println("Removes complete");
65
66 if ((t.findMin() != 2) || (t.findMax() != NUMS - 2)) {
67 System.out.println("FindMin or FindMax error!");
68 }
69
70 for (int i = 2; i < NUMS; i += 2) {
71 if (!t.contains(i)) {
72 System.out.println("Error: find fails for " + i);
73 }
74 }
75
76 for (int i = 1; i < NUMS; i += 2) {
77 if (t.contains(i)) {
78 System.out.println("Error: Found deleted item " + i);
79 }
80 }
81 }
82
83 private AANode root;
84
85 private final AANode nullNode;
86
87 private AANode deletedNode;
88
89 private AANode lastNode;
90
91 /**
92 * Construct the tree.
93 */
94 public AATree() {
95 this.nullNode = new AANode(0, null, null);
96 this.nullNode.left = this.nullNode.right = this.nullNode;
97 this.nullNode.level = 0;
98 this.root = this.nullNode;
99 }
100
101 /**
102 * Find an item in the tree.
103 *
104 * @param x
105 * the item to search for.
106 * @return true if x is found.
107 */
108 //@ requires this.wellFormed();
109 //@ ensures this.wellFormed();
110 public boolean contains(final int x) {
113
114 for (;;) {
115 // int compareResult = x.compareTo(current.element);
116
123 } else {
125 }
126 }
127 }
128
129 /**
130 * Find the largest item in the tree.
131 *
132 * @return the largest item or throw Underflow if empty.
133 */
134 //@ requires this.wellFormed();
135 //@ ensures this.wellFormed();
136 public int findMax() {
139 }
140
142
145 }
146
148 }
149
150 /**
151 * Find the smallest item in the tree.
152 *
153 * @return the smallest item or throw UnderflowException if empty.
154 */
155 //@ requires this.wellFormed();
156 //@ ensures this.wellFormed();
157 public int findMin() {
160 }
161
163
166 }
167
169 }
170
171 /**
172 * Insert into the tree.
173 *
174 * @param x
175 * the item to insert.
176 */
177 //@ requires this.wellFormed();
178 //@ ensures (this.root != this.nullNode) && this.wellFormed();
179 public void insert(final int x) {
182
183 /**
184 * Internal method to insert into a subtree.
185 *
186 * @param x
187 * the item to insert.
188 * @param t
189 * the node that roots the subtree.
190 * @return the new root of the subtree.
191 */
192 private AANode insert(final int x, AANode t) {
195 }
196
197 // int compareResult = x.compareTo(t.element);
198
203 } else {
205 }
206
210 }
211
212 /**
213 * Test if the tree is logically empty.
214 *
215 * @return true if empty, false otherwise.
216 */
217 public boolean isEmpty() {
219 }
220
221 /**
222 * Make the tree logically empty.
223 */
224 public void makeEmpty() {
225 this.root = this.nullNode;
226 }
227
228 private boolean ordered() {
230 }
231
232 private boolean ordered(final AANode t, final Range range) {
235 }
238 }
241 }
245 }
246
247 /**
248 * Remove from the tree.
249 *
250 * @param x
251 * the item to remove.
252 */
253 //@ requires (this.lastNode == null) && (this.deletedNode == null) && this.wellFormed();
254 //@ ensures this.wellFormed();
255 public void remove(final int x) {
259
260 /**
261 * Internal method to remove from a subtree.
262 *
263 * @param x
264 * the item to remove.
265 * @param t
266 * the node that roots the subtree.
267 * @return the new root of the subtree.
268 */
269 private AANode remove(final int x, AANode t) {
271 // Step 1: Search down the tree and set lastNode and deletedNode
275 } else {
278 }
279
280 // Step 2: If at the bottom of the tree and
281 // x is present, we remove it
286 }
289 }
290
291 // Step 3: Otherwise, we are not at the bottom; rebalance
295 }
301 }
302 }
304 }
305
306 /**
307 * Rotate binary tree node with left child.
308 */
309 private AANode rotateWithLeftChild(final AANode k2) {
314 }
315
316 /**
317 * Rotate binary tree node with right child.
318 */
319 private AANode rotateWithRightChild(final AANode k1) {
324 }
325
326 /**
327 * Skew primitive for AA-trees.
328 *
329 * @param t
330 * the node that roots the tree.
331 * @return the new root after the rotation.
332 */
333 private AANode skew(AANode t) {
336 }
338 }
339
340 /**
341 * Split primitive for AA-trees.
342 *
343 * @param t
344 * the node that roots the tree.
345 * @return the new root after the rotation.
346 */
347 private AANode split(AANode t) {
351 }
353 }
354
355 private boolean validGlobals() {
358 }
362 }
364 }
365
366 private boolean wellFormed() {
369 }
372 }
374 }
375
376 // structural invariant of AATree
377 // 1. The level of a leaf node is one.
378 // 2. The level of a left child is strictly == its parent's level - 1.
379 // 3. The level of a right child is less than one or equal to that of its
380 // parent.
381 // 4. The level of a right grandchild is strictly less than that of its
382 // grandparent.
383 // 5. Every node of level greater than one must have two children.
384 private boolean wellLevel(final AANode node, final int parentLevel) {
386 return false;
387 }
390 return false;
391 } else {
393 }
394 }
398 }
399 }
403 }
406 }
407 }
410 }
414 }
416 }
418 }
419 }
2
3 import kiasan.examples.common.Range;
4 import kiasan.examples.common.Underflow;
5
6 // AATree class
7 //
8 // CONSTRUCTION: with no initializer
9 //
10 // ******************PUBLIC OPERATIONS*********************
11 // void insert( x ) --> Insert x
12 // void remove( x ) --> Remove x
13 // boolean contains( x ) --> Return true if x is found
14 // Comparable findMin( ) --> Return smallest item
15 // Comparable findMax( ) --> Return largest item
16 // boolean isEmpty( ) --> Return true if empty; else false
17 // void makeEmpty( ) --> Remove all items
18 // ******************ERRORS********************************
19 // Throws UnderflowException as appropriate
20
21 /**
22 * Implements an AA-tree. Note that all "matching" is based on the compareTo
23 * method.
24 *
25 * @author Mark Allen Weiss
26 */
27 public class AATree {
28 private static class AANode {
29 int element; // The data in the node
30
31 AANode left; // Left child
32 AANode right; // Right child
33 int level; // Level
34
35 // Constructors
36 AANode(final int theElement, final AANode lt, final AANode rt) {
37 this.element = theElement;
38 this.left = lt;
39 this.right = rt;
40 this.level = 1;
41 }
42 }
43
44 // Test program; should print min and max and nothing else
45 public static void main(final String[] args) {
46 final AATree t = new AATree();
47 final int NUMS = 40000;
48 final int GAP = 307;
49
50 System.out.println("Checking... (no bad output means success)");
51
52 t.insert(NUMS * 2);
53 t.insert(NUMS * 3);
54 for (int i = GAP; i != 0; i = (i + GAP) % NUMS) {
55 t.insert(i);
56 }
57 System.out.println("Inserts complete");
58 assert t.wellFormed();
59 t.remove(t.findMax());
60 for (int i = 1; i < NUMS; i += 2) {
61 t.remove(i);
62 }
63 t.remove(t.findMax());
64 System.out.println("Removes complete");
65
66 if ((t.findMin() != 2) || (t.findMax() != NUMS - 2)) {
67 System.out.println("FindMin or FindMax error!");
68 }
69
70 for (int i = 2; i < NUMS; i += 2) {
71 if (!t.contains(i)) {
72 System.out.println("Error: find fails for " + i);
73 }
74 }
75
76 for (int i = 1; i < NUMS; i += 2) {
77 if (t.contains(i)) {
78 System.out.println("Error: Found deleted item " + i);
79 }
80 }
81 }
82
83 private AANode root;
84
85 private final AANode nullNode;
86
87 private AANode deletedNode;
88
89 private AANode lastNode;
90
91 /**
92 * Construct the tree.
93 */
94 public AATree() {
95 this.nullNode = new AANode(0, null, null);
96 this.nullNode.left = this.nullNode.right = this.nullNode;
97 this.nullNode.level = 0;
98 this.root = this.nullNode;
99 }
100
101 /**
102 * Find an item in the tree.
103 *
104 * @param x
105 * the item to search for.
106 * @return true if x is found.
107 */
108 //@ requires this.wellFormed();
109 //@ ensures this.wellFormed();
110 public boolean contains(final int x) {
113
114 for (;;) {
115 // int compareResult = x.compareTo(current.element);
116
123 } else {
125 }
126 }
127 }
128
129 /**
130 * Find the largest item in the tree.
131 *
132 * @return the largest item or throw Underflow if empty.
133 */
134 //@ requires this.wellFormed();
135 //@ ensures this.wellFormed();
136 public int findMax() {
139 }
140
142
145 }
146
148 }
149
150 /**
151 * Find the smallest item in the tree.
152 *
153 * @return the smallest item or throw UnderflowException if empty.
154 */
155 //@ requires this.wellFormed();
156 //@ ensures this.wellFormed();
157 public int findMin() {
160 }
161
163
166 }
167
169 }
170
171 /**
172 * Insert into the tree.
173 *
174 * @param x
175 * the item to insert.
176 */
177 //@ requires this.wellFormed();
178 //@ ensures (this.root != this.nullNode) && this.wellFormed();
179 public void insert(final int x) {
182
183 /**
184 * Internal method to insert into a subtree.
185 *
186 * @param x
187 * the item to insert.
188 * @param t
189 * the node that roots the subtree.
190 * @return the new root of the subtree.
191 */
192 private AANode insert(final int x, AANode t) {
195 }
196
197 // int compareResult = x.compareTo(t.element);
198
203 } else {
205 }
206
210 }
211
212 /**
213 * Test if the tree is logically empty.
214 *
215 * @return true if empty, false otherwise.
216 */
217 public boolean isEmpty() {
219 }
220
221 /**
222 * Make the tree logically empty.
223 */
224 public void makeEmpty() {
225 this.root = this.nullNode;
226 }
227
228 private boolean ordered() {
230 }
231
232 private boolean ordered(final AANode t, final Range range) {
235 }
238 }
241 }
245 }
246
247 /**
248 * Remove from the tree.
249 *
250 * @param x
251 * the item to remove.
252 */
253 //@ requires (this.lastNode == null) && (this.deletedNode == null) && this.wellFormed();
254 //@ ensures this.wellFormed();
255 public void remove(final int x) {
259
260 /**
261 * Internal method to remove from a subtree.
262 *
263 * @param x
264 * the item to remove.
265 * @param t
266 * the node that roots the subtree.
267 * @return the new root of the subtree.
268 */
269 private AANode remove(final int x, AANode t) {
271 // Step 1: Search down the tree and set lastNode and deletedNode
275 } else {
278 }
279
280 // Step 2: If at the bottom of the tree and
281 // x is present, we remove it
286 }
289 }
290
291 // Step 3: Otherwise, we are not at the bottom; rebalance
295 }
301 }
302 }
304 }
305
306 /**
307 * Rotate binary tree node with left child.
308 */
309 private AANode rotateWithLeftChild(final AANode k2) {
314 }
315
316 /**
317 * Rotate binary tree node with right child.
318 */
319 private AANode rotateWithRightChild(final AANode k1) {
324 }
325
326 /**
327 * Skew primitive for AA-trees.
328 *
329 * @param t
330 * the node that roots the tree.
331 * @return the new root after the rotation.
332 */
333 private AANode skew(AANode t) {
336 }
338 }
339
340 /**
341 * Split primitive for AA-trees.
342 *
343 * @param t
344 * the node that roots the tree.
345 * @return the new root after the rotation.
346 */
347 private AANode split(AANode t) {
351 }
353 }
354
355 private boolean validGlobals() {
358 }
362 }
364 }
365
366 private boolean wellFormed() {
369 }
372 }
374 }
375
376 // structural invariant of AATree
377 // 1. The level of a leaf node is one.
378 // 2. The level of a left child is strictly == its parent's level - 1.
379 // 3. The level of a right child is less than one or equal to that of its
380 // parent.
381 // 4. The level of a right grandchild is strictly less than that of its
382 // grandparent.
383 // 5. Every node of level greater than one must have two children.
384 private boolean wellLevel(final AANode node, final int parentLevel) {
386 return false;
387 }
390 return false;
391 } else {
393 }
394 }
398 }
399 }
403 }
406 }
407 }
410 }
414 }
416 }
418 }
419 }