[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 specs65651278549
lib specs20282048102762492
total41864226231086082
ShearSortNoNo65651278549
arrayNoYes21219725
array-copyNoYes7575447122
array-listopsNoYes11189
elemNoYes0000
filter-countNoYes242418161
gelemNoYes0000
gelem-min-maxNoYes0000
get-outsideNoYes0000
listNoYes13013046680
list+array-opsNoYes554115
list-as-arrayinstanceNoYes018234108
list-dataYesYes2828700
list-delNoYes3163161823344
list-dupNoYes101101624146
list-getputNoYes995815
list-lastNoYes163163628148
list-permNoYes138138866259
list-setNoYes136136767145
matrixNoYes29292460
matrix+arrayNoYes0000
natNoYes12012032761
nat-basicNoYes12512538639
nat-divNoYes140140527166
nat-evenNoYes505027248
nat-multNoYes212212698199
nat-potNoYes454522096
oarrayNoYes0000
oarray-sortNoYes0232
oelemNoYes88193
oelem-min-maxNoYes4490
olistNoYes6060475130
olist-actNoYes0000
olist-min-maxNoYes2525427137
olist-sortNoYes27279838
rowcol-updNoYes363624996
ShearSort65651278549
array21219725
array-copy7575447122
array-listops11189
elem0000
filter-count242418161
gelem0000
gelem-min-max0000
get-outside0000
list13013046680
list+array-ops554115
list-as-arrayinstance018234108
list-data2828700
list-del3163161823344
list-dup101101624146
list-getput995815
list-last163163628148
list-perm138138866259
list-set136136767145
matrix29292460
matrix+array0000
nat12012032761
nat-basic12512538639
nat-div140140527166
nat-even505027248
nat-mult212212698199
nat-pot454522096
oarray0000
oarray-sort0232
oelem88193
oelem-min-max4490
olist6060475130
olist-act0000
olist-min-max2525427137
olist-sort27279838
rowcol-upd363624996

Lines et. al. of Specifications

spec-name data? lib? lines axioms operations sorts
all specsNoNo1517210797
all lib specsNoNo1287187697
all nonlib specsNoNo23023100
all data specsNoNo482482
all nondata specsNoNo1493198756
all data lib specsNoNo241241
all nondata lib specsNoNo1263175656
all data nonlib specsNoNo0000
all nondata nonlib specsNoNo23023100
ShearSortNoNo23023100
arrayNoYes41521
array-copyNoYes891240
array-listopsNoYes36530
elemNoYes10001
filter-countNoYes55520
gelemNoYes6000
gelem-min-maxNoYes6000
get-outsideNoYes15100
listNoYes45750
list+array-opsNoYes5000
list-as-arrayinstanceNoYes53000
list-dataYesYes241241
list-delNoYes1032250
list-dupNoYes44740
list-getputNoYes35400
list-lastNoYes751450
list-permNoYes39530
list-setNoYes50840
matrixNoYes63931
matrix+arrayNoYes31400
natNoYes25530
nat-basicNoYes281231
nat-divNoYes19200
nat-evenNoYes36640
nat-multNoYes18210
nat-potNoYes36620
oarrayNoYes8001
oarray-sortNoYes62000
oelemNoYes21310
oelem-min-maxNoYes17220
olistNoYes561140
olist-actNoYes8001
olist-min-maxNoYes27400
olist-sortNoYes22210
rowcol-updNoYes791240