Class Name:
kiasan.examples.binomialqueue.BinomialQueue Report Rendered: Mon May 04 11:28:33 CDT 2009, by Sireum/Kiasan for Java v0.1.20090504
| Branches Covered For Tests: 41/60 (68%) | |
| Instructions Covered For Tests: 377/404 (93%) |
| Branches Covered For Class: 100/99 (101%) | |
| Instructions Covered For Class: 568/807 (70%) |
Methods Covered:
| Class / Method | T | E | Instruction Coverage | Branch Coverage | Time |
| 9 | 4 |
94/94
100%
|
16/16
100%
|
0.652s | |
| 20 | 5 |
283/310
91.29%
|
25/44
56.82%
|
0.745s | |
|
Total
|
29 | 9 |
377/404
93.32%
|
41/60
68.33%
|
1.397s |
Source Code:
1 package kiasan.examples.binomialqueue;
2
3 import kiasan.examples.common.LinkedList;
4 import kiasan.examples.common.Underflow;
5
6 /**
7 * Implements a binomial queue. Note that all "matching" is based on the
8 * compareTo method.
9 *
10 * @author Mark Allen Weiss
11 */
12 public class BinomialQueue {
13 private static class BinomialNode {
14 int element; // The data in the node
15
16 BinomialNode leftChild; // Left child
17
18 BinomialNode nextSibling; // Right child
19
20 // Constructors
21 BinomialNode(final int theElement) {
22 this(theElement, null, null);
23 }
24
25 BinomialNode(final int theElement, final BinomialNode lt,
26 final BinomialNode nt) {
27 this.element = theElement;
28 this.leftChild = lt;
29 this.nextSibling = nt;
30 }
31 }
32
33 private static final int DEFAULT_TREES = 1;
34
35 public static void main(final String[] args) {
36 final int numItems = 10000;
37 final BinomialQueue h = new BinomialQueue();
38 final BinomialQueue h1 = new BinomialQueue();
39 int i = 37;
40
41 System.out.println("Starting check.");
42
43 for (i = 37; i != 0; i = (i + 37) % numItems) {
44 if (i % 2 == 0) {
45 h1.insert(i);
46 } else {
47 h.insert(i);
48 }
49 }
50 assert h.wellFormed();
51 h.merge(h1);
52 assert h.wellFormed();
53 for (i = 1; i < numItems; i++) {
54 // assert h.wellFormed();
55 if (h.deleteMin() != i) {
56 System.out.println("Oops! " + i);
57 }
58 }
59
60 System.out.println("Check done.");
61 }
62
63 private int currentSize; // # items in priority queue
64 private BinomialNode[] theTrees; // An array of tree roots
65
66 /**
67 * Construct the binomial queue.
68 */
69 public BinomialQueue() {
70 this.theTrees = new BinomialNode[BinomialQueue.DEFAULT_TREES];
71 makeEmpty();
72 }
73
74 /**
75 * Construct with a single item.
76 */
82
83 /**
84 * Return the capacity.
85 */
86 private int capacity() {
88 }
89
90 /**
91 * Return the result of merging equal-sized t1 and t2.
92 */
93 private BinomialNode combineTrees(final BinomialNode t1, final BinomialNode t2) {
96 }
100 }
101
102 /**
103 * Remove the smallest item from the priority queue.
104 *
105 * @return the smallest item, or null, if empty.
106 */
107 public int deleteMin() {
108 if (isEmpty()) {
109 throw new Underflow();
110 }
111
112 final int minIndex = findMinIndex();
113 final int minItem = this.theTrees[minIndex].element;
114
115 BinomialNode deletedTree = this.theTrees[minIndex].leftChild;
116
117 // Construct H''
118 final BinomialQueue deletedQueue = new BinomialQueue();
119 deletedQueue.expandTheTrees(minIndex + 1);
120
121 deletedQueue.currentSize = (1 << minIndex) - 1;
122 for (int j = minIndex - 1; j >= 0; j--) {
123 deletedQueue.theTrees[j] = deletedTree;
124 deletedTree = deletedTree.nextSibling;
125 deletedQueue.theTrees[j].nextSibling = null;
126 }
127
128 // Construct H'
129 this.theTrees[minIndex] = null;
130 this.currentSize -= deletedQueue.currentSize + 1;
131
132 merge(deletedQueue);
133
134 return minItem;
135 }
136
137 private void expandTheTrees(final int newNumTrees) {
140
144 }
147 }
149
150 /**
151 * Find the smallest item in the priority queue.
152 *
153 * @return the smallest item, or null, if empty.
154 */
155 //@ requires this.wellFormed();
156 //@ ensures this.wellFormed();
157 public int findMin() {
160 }
161
163 }
164
165 /**
166 * Find index of tree containing the smallest item in the priority queue. The
167 * priority queue must not be empty.
168 *
169 * @return the index of tree containing the smallest item.
170 */
171 private int findMinIndex() {
172 int i;
173 int minIndex;
174
176 ;
177 }
178
183 }
184 }
185
187 }
188
189 /**
190 * Insert into the priority queue, maintaining heap order. This implementation
191 * is not optimized for O(1) performance.
192 *
193 * @param x
194 * the item to insert.
195 */
196 //@ requires this.wellFormed();
197 //@ ensures this.wellFormed();
198 public void insert(final int x) {
201
202 private boolean isAcyclic(final BinomialNode start,
203 final LinkedList<BinomialNode> seen) {
207 }
211 }
212 }
217 }
221 //ns = ns.nextSibling;
222 }
223 }
225 }
226
227 /**
228 * Test if the priority queue is logically empty.
229 *
230 * @return true if empty, false otherwise.
231 */
232 public boolean isEmpty() {
234 }
235
236 /**
237 * Make the priority queue logically empty.
238 */
239 public void makeEmpty() {
240 this.currentSize = 0;
241 for (int i = 0; i < this.theTrees.length; i++) {
242 this.theTrees[i] = null;
243 }
244 }
245
246 /**
247 * Merge rhs into the priority queue. rhs becomes empty. rhs must be different
248 * from this.
249 *
250 * @param rhs
251 * the other binomial queue.
252 */
253 public void merge(final BinomialQueue rhs) {
255 return;
256 }
257
259
264 }
265
270
274
276 case 0: /* No trees */
277 case 1: /* Only this */
279 case 2: /* Only rhs */
283 case 4: /* Only carry */
287 case 3: /* this and rhs */
291 case 5: /* this and carry */
295 case 6: /* rhs and carry */
296 carry = combineTrees(t2, carry);
297 rhs.theTrees[i] = null;
298 break;
299 case 7: /* All three */
300 this.theTrees[i] = carry;
301 carry = combineTrees(t1, t2);
302 rhs.theTrees[i] = null;
303 break;
304 }
305 }
306
309 }
312
313 private boolean ordered(final BinomialNode node) {
317 }
319 return false;
320 }
323 return false;
324 }
326 return false;
327 }
328 }
330 } else {
332 }
333 }
334
335 private boolean wellFormed() {
338 }
344 }
348 }
349 }
350 }
352 }
353
354 private boolean wellStructured() {
357 }
359 return false;
360 }
365 }
368 }
372 }
375 }
378 }
380 }
381 }
384 }
386 }
387
388 //specification method
389 //B_k k has to be a power of 2
390 private boolean wellStructuredBK(final BinomialNode node, int k) {
394 }
397 }
400 }
404 return false;
405 }
406 }
408 }
409 }
2
3 import kiasan.examples.common.LinkedList;
4 import kiasan.examples.common.Underflow;
5
6 /**
7 * Implements a binomial queue. Note that all "matching" is based on the
8 * compareTo method.
9 *
10 * @author Mark Allen Weiss
11 */
12 public class BinomialQueue {
13 private static class BinomialNode {
14 int element; // The data in the node
15
16 BinomialNode leftChild; // Left child
17
18 BinomialNode nextSibling; // Right child
19
20 // Constructors
21 BinomialNode(final int theElement) {
22 this(theElement, null, null);
23 }
24
25 BinomialNode(final int theElement, final BinomialNode lt,
26 final BinomialNode nt) {
27 this.element = theElement;
28 this.leftChild = lt;
29 this.nextSibling = nt;
30 }
31 }
32
33 private static final int DEFAULT_TREES = 1;
34
35 public static void main(final String[] args) {
36 final int numItems = 10000;
37 final BinomialQueue h = new BinomialQueue();
38 final BinomialQueue h1 = new BinomialQueue();
39 int i = 37;
40
41 System.out.println("Starting check.");
42
43 for (i = 37; i != 0; i = (i + 37) % numItems) {
44 if (i % 2 == 0) {
45 h1.insert(i);
46 } else {
47 h.insert(i);
48 }
49 }
50 assert h.wellFormed();
51 h.merge(h1);
52 assert h.wellFormed();
53 for (i = 1; i < numItems; i++) {
54 // assert h.wellFormed();
55 if (h.deleteMin() != i) {
56 System.out.println("Oops! " + i);
57 }
58 }
59
60 System.out.println("Check done.");
61 }
62
63 private int currentSize; // # items in priority queue
64 private BinomialNode[] theTrees; // An array of tree roots
65
66 /**
67 * Construct the binomial queue.
68 */
69 public BinomialQueue() {
70 this.theTrees = new BinomialNode[BinomialQueue.DEFAULT_TREES];
71 makeEmpty();
72 }
73
74 /**
75 * Construct with a single item.
76 */
82
83 /**
84 * Return the capacity.
85 */
86 private int capacity() {
88 }
89
90 /**
91 * Return the result of merging equal-sized t1 and t2.
92 */
93 private BinomialNode combineTrees(final BinomialNode t1, final BinomialNode t2) {
96 }
100 }
101
102 /**
103 * Remove the smallest item from the priority queue.
104 *
105 * @return the smallest item, or null, if empty.
106 */
107 public int deleteMin() {
108 if (isEmpty()) {
109 throw new Underflow();
110 }
111
112 final int minIndex = findMinIndex();
113 final int minItem = this.theTrees[minIndex].element;
114
115 BinomialNode deletedTree = this.theTrees[minIndex].leftChild;
116
117 // Construct H''
118 final BinomialQueue deletedQueue = new BinomialQueue();
119 deletedQueue.expandTheTrees(minIndex + 1);
120
121 deletedQueue.currentSize = (1 << minIndex) - 1;
122 for (int j = minIndex - 1; j >= 0; j--) {
123 deletedQueue.theTrees[j] = deletedTree;
124 deletedTree = deletedTree.nextSibling;
125 deletedQueue.theTrees[j].nextSibling = null;
126 }
127
128 // Construct H'
129 this.theTrees[minIndex] = null;
130 this.currentSize -= deletedQueue.currentSize + 1;
131
132 merge(deletedQueue);
133
134 return minItem;
135 }
136
137 private void expandTheTrees(final int newNumTrees) {
140
144 }
147 }
149
150 /**
151 * Find the smallest item in the priority queue.
152 *
153 * @return the smallest item, or null, if empty.
154 */
155 //@ requires this.wellFormed();
156 //@ ensures this.wellFormed();
157 public int findMin() {
160 }
161
163 }
164
165 /**
166 * Find index of tree containing the smallest item in the priority queue. The
167 * priority queue must not be empty.
168 *
169 * @return the index of tree containing the smallest item.
170 */
171 private int findMinIndex() {
172 int i;
173 int minIndex;
174
176 ;
177 }
178
183 }
184 }
185
187 }
188
189 /**
190 * Insert into the priority queue, maintaining heap order. This implementation
191 * is not optimized for O(1) performance.
192 *
193 * @param x
194 * the item to insert.
195 */
196 //@ requires this.wellFormed();
197 //@ ensures this.wellFormed();
198 public void insert(final int x) {
201
202 private boolean isAcyclic(final BinomialNode start,
203 final LinkedList<BinomialNode> seen) {
207 }
211 }
212 }
217 }
221 //ns = ns.nextSibling;
222 }
223 }
225 }
226
227 /**
228 * Test if the priority queue is logically empty.
229 *
230 * @return true if empty, false otherwise.
231 */
232 public boolean isEmpty() {
234 }
235
236 /**
237 * Make the priority queue logically empty.
238 */
239 public void makeEmpty() {
240 this.currentSize = 0;
241 for (int i = 0; i < this.theTrees.length; i++) {
242 this.theTrees[i] = null;
243 }
244 }
245
246 /**
247 * Merge rhs into the priority queue. rhs becomes empty. rhs must be different
248 * from this.
249 *
250 * @param rhs
251 * the other binomial queue.
252 */
253 public void merge(final BinomialQueue rhs) {
255 return;
256 }
257
259
264 }
265
270
274
276 case 0: /* No trees */
277 case 1: /* Only this */
279 case 2: /* Only rhs */
283 case 4: /* Only carry */
287 case 3: /* this and rhs */
291 case 5: /* this and carry */
295 case 6: /* rhs and carry */
296 carry = combineTrees(t2, carry);
297 rhs.theTrees[i] = null;
298 break;
299 case 7: /* All three */
300 this.theTrees[i] = carry;
301 carry = combineTrees(t1, t2);
302 rhs.theTrees[i] = null;
303 break;
304 }
305 }
306
309 }
312
313 private boolean ordered(final BinomialNode node) {
317 }
319 return false;
320 }
323 return false;
324 }
326 return false;
327 }
328 }
330 } else {
332 }
333 }
334
335 private boolean wellFormed() {
338 }
344 }
348 }
349 }
350 }
352 }
353
354 private boolean wellStructured() {
357 }
359 return false;
360 }
365 }
368 }
372 }
375 }
378 }
380 }
381 }
384 }
386 }
387
388 //specification method
389 //B_k k has to be a power of 2
390 private boolean wellStructuredBK(final BinomialNode node, int k) {
394 }
397 }
400 }
404 return false;
405 }
406 }
408 }
409 }