[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 9 18 308 64
lib specs 1748 1748 7456 1901
total 1757 1766 7764 1965
caterpillar-asm No No 0 3 16 0
caterpillar-refines-tree-buffer No No 2 5 52 7
del-lists No No 3 3 56 22
implementation-asm No No 0 0 0 0
implementation-refines-caterpillar No No 4 7 184 35
tree-buffer-asm No No 0 0 0 0
cell Yes Yes 1 1 1 1
cell-heap No Yes 0 0 0 0
elem 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
linked-list No Yes 7 7 66 33
linked-list-seg No Yes 15 15 122 40
list No Yes 130 130 440 87
list-data Yes Yes 28 28 66 0
list-del No Yes 311 311 1706 336
list-dup No Yes 101 101 595 145
list-last No Yes 163 163 579 153
list-prefixn No Yes 49 49 229 43
maplet No Yes 36 36 228 101
nat No Yes 120 120 296 66
nat-basic No Yes 125 125 355 39
nat-mult No Yes 212 212 602 202
obj No Yes 0 0 0 0
ops No Yes 0 0 35 3
ref No Yes 0 0 0 0
reflist No Yes 0 0 0 0
refobj No Yes 0 0 0 0
refset No Yes 0 0 0 0
separation No Yes 15 15 100 45
set-basic No Yes 96 96 444 86
set-union No Yes 198 198 773 141
Lines et. al. of Specifications
spec-name data? lib? lines axioms operations sorts
all specs No No 1385 174 91 11
all lib specs No No 1043 170 89 11
all nonlib specs No No 342 4 2 0
all data specs No No 82 46 18 4
all nondata specs No No 1344 151 82 9
all data lib specs No No 41 23 9 2
all nondata lib specs No No 1002 147 80 9
all data nonlib specs No No 0 0 0 0
all nondata nonlib specs No No 342 4 2 0
caterpillar-asm No No 78 0 0 0
caterpillar-refines-tree-buffer No No 22 0 0 0
del-lists No No 33 3 2 0
implementation-asm No No 120 1 0 0
implementation-refines-caterpillar No No 27 0 0 0
tree-buffer-asm No No 62 0 0 0
cell Yes Yes 20 11 5 1
cell-heap No Yes 19 0 0 1
elem No Yes 22 0 0 1
gref No Yes 26 0 0 0
heap No Yes 89 22 12 1
heap-sep No Yes 91 16 16 0
linked-list No Yes 27 2 1 0
linked-list-seg No Yes 49 5 3 0
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
list-prefixn No Yes 31 3 3 0
maplet No Yes 40 6 6 0
nat No Yes 31 5 3 0
nat-basic No Yes 42 12 3 1
nat-mult No Yes 23 2 1 0
obj No Yes 22 0 0 1
ops No Yes 33 7 0 0
ref No Yes 22 0 1 1
reflist No Yes 42 0 0 1
refobj No Yes 23 0 0 0
refset No Yes 27 0 0 1
separation No Yes 26 2 2 0
set-basic No Yes 42 6 5 1
set-union No Yes 35 5 5 0