[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 specs232336668
lib specs8568562926982
total87987932921050
data-refinementNoNo773714
ordered-setNoNo0000
search-treeNoNo161632954
elemNoYes0000
gelemNoYes0000
grefNoYes0000
heapNoYes5555292132
heap-sepNoYes7878421228
linked-treeNoYes662110
mapletNoYes3636247122
natNoYes12112123971
nat-basic1YesYes6262984
nat-basic2NoYes686818956
nodeYesYes0000
node-heapNoYes0000
objNoYes0000
oelemNoYes88113
opsNoYes00353
osetNoYes11211223577
osetaNoYes2222
refNoYes0000
refobjNoYes0000
refsetNoYes0000
separationNoYes14148647
set-basicNoYes979739486
set-unionNoYes197197656141
treeYesYes0000

Lines et. al. of Specifications

spec-name data? lib? lines axioms operations sorts
all specsNoNo8801448511
all lib specsNoNo7241337911
all nonlib specsNoNo1561160
all data specsNoNo11296386
all nondata specsNoNo82496668
all data lib specsNoNo5648193
all nondata lib specsNoNo66885608
all data nonlib specsNoNo0000
all nondata nonlib specsNoNo1561160
data-refinementNoNo23110
ordered-setNoNo25000
search-treeNoNo1081050
elemNoYes20001
gelemNoYes24000
grefNoYes24000
heapNoYes8622121
heap-sepNoYes8916160
linked-treeNoYes27210
mapletNoYes39660
natNoYes26540
nat-basic1YesYes16931
nat-basic2NoYes25310
nodeYesYes181871
node-heapNoYes19001
objNoYes20001
oelemNoYes25310
opsNoYes31700
osetNoYes39860
osetaNoYes9001
refNoYes20011
refobjNoYes21000
refsetNoYes27001
separationNoYes24220
set-basicNoYes40651
set-unionNoYes33550
treeYesYes222191