| Data Structure |
#Recursively- defined Integers |
#Recursively- defined Sets |
#Recursively- defined Multisets |
#Recursively- defined Predicates |
Routine |
#Basic Blocks |
Max. #Nodes in Footprint |
Total
Time(s) |
Avg. Time (s) per VC |
VCs proved valid ? |
| Sorted
List |
0 |
0 |
1 |
1 |
insert |
4 |
3 |
0.24 |
0.06 |
Yes |
| delete |
3 |
3 |
0.17 |
0.06 |
Yes |
|||||
| insertion-sort |
3 |
4 |
0.11 |
0.04 |
Yes |
|||||
| Binary Heap |
0 |
0 |
1 |
1 |
max-heapify |
5 |
8 |
1.89 |
0.38 |
Yes |
| Treap |
0 |
2 |
0 |
1 |
insert |
7 |
6 |
4.06 |
0.58 |
Yes |
| delete |
6 |
4 |
0.81 |
0.14 |
Yes |
|||||
| remove-root |
7 |
8 |
2.96 |
0.42 |
Yes |
|||||
| AVL Tree |
1 |
0 |
1 |
1 | insert |
11 |
8 |
1.45 |
0.13 |
Yes |
| delete |
18 |
7 |
2.13 |
0.19 |
Yes | |||||
| Red-Black
Tree |
1 |
0 |
1 |
1 |
insert |
19 |
8 |
1.93 |
0.11 |
Yes |
| delete |
24 |
7 |
3.22 |
0.14 |
Yes |
|||||
| B-Tree |
2 |
0 |
1 |
2 |
insert |
12 |
6 |
0.40 |
0.03 |
Yes |
| find |
8 |
3 |
0.12 |
0.02 |
Yes |
|||||
| Binomial
Heap |
0 |
0 |
1 |
3 |
delete-minimum |
3 |
7 |
0.29 |
0.10 |
Yes |
| find-minimum |
4 |
6 |
1.81 |
0.45 |
Yes |
|||||
| merge |
13 |
7 |
17.38 |
1.37 |
Yes |
|||||
| Total |
147 |