[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 97 140 1390 385
lib specs 2147 2147 9098 2351
total 2244 2287 10488 2736
directory-tree No No 45 45 319 105
directory-tree-base No No 0 0 0 0
directory-tree-fids No No 10 10 141 68
directory-tree-inst No No 2 6 36 17
fidbag No No 0 0 0 0
fidset No No 0 0 0 0
file-data Yes No 2 2 2 0
file-data-store No No 0 0 0 0
file-handle Yes No 2 2 2 0
file-id No No 0 0 0 0
open-file-handles No No 0 0 0 0
open-file-handles-ext No No 2 2 19 8
pathset No No 0 0 0 0
posix-asm No No 5 44 704 97
posix-base No No 7 7 86 40
posix-links No No 7 7 66 35
posix-permission No No 0 0 0 0
posix-pre No No 15 15 15 15
align No Yes 77 77 377 89
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
char No Yes 0 0 0 0
data No Yes 0 0 0 0
dataset No 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
file-mode Yes Yes 0 0 0 0
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
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-mult No Yes 213 213 648 238
path No Yes 3 3 8 3
path-permission No Yes 12 12 35 10
permission No Yes 0 0 0 0
permission-param No Yes 0 0 0 0
seekflag Yes Yes 0 0 0 0
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
string No Yes 0 0 0 0
stringset 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 3219 589 196 31
all lib specs No No 1530 362 135 20
all nonlib specs No No 1689 227 61 11
all data specs No No 212 384 78 10
all nondata specs No No 3084 368 145 24
all data lib specs No No 106 192 39 5
all nondata lib specs No No 1424 170 96 15
all data nonlib specs No No 29 29 12 2
all nondata nonlib specs No No 1660 198 49 9
directory-tree No No 112 24 14 0
directory-tree-base No No 90 15 10 3
directory-tree-fids No No 32 4 2 0
directory-tree-inst No No 52 0 0 0
fidbag No No 27 0 0 1
fidset No No 27 0 0 1
file-data Yes No 14 11 5 1
file-data-store No No 50 0 0 1
file-handle Yes No 15 18 7 1
file-id No No 20 0 0 1
open-file-handles No No 49 0 0 1
open-file-handles-ext No No 26 2 1 0
pathset No No 27 0 0 1
posix-asm No No 447 0 0 0
posix-base No No 52 7 4 0
posix-links No No 28 2 2 0
posix-permission No No 20 0 0 0
posix-pre No No 601 144 16 0
align No Yes 30 3 3 0
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
char No Yes 34 0 0 1
data No Yes 23 0 0 1
dataset No Yes 25 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
file-mode Yes Yes 16 4 3 1
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
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-mult No Yes 23 2 1 0
path No Yes 53 0 0 1
path-permission No Yes 39 5 5 0
permission No Yes 25 0 3 0
permission-param No Yes 23 0 1 1
seekflag Yes Yes 16 4 3 1
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
string No Yes 53 0 0 1
stringset No Yes 27 0 0 1
user No Yes 20 0 0 1