[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 10 10 214 103
lib specs 1158 1158 3972 1236
total 1168 1168 4186 1339
cell Yes No 0 0 0 0
cell-heap No No 0 0 0 0
dllist No No 4 4 81 42
implementation No No 6 6 133 61
reflist No No 0 0 0 0
elem No Yes 0 0 0 0
gelem No Yes 0 0 0 0
gref No Yes 0 0 0 0
heap No Yes 55 55 292 132
heap-sep No Yes 71 71 351 186
list No Yes 131 131 354 87
list-data Yes Yes 30 30 46 0
list-dup No Yes 104 104 572 166
list-last No Yes 167 167 458 144
maplet No Yes 33 33 226 113
nat No Yes 121 121 239 71
nat-basic1 Yes Yes 62 62 98 4
nat-basic2 No Yes 68 68 189 56
obj No Yes 0 0 0 0
oelem No Yes 8 8 11 3
ref No Yes 0 0 0 0
refobj No Yes 0 0 0 0
refset No Yes 0 0 0 0
separation No Yes 14 14 86 47
set-basic No Yes 97 97 394 86
set-union No Yes 197 197 656 141
Lines et. al. of Specifications
spec-name data? lib? lines axioms operations sorts
all specs No No 843 132 84 11
all lib specs No No 692 112 76 8
all nonlib specs No No 151 20 8 3
all data specs No No 90 42 18 4
all nondata specs No No 784 93 68 8
all data lib specs No No 45 21 9 2
all nondata lib specs No No 647 91 67 6
all data nonlib specs No No 14 18 7 1
all nondata nonlib specs No No 137 2 1 2
cell Yes No 14 18 7 1
cell-heap No No 17 0 0 1
dllist No No 37 2 1 0
implementation No No 34 0 0 0
reflist No No 49 0 0 1
elem No Yes 20 0 0 1
gelem No Yes 24 0 0 0
gref No Yes 24 0 0 0
heap No Yes 82 21 11 1
heap-sep No Yes 76 14 14 0
list No Yes 34 6 5 0
list-data Yes Yes 30 12 6 1
list-dup No Yes 35 7 4 0
list-last No Yes 52 11 8 0
maplet No Yes 39 6 6 0
nat No Yes 26 5 4 0
nat-basic1 Yes Yes 15 9 3 1
nat-basic2 No Yes 25 5 1 0
obj No Yes 20 0 0 1
oelem No Yes 25 3 1 0
ref No Yes 20 0 1 1
refobj No Yes 21 0 0 0
refset No Yes 27 0 0 1
separation No Yes 24 2 2 0
set-basic No Yes 40 6 5 1
set-union No Yes 33 5 5 0