[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 51 51 826 304
lib specs 953 953 3324 1050
total 1004 1004 4150 1354
copy No No 22 22 645 251
elem-option Yes No 0 0 0 0
eval No No 3 3 57 0
functions No No 26 26 124 53
node Yes No 0 0 0 0
node-heap No No 0 0 0 0
ref-map No No 0 0 0 0
store+set-r No No 0 0 0 0
successors No No 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
gref No Yes 0 0 0 0
heap No Yes 55 55 292 132
heap-sep No Yes 62 62 330 178
list No Yes 130 130 352 86
list-data Yes Yes 30 30 46 0
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 66 66 187 56
obj No Yes 0 0 0 0
ops-impl No Yes 0 0 0 0
ref No Yes 0 0 0 0
refobj No Yes 0 0 0 0
refset No Yes 0 0 0 0
separation No Yes 13 13 85 47
set-basic No Yes 96 96 390 84
set-union No Yes 186 186 619 124
store No Yes 76 76 371 126
store+set No Yes 23 23 89 29
Lines et. al. of Specifications
spec-name data? lib? lines axioms operations sorts
all specs No No 1057 147 103 16
all lib specs No No 678 110 77 11
all nonlib specs No No 379 37 26 5
all data specs No No 84 42 18 4
all nondata specs No No 985 110 86 12
all data lib specs No No 42 21 9 2
all nondata lib specs No No 636 89 68 9
all data nonlib specs No No 30 16 8 2
all nondata nonlib specs No No 349 21 18 3
copy No No 138 5 5 0
elem-option Yes No 17 5 3 1
eval No No 31 0 0 0
functions No No 78 16 13 0
node Yes No 13 11 5 1
node-heap No No 17 0 0 1
ref-map No No 50 0 0 1
store+set-r No No 5 0 0 0
successors No No 30 0 0 1
data No Yes 19 0 0 1
elem No Yes 18 0 0 1
elemdata No Yes 4 0 0 0
gref No Yes 22 0 0 0
heap No Yes 87 22 12 1
heap-sep No Yes 89 15 15 0
list No Yes 26 6 5 0
list-data Yes Yes 29 12 6 1
maplet No Yes 40 6 6 0
nat No Yes 24 5 4 0
nat-basic1 Yes Yes 13 9 3 1
nat-basic2 No Yes 23 5 1 0
obj No Yes 18 0 0 1
ops-impl No Yes 39 1 0 0
ref No Yes 18 0 1 1
refobj No Yes 19 0 0 0
refset No Yes 25 0 0 1
separation No Yes 20 2 2 0
set-basic No Yes 36 6 5 1
set-union No Yes 28 5 5 0
store No Yes 56 12 9 2
store+set No Yes 25 4 3 0