[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 39 39 1728 680
lib specs 1352 1352 4807 1184
total 1391 1391 6535 1864
array-perm No No 6 6 106 18
array_of_nat No No 0 0 0 0
list_of_nat No No 0 0 0 0
map_nat_nat No No 0 0 0 0
partelem Yes No 0 0 0 0
partition No No 0 0 0 0
partition-refinement No No 27 27 1515 656
partition-refinement-test No No 6 6 107 6
set_of_nat No No 0 0 0 0
array No Yes 12 12 25 6
data No Yes 0 0 0 0
elem No Yes 0 0 0 0
elemdata No Yes 0 0 0 0
list No Yes 130 130 352 86
list-data Yes Yes 30 30 46 0
list-del No Yes 309 309 1481 330
list-dup No Yes 104 104 574 167
list-last No Yes 160 160 425 130
nat No Yes 121 121 239 71
nat-basic1 Yes Yes 62 62 98 4
nat-basic2 No Yes 66 66 187 56
set-basic No Yes 96 96 390 84
set-union No Yes 186 186 619 124
store No Yes 76 76 371 126
Lines et. al. of Specifications
spec-name data? lib? lines axioms operations sorts
all specs No No 939 150 92 14
all lib specs No No 457 109 65 8
all nonlib specs No No 482 41 27 6
all data specs No No 84 42 18 4
all nondata specs No No 883 111 76 11
all data lib specs No No 42 21 9 2
all nondata lib specs No No 415 88 56 6
all data nonlib specs No No 14 18 7 1
all nondata nonlib specs No No 468 23 20 5
array-perm No No 27 3 2 0
array_of_nat No No 21 0 0 1
list_of_nat No No 58 0 0 1
map_nat_nat No No 32 0 0 1
partelem Yes No 14 18 7 1
partition No No 58 0 0 1
partition-refinement No No 229 20 18 0
partition-refinement-test No No 18 0 0 0
set_of_nat No No 25 0 0 1
array No Yes 36 5 4 1
data No Yes 19 0 0 1
elem No Yes 18 0 0 1
elemdata No Yes 4 0 0 0
list No Yes 26 6 5 0
list-data Yes Yes 29 12 6 1
list-del No Yes 72 26 11 0
list-dup No Yes 34 7 4 0
list-last No Yes 39 11 8 0
nat No Yes 24 5 4 0
nat-basic1 Yes Yes 13 9 3 1
nat-basic2 No Yes 23 5 1 0
set-basic No Yes 36 6 5 1
set-union No Yes 28 5 5 0
store No Yes 56 12 9 2