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 30 90 2078 312 lib specs 1727 1745 7717 1958 total 1757 1835 9795 2270 aecheader Yes No 1 1 3 1 apeb Yes No 0 0 0 0 apebs No No 0 0 0 0 aubi-io-asm No No 0 29 460 38 avidheader Yes No 1 1 3 1 echeader Yes No 0 0 0 0 encoding-echeader No No 0 0 0 0 encoding-vidheader No No 0 0 0 0 ubi-io-abs No No 15 15 91 16 ubi-io-asm No No 0 16 338 48 ubi-io-base No No 1 1 24 0 ubi-io-inv No No 11 11 53 5 ubi-io-pre No No 0 0 0 0 ubi-io-refine No No 1 16 1106 203 vidheader Yes No 0 0 0 0 align No Yes 77 77 377 89 array No Yes 14 14 46 11 array-copy No Yes 53 53 277 85 array-splice No Yes 84 84 752 300 bool Yes Yes 0 0 0 0 buffer No Yes 2 2 9 5 char No Yes 0 0 0 0 checksum No Yes 2 2 4 2 data No Yes 0 0 0 0 datasize No Yes 35 35 345 71 debug No Yes 0 0 0 0 elem No Yes 0 0 0 0 encoding No Yes 3 3 31 17 encoding-elem-size No Yes 0 0 0 0 encoding-fixed-size No Yes 1 1 2 1 encoding-fixed-size-nonempty No Yes 6 6 50 11 encoding-page-size-nonempty No Yes 5 5 47 14 eraseblock No Yes 54 54 214 77 error Yes Yes 0 0 0 0 error-class No Yes 19 19 36 9 list No Yes 130 130 440 87 list-data Yes Yes 29 29 68 0 list-del No Yes 311 311 1700 334 list-dup No Yes 104 104 600 147 list-last No Yes 163 163 579 153 min-max No Yes 30 30 65 7 mtd-asm No Yes 1 19 260 22 mtd-base No Yes 3 3 21 5 nat No Yes 120 120 302 69 nat-basic No Yes 129 129 356 39 nat-div No Yes 139 139 488 165 nat-mult No Yes 213 213 648 238 peb Yes Yes 0 0 0 0 pebs No Yes 0 0 0 0 string No Yes 0 0 0 0 volid No Yes 0 0 0 0

Lines et. al. of Specifications spec-name data? lib? lines axioms operations sorts all specs No No 2727 454 154 19 all lib specs No No 1565 292 99 13 all nonlib specs No No 1162 162 55 6 all data specs No No 166 306 58 8 all nondata specs No No 2546 161 92 10 all data lib specs No No 83 153 29 4 all nondata lib specs No No 1482 139 70 9 all data nonlib specs No No 98 140 33 5 all nondata nonlib specs No No 1064 22 22 1 aecheader Yes No 19 13 4 1 apeb Yes No 20 38 11 1 apebs No No 32 0 0 1 aubi-io-asm No No 302 0 0 0 avidheader Yes No 25 45 4 1 echeader Yes No 14 6 3 1 encoding-echeader No No 30 0 0 0 encoding-vidheader No No 30 0 0 0 ubi-io-abs No No 83 6 5 0 ubi-io-asm No No 380 0 1 0 ubi-io-base No No 40 2 2 0 ubi-io-inv No No 51 4 4 0 ubi-io-pre No No 85 10 10 0 ubi-io-refine No No 31 0 0 0 vidheader Yes No 20 38 11 1 align No Yes 30 3 3 0 array No Yes 48 5 2 1 array-copy No Yes 100 14 4 0 array-splice No Yes 68 10 8 0 bool Yes Yes 16 2 2 1 buffer No Yes 40 0 0 1 char No Yes 34 0 0 1 checksum No Yes 25 1 1 0 data No Yes 23 0 0 1 datasize No Yes 30 3 2 0 debug No Yes 23 1 1 0 elem No Yes 22 0 0 1 encoding No Yes 59 5 3 0 encoding-elem-size No Yes 34 0 1 0 encoding-fixed-size No Yes 26 2 0 0 encoding-fixed-size-nonempty No Yes 51 2 2 0 encoding-page-size-nonempty No Yes 50 2 2 0 eraseblock No Yes 56 11 10 0 error Yes Yes 32 121 16 1 error-class No Yes 39 1 1 0 list No Yes 38 7 5 0 list-data Yes Yes 21 12 4 1 list-del No Yes 101 26 5 0 list-dup No Yes 39 7 4 0 list-last No Yes 62 14 5 0 min-max No Yes 26 2 2 0 mtd-asm No Yes 181 0 0 0 mtd-base No Yes 41 2 2 0 nat No Yes 31 5 3 0 nat-basic No Yes 42 12 3 1 nat-div No Yes 32 2 0 0 nat-mult No Yes 23 2 1 0 peb Yes Yes 14 18 7 1 pebs No Yes 32 0 0 1 string No Yes 53 0 0 1 volid No Yes 23 0 0 1