[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 124 163 11777 1299
lib specs 3012 3094 17448 4344
total 3136 3257 29225 5643
file-id-data Yes No 0 0 0 0
open-files No No 0 0 0 0
posix-refine No No 32 52 4564 473
vfs-abs No No 45 45 656 245
vfs-asm No No 13 32 5251 248
vfs-base No No 13 13 64 16
vfs-contracts No No 21 21 1242 317
vfs-permission No No 0 0 0 0
abstract-dir Yes Yes 0 0 0 0
abstract-file Yes Yes 0 0 0 0
afs-asm No Yes 17 56 2779 140
afs-base No Yes 85 85 579 148
afs-contracts No Yes 10 10 624 84
afs-pre No Yes 0 0 0 0
afs-stream No Yes 28 28 209 93
align No Yes 77 77 377 89
alink Yes Yes 0 0 0 0
alink-set No Yes 0 0 0 0
array No Yes 14 14 46 11
array-copy No Yes 53 53 277 85
array-splice No Yes 84 84 752 300
bag-basic No Yes 7 7 24 6
bag-union No Yes 45 45 253 98
buffer No Yes 2 2 9 5
buffer-inf No Yes 0 0 0 0
buffer-inf-conv No Yes 14 14 64 32
buffer-option Yes Yes 0 0 0 0
char No Yes 0 0 0 0
data No Yes 0 0 0 0
dentry Yes Yes 0 0 0 0
dir-entries No Yes 0 0 0 0
dir-heap No Yes 0 0 0 0
directory-tree No Yes 45 45 319 105
directory-tree-base No Yes 0 0 0 0
directory-tree-fids No Yes 10 10 141 68
directory-tree-inst No Yes 2 6 36 17
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
fidbag No Yes 0 0 0 0
fidset No Yes 0 0 0 0
file Yes Yes 0 0 0 0
file-content No Yes 0 0 0 0
file-data Yes Yes 2 2 2 0
file-data-store No Yes 0 0 0 0
file-handle Yes Yes 2 2 2 0
file-heap No Yes 0 0 0 0
file-id No Yes 0 0 0 0
file-mode Yes Yes 0 0 0 0
gelem No Yes 0 0 0 0
gref No Yes 0 0 0 0
heap No Yes 59 59 346 145
heap-sep No Yes 82 82 473 235
inode Yes Yes 0 0 0 0
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
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-inf No Yes 72 72 203 76
nat-mult No Yes 213 213 648 238
nat-set No Yes 6 6 36 18
obj No Yes 0 0 0 0
oelem No Yes 8 8 18 3
open-file-handles No Yes 0 0 0 0
open-file-handles-ext No Yes 2 2 19 8
oset No Yes 111 111 328 76
page No Yes 3 3 6 1
path No Yes 3 3 8 3
path-permission No Yes 12 12 35 10
pathset No Yes 0 0 0 0
permission No Yes 0 0 0 0
permission-param No Yes 0 0 0 0
posix-asm No Yes 5 44 704 97
posix-base No Yes 7 7 86 40
posix-links No Yes 7 7 66 35
posix-permission No Yes 0 0 0 0
posix-pre No Yes 15 15 15 15
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
seekflag Yes 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
stream No Yes 218 218 957 408
stream-basic Yes Yes 4 4 10 3
string No Yes 0 0 0 0
user No Yes 0 0 0 0
Lines et. al. of Specifications
spec-name data? lib? lines axioms operations sorts
all specs No No 6887 897 359 51
all lib specs No No 5469 872 340 49
all nonlib specs No No 1418 25 19 2
all data specs No No 502 700 188 28
all nondata specs No No 6622 543 263 36
all data lib specs No No 251 350 94 14
all nondata lib specs No No 5218 522 246 35
all data nonlib specs No No 14 4 2 1
all nondata nonlib specs No No 1404 21 17 1
file-id-data Yes No 14 4 2 1
open-files No No 49 0 0 1
posix-refine No No 31 0 0 0
vfs-abs No No 99 12 7 0
vfs-asm No No 1101 0 0 0
vfs-base No No 40 5 6 0
vfs-contracts No No 64 4 4 0
vfs-permission No No 20 0 0 0
abstract-dir Yes Yes 20 38 11 1
abstract-file Yes Yes 17 27 9 1
afs-asm No Yes 642 0 0 0
afs-base No Yes 182 24 21 0
afs-contracts No Yes 30 1 1 0
afs-pre No Yes 188 17 17 0
afs-stream No Yes 43 4 4 0
align No Yes 30 3 3 0
alink Yes Yes 14 5 3 1
alink-set No Yes 27 0 0 1
array No Yes 48 5 2 1
array-copy No Yes 100 14 4 0
array-splice No Yes 68 10 8 0
bag-basic No Yes 36 3 3 1
bag-union No Yes 49 11 7 0
buffer No Yes 40 0 0 1
buffer-inf No Yes 80 0 0 1
buffer-inf-conv No Yes 32 5 3 0
buffer-option Yes Yes 16 11 4 1
char No Yes 34 0 0 1
data No Yes 23 0 0 1
dentry Yes Yes 18 20 6 1
dir-entries No Yes 50 0 0 1
dir-heap No Yes 79 0 0 1
directory-tree No Yes 112 24 14 0
directory-tree-base No Yes 90 15 10 3
directory-tree-fids No Yes 32 4 2 0
directory-tree-inst No Yes 52 0 0 0
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
fidbag No Yes 27 0 0 1
fidset No Yes 27 0 0 1
file Yes Yes 14 18 7 1
file-content No Yes 29 0 0 1
file-data Yes Yes 14 11 5 1
file-data-store No Yes 50 0 0 1
file-handle Yes Yes 15 18 7 1
file-heap No Yes 79 0 0 1
file-id No Yes 20 0 0 1
file-mode Yes Yes 16 4 3 1
gelem No Yes 26 0 0 0
gref No Yes 26 0 0 0
heap No Yes 89 22 12 1
heap-sep No Yes 91 16 16 0
inode Yes Yes 21 51 13 1
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
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-inf No Yes 48 13 5 1
nat-mult No Yes 23 2 1 0
nat-set No Yes 34 0 0 1
obj No Yes 22 0 0 1
oelem No Yes 27 3 1 0
open-file-handles No Yes 49 0 0 1
open-file-handles-ext No Yes 26 2 1 0
oset No Yes 61 8 2 0
page No Yes 26 2 2 0
path No Yes 53 0 0 1
path-permission No Yes 39 5 5 0
pathset No Yes 27 0 0 1
permission No Yes 25 0 3 0
permission-param No Yes 23 0 1 1
posix-asm No Yes 447 0 0 0
posix-base No Yes 52 7 4 0
posix-links No Yes 28 2 2 0
posix-permission No Yes 20 0 0 0
posix-pre No Yes 601 144 16 0
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
seekflag Yes Yes 16 4 3 1
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
stream No Yes 114 30 7 0
stream-basic Yes Yes 17 10 3 1
string No Yes 53 0 0 1
user No Yes 20 0 0 1