[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 231 266 4112 1099
lib specs 2854 2940 14232 3794
total 3085 3206 18344 4893
address-set-array No No 0 0 0 0
address-set-array-ops No No 17 17 125 39
btree-asm No No 3 19 1260 137
btree-inv No No 73 73 933 377
btree-refine No No 0 16 534 35
key-order No No 0 3 57 31
key-order-def No No 0 0 0 0
modification Yes No 0 0 0 0
node-index-restrict No No 20 20 106 46
node-status Yes No 0 0 0 0
restructure Yes No 0 0 0 0
separation-all No No 0 0 0 0
zbranch Yes No 0 0 0 0
zbranch-array No No 0 0 0 0
zbranch-array-ops No No 66 66 849 335
zbranch-array-sorted No No 11 11 75 31
zheap No No 0 0 0 0
znode Yes No 0 0 0 0
znode-ops No No 41 41 173 68
ablock Yes Yes 0 0 0 0
ablock-nodes No Yes 12 12 105 41
ablock-store No Yes 0 0 0 0
ablock-store-inv No Yes 93 93 686 172
ablock-store-refsize-cons No Yes 28 28 259 94
address No Yes 0 0 0 0
address-data Yes Yes 0 0 0 0
address-list-set No Yes 0 0 0 0
address-store No Yes 0 0 0 0
align No Yes 77 77 377 89
apersistence-asm No Yes 0 43 580 38
apersistence-base No Yes 33 33 191 73
array No Yes 14 14 46 11
array-copy No Yes 53 53 277 85
array-list No Yes 1 1 19 10
array-splice No Yes 84 84 752 300
aubifs-base No Yes 79 79 460 149
aubifs-inv No Yes 89 89 618 181
branch Yes Yes 0 0 0 0
branch-array No Yes 0 0 0 0
buffer No Yes 2 2 9 5
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
dentry Yes Yes 0 0 0 0
elem No Yes 0 0 0 0
elemdata No Yes 0 0 0 0
eraseblock No Yes 54 54 214 77
error Yes Yes 0 0 0 0
error-class No Yes 19 19 36 9
existential No Yes 2 2 24 11
gelem No Yes 0 0 0 0
gref No Yes 0 0 0 0
group-store No Yes 0 0 0 0
groupnode Yes Yes 0 0 0 0
heap No Yes 59 59 346 145
heap-sep No Yes 82 82 473 235
index-asm No Yes 0 43 480 22
index-base No Yes 3 3 23 11
index-store No Yes 0 0 0 0
indexnode Yes Yes 0 0 0 0
inode Yes Yes 0 0 0 0
iter-n No Yes 9 9 67 30
key Yes Yes 7 7 18 0
key-list-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
maplet No Yes 36 36 228 101
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-set No Yes 0 0 0 0
nat-mult No Yes 213 213 648 238
nat-set No Yes 6 6 36 18
nat-store No Yes 0 0 0 0
nat-store+set No Yes 1 1 15 3
node Yes Yes 0 0 0 0
node-index No Yes 0 0 0 0
node-list No Yes 0 0 0 0
node-store No Yes 1 1 1 0
obj No 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
persistence-state Yes Yes 1 1 3 1
ref No Yes 0 0 0 0
refobj No Yes 0 0 0 0
refset No Yes 0 0 0 0
root-ino No Yes 0 0 0 0
separation No Yes 15 15 100 45
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
string-less No Yes 39 39 118 47
stringset No Yes 0 0 0 0
Lines et. al. of Specifications
spec-name data? lib? lines axioms operations sorts
all specs No No 6905 946 367 51
all lib specs No No 4886 779 303 43
all nonlib specs No No 2019 167 64 8
all data specs No No 500 932 212 26
all nondata specs No No 6566 363 227 33
all data lib specs No No 250 466 106 13
all nondata lib specs No No 4636 313 197 30
all data nonlib specs No No 89 117 34 5
all nondata nonlib specs No No 1930 50 30 3
address-set-array No No 32 0 0 1
address-set-array-ops No No 31 3 2 0
btree-asm No No 1234 0 0 0
btree-inv No No 161 8 6 0
btree-refine No No 42 0 0 0
key-order No No 13 0 0 0
key-order-def No No 37 3 1 0
modification Yes No 18 40 9 1
node-index-restrict No No 34 4 2 0
node-status Yes No 16 4 3 1
restructure Yes No 17 8 3 1
separation-all No No 24 0 0 0
zbranch Yes No 18 27 8 1
zbranch-array No No 32 0 0 1
zbranch-array-ops No No 109 14 8 0
zbranch-array-sorted No No 34 4 2 0
zheap No No 68 0 0 1
znode Yes No 20 38 11 1
znode-ops No No 79 14 9 0
ablock Yes Yes 16 18 7 1
ablock-nodes No Yes 26 2 1 0
ablock-store No Yes 20 0 0 1
ablock-store-inv No Yes 93 14 11 0
ablock-store-refsize-cons No Yes 38 5 4 0
address No Yes 26 0 0 1
address-data Yes Yes 14 18 7 1
address-list-set No Yes 72 0 0 1
address-store No Yes 53 0 0 1
align No Yes 30 3 3 0
apersistence-asm No Yes 627 0 0 0
apersistence-base No Yes 101 10 8 0
array No Yes 48 5 2 1
array-copy No Yes 100 14 4 0
array-list No Yes 42 5 3 0
array-splice No Yes 68 10 8 0
aubifs-base No Yes 189 29 23 0
aubifs-inv No Yes 97 11 11 0
branch Yes Yes 16 24 8 1
branch-array No Yes 32 0 0 1
buffer No Yes 40 0 0 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
dentry Yes Yes 18 20 6 1
elem No Yes 22 0 0 1
elemdata No Yes 23 0 0 0
eraseblock No Yes 56 11 10 0
error Yes Yes 32 121 16 1
error-class No Yes 39 1 1 0
existential No Yes 27 1 1 0
gelem No Yes 26 0 0 0
gref No Yes 26 0 0 0
group-store No Yes 122 0 0 1
groupnode Yes Yes 16 27 9 1
heap No Yes 89 22 12 1
heap-sep No Yes 91 16 16 0
index-asm No Yes 566 0 0 0
index-base No Yes 25 1 1 0
index-store No Yes 122 0 0 1
indexnode Yes Yes 16 18 7 1
inode Yes Yes 21 51 13 1
iter-n No Yes 26 2 1 0
key Yes Yes 19 35 8 1
key-list-set No Yes 72 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
maplet No Yes 40 6 6 0
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-set No Yes 72 0 0 1
nat-mult No Yes 23 2 1 0
nat-set No Yes 34 0 0 1
nat-store No Yes 36 0 0 1
nat-store+set No Yes 23 0 0 0
node Yes Yes 29 88 10 1
node-index No Yes 50 0 0 1
node-list No Yes 56 0 0 1
node-store No Yes 50 0 0 1
obj No Yes 22 0 0 1
oelem No Yes 27 3 1 0
oset No Yes 61 8 2 0
page No Yes 26 2 2 0
persistence-state Yes Yes 18 23 6 1
ref No Yes 22 0 1 1
refobj No Yes 23 0 0 0
refset No Yes 27 0 0 1
root-ino No Yes 23 1 1 0
separation 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
string-less No Yes 64 11 3 0
stringset No Yes 27 0 0 1