Project Statistics

theorems contains the number of theorems (not axioms) that were invented by the user.
proofs shows how many proofs were done, for a completed project this is equal to the number of user defined theorems + the number of (generated) proof obligations.
proof steps shows the number of rule applications of the calculus.
interactions is the number rule applications that were done by the user.

Proofs spec-name data? lib? theorems proofs proof steps interactions nonlib specs 15 15 230 89 lib specs 2346 2346 11435 2853 total 4722 4722 23330 5884 DLL2BST No No 5 5 119 43 dlinked-list No No 0 0 0 0 linked-tree-list No No 10 10 111 46 elem No Yes 0 0 0 0 gelem No Yes 0 0 0 0 gref No Yes 0 0 0 0 heap No Yes 78 78 437 168 heap-sep No Yes 83 83 541 247 linked-tree No Yes 6 6 27 10 list No Yes 130 130 466 80 list-data Yes Yes 28 28 70 0 list-del No Yes 315 315 1809 340 list-dup No Yes 101 101 624 146 list-getput No Yes 9 9 58 15 list-last No Yes 163 163 628 148 list-perm No Yes 138 138 866 259 list-set No Yes 136 136 767 145 maplet No Yes 36 36 252 104 nat No Yes 120 120 327 61 nat-basic No Yes 125 125 386 39 nat-div No Yes 140 140 527 166 nat-even No Yes 50 50 272 48 nat-mult No Yes 212 212 698 199 nat-pot No Yes 44 44 211 90 node Yes Yes 0 0 0 0 node-heap No Yes 0 0 0 0 obj No Yes 0 0 0 0 oelem No Yes 8 8 19 3 olist No Yes 59 59 470 127 olist-act No Yes 0 0 0 0 olist-min-max No Yes 24 24 406 131 olist-sort No Yes 27 27 98 38 ops No Yes 0 0 0 0 ref No Yes 0 0 0 0 refobj No Yes 0 0 0 0 refset No Yes 0 0 0 0 separation No Yes 15 15 102 46 set-basic No Yes 99 99 486 91 set-union No Yes 200 200 888 152 tree Yes Yes 0 0 0 0 DLL2BST 5 5 119 43 dlinked-list 0 0 0 0 linked-tree-list 10 10 111 46 elem 0 0 0 0 gelem 0 0 0 0 gref 0 0 0 0 heap 78 78 437 168 heap-sep 83 83 541 247 linked-tree 6 6 27 10 list 130 130 466 80 list-data 28 28 70 0 list-del 315 315 1809 340 list-dup 101 101 624 146 list-getput 9 9 58 15 list-last 163 163 628 148 list-perm 138 138 866 259 list-set 136 136 767 145 maplet 36 36 252 104 nat 120 120 327 61 nat-basic 125 125 386 39 nat-div 140 140 527 166 nat-even 50 50 272 48 nat-mult 212 212 698 199 nat-pot 44 44 211 90 node 0 0 0 0 node-heap 0 0 0 0 obj 0 0 0 0 oelem 8 8 19 3 olist 59 59 470 127 olist-act 0 0 0 0 olist-min-max 24 24 406 131 olist-sort 27 27 98 38 ops 0 0 0 0 ref 0 0 0 0 refobj 0 0 0 0 refset 0 0 0 0 separation 15 15 102 46 set-basic 99 99 486 91 set-union 200 200 888 152 tree 0 0 0 0

Lines et. al. of Specifications spec-name data? lib? lines axioms operations sorts all specs No No 1424 255 117 12 all lib specs No No 1208 239 108 12 all nonlib specs No No 216 16 9 0 all data specs No No 116 102 28 6 all nondata specs No No 1366 204 103 9 all data lib specs No No 58 51 14 3 all nondata lib specs No No 1150 188 94 9 all data nonlib specs No No 0 0 0 0 all nondata nonlib specs No No 216 16 9 0 DLL2BST No No 101 0 0 0 dlinked-list No No 33 3 2 0 linked-tree-list No No 82 13 7 0 elem No Yes 10 0 0 1 gelem No Yes 6 0 0 0 gref No Yes 6 0 0 0 heap No Yes 105 23 13 1 heap-sep No Yes 79 16 16 0 linked-tree No Yes 25 2 1 0 list No Yes 45 7 5 0 list-data Yes Yes 24 12 4 1 list-del No Yes 103 22 5 0 list-dup No Yes 44 7 4 0 list-getput No Yes 35 4 0 0 list-last No Yes 75 14 5 0 list-perm No Yes 39 5 3 0 list-set No Yes 50 8 4 0 maplet No Yes 42 6 6 0 nat No Yes 25 5 3 0 nat-basic No Yes 28 12 3 1 nat-div No Yes 19 2 0 0 nat-even No Yes 36 6 4 0 nat-mult No Yes 18 2 1 0 nat-pot No Yes 36 6 2 0 node Yes Yes 13 18 7 1 node-heap No Yes 14 0 0 1 obj No Yes 8 0 0 1 oelem No Yes 21 3 1 0 olist No Yes 55 11 4 0 olist-act No Yes 8 0 0 1 olist-min-max No Yes 25 4 0 0 olist-sort No Yes 22 2 1 0 ops No Yes 35 8 0 0 ref No Yes 11 0 1 1 refobj No Yes 6 0 0 0 refset No Yes 19 0 0 1 separation No Yes 24 2 2 0 set-basic No Yes 47 6 5 1 set-union No Yes 29 5 5 0 tree Yes Yes 21 21 3 1