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 930 945 6757 2927 lib specs 1082 1082 4469 898 total 2012 2027 11226 3825 calculus No No 7 7 56 24 cell Yes No 1 1 2 1 cellparam No No 0 0 0 0 dlinked-list No No 12 12 96 42 dlinked-list-seg No No 18 18 150 57 dlinked-maplist No No 10 10 67 29 dlinked-maplist-seg No No 18 18 150 57 ex-maplet No No 15 15 81 33 existential No No 2 2 24 11 gownership Yes No 0 0 0 0 heap No No 34 34 112 34 heap-aux No No 82 82 271 67 heap-fun No No 35 35 175 70 heap-is-map-instance No No 0 15 87 20 heap-mod No No 6 6 238 139 heap-old No No 74 74 436 172 heap-sep No No 96 96 706 339 heapfuns No No 76 76 618 254 heapfuns-map No No 65 65 493 234 heapmap No No 1 1 4 2 iter-map No No 8 8 70 34 iter-n No No 9 9 72 30 iter-set No No 7 7 74 32 linked-list No No 10 10 92 43 linked-list-seg No No 27 27 226 95 linked-maplist No No 7 7 63 30 linked-maplist-seg No No 15 15 127 42 linked-maptree No No 6 6 28 10 linked-tree No No 9 9 97 45 linked-tree-path No No 3 3 101 53 linkedlist-of-instance No No 0 0 0 0 map-ex-maplet No No 10 10 44 16 map-maplet No No 20 20 204 95 map-sep No No 90 90 715 347 map-separation No No 21 21 104 39 maplet No No 32 32 252 111 node Yes No 0 0 0 0 ownership No No 0 0 0 0 polyref No No 0 0 0 0 reachable No No 0 0 0 0 refmap-ex-maplet No No 13 13 56 18 refmap-maplet No No 18 18 109 45 refmap-separation No No 21 21 109 44 separation No No 26 26 130 54 separation-rg No No 20 20 282 147 tree Yes No 0 0 0 0 tree-path No No 6 6 36 12 list No Yes 140 140 520 91 list-data Yes Yes 30 30 77 2 list-dup No Yes 102 102 659 161 list-last No Yes 165 165 626 148 map No Yes 80 80 461 138 nat No Yes 120 120 327 61 nat-basic No Yes 125 125 386 39 relops No Yes 5 5 44 19 set-basic No Yes 101 101 489 90 set-union No Yes 214 214 880 149

Lines et. al. of Specifications spec-name data? lib? lines axioms operations sorts all specs No No 2410 351 200 13 all lib specs No No 514 104 58 4 all nonlib specs No No 1896 247 142 9 all data specs No No 514 104 58 4 all nondata specs No No 2331 284 178 8 all data lib specs No No 23 12 4 1 all nondata lib specs No No 491 92 54 3 all data nonlib specs No No 56 55 18 4 all nondata nonlib specs No No 1840 192 124 5 calculus No No 10 0 0 0 cell Yes No 13 11 5 1 cellparam No No 14 0 3 1 dlinked-list No No 34 3 2 0 dlinked-list-seg No No 69 6 3 0 dlinked-maplist No No 34 3 2 0 dlinked-maplist-seg No No 72 6 3 0 ex-maplet No No 23 2 2 0 existential No No 19 1 1 0 gownership Yes No 11 5 3 1 heap No No 80 12 3 1 heap-aux No No 228 6 6 0 heap-fun No No 34 3 2 0 heap-is-map-instance No No 68 0 0 0 heap-mod No No 36 4 4 0 heap-old No No 111 23 9 1 heap-sep No No 79 16 16 0 heapfuns No No 66 14 6 0 heapfuns-map No No 48 8 5 0 heapmap No No 61 7 0 0 iter-map No No 32 4 2 0 iter-n No No 22 2 1 0 iter-set No No 31 4 2 0 linked-list No No 27 2 1 0 linked-list-seg No No 55 6 4 0 linked-maplist No No 27 2 1 0 linked-maplist-seg No No 51 5 3 0 linked-maptree No No 26 2 1 0 linked-tree No No 26 2 1 0 linked-tree-path No No 37 3 0 0 linkedlist-of-instance No No 5 0 0 0 map-ex-maplet No No 19 1 1 0 map-maplet No No 31 3 3 0 map-sep No No 79 16 16 0 map-separation No No 24 2 2 0 maplet No No 37 4 4 0 node Yes No 12 18 7 1 ownership No No 11 0 0 1 polyref No No 8 0 1 1 reachable No No 19 1 1 0 refmap-ex-maplet No No 23 2 2 0 refmap-maplet No No 32 3 3 0 refmap-separation No No 24 2 2 0 separation No No 28 2 2 0 separation-rg No No 36 3 3 0 tree Yes No 20 21 3 1 tree-path No No 44 7 1 0 list No Yes 60 11 7 0 list-data Yes Yes 23 12 4 1 list-dup No Yes 47 7 4 0 list-last No Yes 75 14 5 0 map No Yes 69 11 6 1 nat No Yes 25 5 3 0 nat-basic No Yes 28 12 3 1 relops No Yes 69 13 11 0 set-basic No Yes 49 6 5 1 set-union No Yes 69 13 10 0