[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 416 416 2096 729
lib specs 2124 2124 7055 2164
total 2540 2540 9151 2893
address No No 0 0 0 0
address-data Yes No 0 0 0 0
address-list No No 0 0 0 0
align No No 61 61 243 64
alink Yes No 0 0 0 0
alink-set No No 0 0 0 0
array-indices No No 24 24 122 48
array-splice No No 59 59 632 276
buffer No No 0 0 0 0
buffer-inf No No 0 0 0 0
buffer-inf-conv No No 14 14 63 34
checksum No No 2 2 8 5
checksum-data No No 0 0 0 0
dataarray No No 0 0 0 0
dataset No No 0 0 0 0
datasize No No 35 35 350 85
datastream No No 0 0 0 0
datastream-conv No No 9 9 27 15
dentry Yes No 0 0 0 0
elem-list-repr No No 2 2 4 3
elem-list-repr-base No No 0 0 0 0
elem-repr No No 2 2 4 2
eraseblock No No 30 30 84 47
error Yes No 0 0 0 0
error-class No No 16 16 23 6
file Yes No 0 0 0 0
inode Yes No 0 0 0 0
key Yes No 7 7 11 0
key-set No No 0 0 0 0
laddress Yes No 0 0 0 0
laddress-list No No 0 0 0 0
list-prefixn No No 36 36 138 25
lp-array No No 0 0 0 0
lprops Yes No 0 0 0 0
metadata No No 0 0 0 0
min-max No No 21 21 32 0
mode Yes No 0 0 0 0
nat-list No No 0 0 0 0
nat-list-less No No 4 4 24 5
nat-set No No 6 6 34 19
page No No 0 0 0 0
path No No 3 3 6 3
path-permission No No 6 6 16 6
permission No No 0 0 0 0
permission-param No No 0 0 0 0
posix-event Yes No 0 0 0 0
posix-history No No 0 0 0 0
root-ino No No 0 0 0 0
seekflag Yes No 0 0 0 0
store-access No No 76 76 268 83
store-base No No 0 0 0 0
store-iter No No 3 3 7 3
stringset No No 0 0 0 0
user No No 0 0 0 0
array No Yes 14 14 40 11
array-copy No Yes 48 48 242 77
char No Yes 0 0 0 0
data No Yes 0 0 0 0
elem No Yes 0 0 0 0
elemdata No Yes 0 0 0 0
gelem No Yes 0 0 0 0
list No Yes 131 131 354 87
list-data Yes Yes 30 30 46 0
list-del No Yes 313 313 1489 334
list-dup No Yes 104 104 572 166
list-last No Yes 167 167 458 144
nat No Yes 121 121 239 71
nat-basic1 Yes Yes 62 62 98 4
nat-basic2 No Yes 68 68 189 56
nat-div No Yes 139 139 390 160
nat-inf No Yes 69 69 195 92
nat-inf-basic Yes Yes 3 3 5 2
nat-mult No Yes 214 214 570 240
oelem No Yes 8 8 11 3
oset No Yes 112 112 235 77
oseta No Yes 2 2 2 2
set-basic No Yes 97 97 394 86
set-union No Yes 197 197 656 141
stream No Yes 217 217 857 408
stream-basic Yes Yes 4 4 6 3
string-data Yes Yes 4 4 7 0
Lines et. al. of Specifications
spec-name data? lib? lines axioms operations sorts
all specs No No 2667 731 292 45
all lib specs No No 893 183 107 11
all nonlib specs No No 1774 548 185 34
all data specs No No 192 84 40 10
all nondata specs No No 2345 231 161 27
all data lib specs No No 96 42 20 5
all nondata lib specs No No 797 141 87 6
all data nonlib specs No No 226 458 111 13
all nondata nonlib specs No No 1548 90 74 21
address No No 25 0 2 1
address-data Yes No 14 18 7 1
address-list No No 63 0 0 1
align No No 28 3 3 0
alink Yes No 14 5 3 1
alink-set No No 27 0 0 1
array-indices No No 82 14 10 0
array-splice No No 70 12 8 0
buffer No No 40 0 0 1
buffer-inf No No 87 0 0 1
buffer-inf-conv No No 30 5 3 0
checksum No No 24 1 1 0
checksum-data No No 21 0 1 1
dataarray No No 40 0 0 1
dataset No No 25 0 0 0
datasize No No 28 3 2 0
datastream No No 87 0 0 1
datastream-conv No No 30 5 3 0
dentry Yes No 16 20 8 1
elem-list-repr No No 23 2 1 0
elem-list-repr-base No No 9 0 0 1
elem-repr No No 26 1 2 0
eraseblock No No 52 12 9 0
error Yes No 30 92 14 1
error-class No No 35 1 1 0
file Yes No 14 18 7 1
inode Yes No 20 38 11 1
key Yes No 17 35 12 1
key-set No No 27 0 0 1
laddress Yes No 14 11 5 1
laddress-list No No 63 0 0 1
list-prefixn No No 29 3 3 0
lp-array No No 42 0 0 1
lprops Yes No 24 31 12 2
metadata No No 18 0 0 1
min-max No No 24 2 2 0
mode Yes No 16 4 3 1
nat-list No No 60 0 0 1
nat-list-less No No 23 2 1 0
nat-set No No 34 0 0 1
page No No 26 3 2 0
path No No 60 0 0 1
path-permission No No 36 4 4 0
permission No No 23 0 3 0
permission-param No No 21 0 1 1
posix-event Yes No 31 182 26 1
posix-history No No 37 0 0 1
root-ino No No 21 1 1 0
seekflag Yes No 16 4 3 1
store-access No No 54 13 8 0
store-base No No 27 0 2 1
store-iter No No 26 3 1 0
stringset No No 27 0 0 1
user No No 18 0 0 1
array No Yes 41 5 4 1
array-copy No Yes 79 14 11 0
char No Yes 32 0 0 1
data No Yes 21 0 0 1
elem No Yes 20 0 0 1
elemdata No Yes 6 0 0 0
gelem No Yes 24 0 0 0
list No Yes 34 6 5 0
list-data Yes Yes 30 12 6 1
list-del No Yes 91 26 11 0
list-dup No Yes 37 7 4 0
list-last No Yes 52 11 8 0
nat No Yes 26 5 4 0
nat-basic1 Yes Yes 16 9 3 1
nat-basic2 No Yes 25 3 1 0
nat-div No Yes 24 2 2 0
nat-inf No Yes 32 8 3 0
nat-inf-basic Yes Yes 15 5 3 1
nat-mult No Yes 21 2 1 0
oelem No Yes 25 3 1 0
oset No Yes 39 8 6 0
oseta No Yes 9 0 0 1
set-basic No Yes 40 6 5 1
set-union No Yes 33 5 5 0
stream No Yes 86 30 16 0
stream-basic Yes Yes 16 10 5 1
string-data Yes Yes 19 6 3 1