[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 specs831081784740
lib specs21252145107892551
total22082253125733291
BubbleSortNoNo1114852
Bubblesort-colNoNo1414283112
Bubblesort-rowNoNo023605
Bubblesort-row-revNoNo0240
ShearSortNoNo68681289571
matrix-revopsNoNo0000
arrayNoYes21219725
array-copyNoYes7373435113
array-listopsNoYes11189
filter-countNoYes242418161
gen-tord-min-maxNoYes0000
get-outsideNoYes0000
listNoYes13413447981
list-as-arrayinstanceNoYes018236108
list-dataYesYes2828700
list-delNoYes3093091765332
list-dupNoYes101101624146
list-getputNoYes995815
list-lastNoYes164164630148
list-permNoYes139139868260
list-setNoYes136136767144
matrixNoYes29292460
matrix+arrayNoYes22166
natNoYes12012032761
nat-basicNoYes12512538639
nat-divNoYes140140527166
nat-evenNoYes484828351
nat-multNoYes212212698199
nat-potNoYes454522096
oarray-sortNoYes02113
olistNoYes8484614189
olist-min-maxNoYes9595831153
olist-sortNoYes27279838
rowcol-updNoYes4747276105
tordNoYes88193
tord-min-maxNoYes4490

Lines et. al. of Specifications

spec-name data? lib? lines axioms operations sorts
all specsNoNo1703224895
all lib specsNoNo1323199795
all nonlib specsNoNo38025100
all data specsNoNo462482
all nondata specsNoNo1680212854
all data lib specsNoNo231241
all nondata lib specsNoNo1300187754
all data nonlib specsNoNo0000
all nondata nonlib specsNoNo38025100
BubbleSortNoNo40000
Bubblesort-colNoNo58000
Bubblesort-rowNoNo26000
Bubblesort-row-revNoNo19000
ShearSortNoNo20523100
matrix-revopsNoNo32200
arrayNoYes40521
array-copyNoYes951240
array-listopsNoYes36530
filter-countNoYes55520
gen-tord-min-maxNoYes6000
get-outsideNoYes15100
listNoYes581170
list-as-arrayinstanceNoYes55000
list-dataYesYes231241
list-delNoYes1012250
list-dupNoYes44740
list-getputNoYes35400
list-lastNoYes741450
list-permNoYes39530
list-setNoYes50840
matrixNoYes62931
matrix+arrayNoYes31400
natNoYes25530
nat-basicNoYes281231
nat-divNoYes19200
nat-evenNoYes37640
nat-multNoYes18210
nat-potNoYes36620
oarray-sortNoYes72000
olistNoYes571140
olist-min-maxNoYes681280
olist-sortNoYes22210
rowcol-updNoYes791240
tordNoYes22311
tord-min-maxNoYes21220