[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 436 544 8716 1910
lib specs 2468 2516 12009 2966
total 2904 3060 20725 4876
ablock Yes No 0 0 0 0
ablock-nodes No No 12 12 105 41
ablock-store No No 0 0 0 0
ablock-store-inv No No 93 93 686 172
ablock-store-refsize-cons No No 28 28 259 94
abs-leb No No 1 1 2 0
abs-list No No 68 68 1092 435
abs-node No No 30 30 388 113
address-store No No 0 0 0 0
apersistence-asm No No 0 43 580 38
apersistence-base No No 33 33 191 73
encoding-group-node No No 0 0 0 0
encoding-index-node No No 0 0 0 0
encoding-node-base No No 3 3 5 3
encoding-node-header No No 0 0 0 0
encoding-node-headerless No No 0 0 0 0
gc-heap-base No No 0 20 27 1
gc-heap-rename No No 9 9 23 7
group-store No No 0 0 0 0
index-store No No 0 0 0 0
nat-store No No 0 0 0 0
nat-store+set No No 1 1 15 3
node-header Yes No 0 0 0 0
node-header-size No No 12 12 54 27
persistence-asm No No 19 41 1551 270
persistence-base No No 124 124 1736 364
persistence-refine No No 2 25 1999 268
persistence-state Yes No 1 1 3 1
address No Yes 0 0 0 0
address-data Yes Yes 0 0 0 0
address-list-set 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
awbuf-asm No Yes 1 49 595 40
awbuf-inv No Yes 36 36 178 59
bin-min-heap Yes Yes 0 0 0 0
bin-min-heap-inv No Yes 47 47 606 132
bin-min-heap-ops No Yes 0 0 0 0
bin-min-heap-prepost No Yes 14 14 659 154
binheap-key No Yes 0 0 0 0
branch Yes Yes 0 0 0 0
branch-array No Yes 0 0 0 0
buffer No Yes 2 2 9 5
bufleb Yes Yes 2 2 4 2
char No Yes 0 0 0 0
constants No Yes 2 2 4 0
data No Yes 0 0 0 0
debug No Yes 0 0 0 0
ebm-vol-inv No Yes 9 9 44 11
elem No Yes 0 0 0 0
elem-index Yes Yes 0 0 0 0
elemdata 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
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
groupnode Yes Yes 0 0 0 0
index-array No Yes 5 5 42 8
index-array-base No Yes 0 0 0 0
indexnode Yes Yes 0 0 0 0
key Yes Yes 7 7 18 0
key-index Yes Yes 0 0 0 0
key-index-array No Yes 0 0 0 0
keyindex-set No Yes 0 0 0 0
laddress Yes Yes 0 0 0 0
laddress-list 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
metadata No 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-pot No Yes 44 44 185 89
nat-set No Yes 6 6 36 18
node Yes Yes 0 0 0 0
oelem No Yes 8 8 18 3
oset No Yes 111 111 328 76
page No Yes 3 3 6 1
set-basic No Yes 96 96 444 86
set-union No Yes 197 197 770 140
store No Yes 76 76 444 141
store+set No Yes 40 40 163 52
store-map No Yes 0 0 0 0
string No Yes 0 0 0 0
Lines et. al. of Specifications
spec-name data? lib? lines axioms operations sorts
all specs No No 6874 785 311 47
all lib specs No No 3354 663 237 37
all nonlib specs No No 3520 122 74 10
all data specs No No 568 872 214 32
all nondata specs No No 6542 297 186 28
all data lib specs No No 284 436 107 16
all nondata lib specs No No 3070 227 130 21
all data nonlib specs No No 48 52 18 3
all nondata nonlib specs No No 3472 70 56 7
ablock Yes No 16 18 7 1
ablock-nodes No No 26 2 1 0
ablock-store No No 20 0 0 1
ablock-store-inv No No 93 14 11 0
ablock-store-refsize-cons No No 38 5 4 0
abs-leb No No 31 1 1 0
abs-list No No 52 5 3 0
abs-node No No 54 3 3 0
address-store No No 53 0 0 1
apersistence-asm No No 627 0 0 0
apersistence-base No No 101 10 8 0
encoding-group-node No No 82 0 0 1
encoding-index-node No No 82 0 0 1
encoding-node-base No No 123 2 2 0
encoding-node-header No No 26 0 0 0
encoding-node-headerless No No 12 0 0 0
gc-heap-base No No 67 0 0 0
gc-heap-rename No No 36 0 0 0
group-store No No 122 0 0 1
index-store No No 122 0 0 1
nat-store No No 36 0 0 1
nat-store+set No No 23 0 0 0
node-header Yes No 14 11 5 1
node-header-size No No 34 5 3 0
persistence-asm No No 1327 0 0 0
persistence-base No No 229 23 20 0
persistence-refine No No 56 0 0 0
persistence-state Yes No 18 23 6 1
address No Yes 26 0 0 1
address-data Yes Yes 14 18 7 1
address-list-set No Yes 72 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
awbuf-asm No Yes 479 0 0 0
awbuf-inv No Yes 73 7 6 0
bin-min-heap Yes Yes 15 11 5 1
bin-min-heap-inv No Yes 60 7 6 0
bin-min-heap-ops No Yes 146 0 0 0
bin-min-heap-prepost No Yes 74 4 4 0
binheap-key No Yes 11 0 0 0
branch Yes Yes 16 24 8 1
branch-array No Yes 32 0 0 1
buffer No Yes 40 0 0 1
bufleb Yes Yes 16 8 3 1
char No Yes 34 0 0 1
constants No Yes 26 2 3 0
data No Yes 23 0 0 1
debug No Yes 23 1 1 0
ebm-vol-inv No Yes 44 2 2 0
elem No Yes 22 0 0 1
elem-index Yes Yes 18 11 5 1
elemdata No Yes 23 0 0 0
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
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
groupnode Yes Yes 16 27 9 1
index-array No Yes 26 1 1 0
index-array-base No Yes 18 0 0 1
indexnode Yes Yes 16 18 7 1
key Yes Yes 19 35 8 1
key-index Yes Yes 18 11 5 1
key-index-array No Yes 32 0 0 1
keyindex-set No Yes 16 0 0 1
laddress Yes Yes 14 11 5 1
laddress-list No Yes 56 0 0 1
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
metadata No Yes 20 0 0 1
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-pot No Yes 36 6 2 0
nat-set No Yes 34 0 0 1
node Yes Yes 29 88 10 1
oelem No Yes 27 3 1 0
oset No Yes 61 8 2 0
page No Yes 26 2 2 0
set-basic No Yes 42 6 5 1
set-union No Yes 35 5 5 0
store No Yes 58 11 6 1
store+set No Yes 42 8 5 0
store-map No Yes 32 4 2 0
string No Yes 53 0 0 1