[Imprint][Data Privacy Statement][E-Mail]

Back to the index. View project statistic. View project symbols. View KIV symbols to check that all symbols are available.

Project Statistics

The following tables contain statistical data about the project. The most significant numbers that give an impression about the effort for the project are Proofs - nonlib specs. This line contains a summary for specifications that are not imported from a library, but unique for the project. (Library specifications are orange in the development graph, the other either blue or green, depending on their status.)

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 85 132 2669 398
lib specs 2199 2220 9390 2329
total 2284 2352 12059 2727
apersistence-io-asm No No 0 23 240 11
encoding-log No No 10 10 90 36
encoding-lprops No No 0 0 0 0
encoding-lpt No No 7 7 41 17
encoding-orphans No No 7 7 71 28
encoding-ref-node No No 0 0 0 0
encoding-superblock No No 0 0 0 0
persistence-io-asm No No 31 43 1532 213
persistence-io-inv No No 29 29 161 55
persistence-io-refine No No 1 13 534 38
ref-node Yes No 0 0 0 0
superblock Yes No 0 0 0 0
address No Yes 0 0 0 0
aleb Yes Yes 1 1 2 1
align No Yes 77 77 377 89
array No Yes 14 14 46 11
array-copy No Yes 53 53 277 85
array-indices No Yes 24 24 148 51
array-splice No Yes 84 84 752 300
avolume No Yes 0 0 0 0
buffer No Yes 2 2 9 5
char No Yes 0 0 0 0
data No Yes 0 0 0 0
debug No Yes 0 0 0 0
ebm-avol-asm No Yes 0 21 188 11
ebm-vol-inv No Yes 9 9 44 11
elem No Yes 0 0 0 0
encoding No Yes 3 3 31 17
encoding-aligned No Yes 3 3 50 16
encoding-elem-alignment No Yes 0 0 0 0
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-nat No Yes 0 0 0 0
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
gelem No Yes 0 0 0 0
list No Yes 130 130 440 87
list+set No Yes 5 5 19 10
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
list-prefixn No Yes 49 49 229 43
lp-array No Yes 0 0 0 0
lprops Yes Yes 0 0 0 0
min-max No Yes 30 30 65 7
nat No Yes 120 120 302 69
nat-basic No Yes 129 129 356 39
nat-div No Yes 139 139 488 165
nat-list-less No Yes 4 4 27 5
nat-list-set No Yes 0 0 0 0
nat-mult No Yes 213 213 648 238
nat-set No Yes 6 6 36 18
oelem No Yes 8 8 18 3
oset No Yes 111 111 328 76
set-basic No Yes 96 96 444 86
set-union No Yes 197 197 770 140
string No Yes 0 0 0 0
Lines et. al. of Specifications
spec-name data? lib? lines axioms operations sorts
all specs No No 3603 443 165 20
all lib specs No No 2158 354 133 18
all nonlib specs No No 1445 89 32 2
all data specs No No 186 348 70 10
all nondata specs No No 3470 197 112 13
all data lib specs No No 93 174 35 5
all nondata lib specs No No 2065 180 98 13
all data nonlib specs No No 40 72 18 2
all nondata nonlib specs No No 1405 17 14 0
apersistence-io-asm No No 329 0 0 0
encoding-log No No 30 2 1 0
encoding-lprops No No 21 0 0 0
encoding-lpt No No 44 4 4 0
encoding-orphans No No 39 3 2 0
encoding-ref-node No No 30 0 0 0
encoding-superblock No No 27 0 0 0
persistence-io-asm No No 754 0 0 0
persistence-io-inv No No 90 8 7 0
persistence-io-refine No No 41 0 0 0
ref-node Yes No 16 6 3 1
superblock Yes No 24 66 15 1
address No Yes 26 0 0 1
aleb Yes Yes 16 10 3 1
align No Yes 30 3 3 0
array No Yes 48 5 2 1
array-copy No Yes 100 14 4 0
array-indices No Yes 83 14 10 0
array-splice No Yes 68 10 8 0
avolume No Yes 40 0 0 1
buffer No Yes 40 0 0 1
char No Yes 34 0 0 1
data No Yes 23 0 0 1
debug No Yes 23 1 1 0
ebm-avol-asm No Yes 201 0 0 0
ebm-vol-inv No Yes 44 2 2 0
elem No Yes 22 0 0 1
encoding No Yes 59 5 3 0
encoding-aligned No Yes 46 2 2 0
encoding-elem-alignment No Yes 35 1 1 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-nat No Yes 21 0 0 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
gelem No Yes 26 0 0 0
list No Yes 38 7 5 0
list+set No Yes 24 1 1 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
list-prefixn No Yes 31 3 3 0
lp-array No Yes 42 0 0 1
lprops Yes Yes 24 31 12 2
min-max No Yes 26 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-list-less No Yes 25 2 1 0
nat-list-set No Yes 72 0 0 1
nat-mult No Yes 23 2 1 0
nat-set No Yes 34 0 0 1
oelem No Yes 27 3 1 0
oset No Yes 61 8 2 0
set-basic No Yes 42 6 5 1
set-union No Yes 35 5 5 0
string No Yes 53 0 0 1