[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 66 66 1307 294
lib specs 1013 1013 3534 925
total 1079 1079 4841 1219
bin-min-heap Yes No 0 0 0 0
bin-min-heap-inv No No 47 47 606 132
bin-min-heap-ops No No 0 0 0 0
bin-min-heap-prepost No No 14 14 659 154
binheap-key No No 0 0 0 0
elem-index Yes No 0 0 0 0
index-array No No 5 5 42 8
index-array-base No No 0 0 0 0
key-index Yes No 0 0 0 0
key-index-array No No 0 0 0 0
keyindex-set No No 0 0 0 0
array No Yes 14 14 46 11
array-copy No Yes 53 53 277 85
elem No Yes 0 0 0 0
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
nat-pot No Yes 44 44 185 89
oelem No Yes 8 8 18 3
set-basic No Yes 96 96 444 86
set-union No Yes 197 197 770 140
Lines et. al. of Specifications
spec-name data? lib? lines axioms operations sorts
all specs No No 872 105 52 10
all lib specs No No 438 60 26 4
all nonlib specs No No 434 45 26 6
all data specs No No 0 0 0 0
all nondata specs No No 821 72 37 7
all data lib specs No No 0 0 0 0
all nondata lib specs No No 438 60 26 4
all data nonlib specs No No 51 33 15 3
all nondata nonlib specs No No 383 12 11 3
bin-min-heap Yes No 15 11 5 1
bin-min-heap-inv No No 60 7 6 0
bin-min-heap-ops No No 146 0 0 0
bin-min-heap-prepost No No 74 4 4 0
binheap-key No No 11 0 0 0
elem-index Yes No 18 11 5 1
index-array No No 26 1 1 0
index-array-base No No 18 0 0 1
key-index Yes No 18 11 5 1
key-index-array No No 32 0 0 1
keyindex-set No No 16 0 0 1
array No Yes 48 5 2 1
array-copy No Yes 100 14 4 0
elem No Yes 22 0 0 1
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
nat-pot No Yes 36 6 2 0
oelem No Yes 27 3 1 0
set-basic No Yes 42 6 5 1
set-union No Yes 35 5 5 0