[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 3521 3551 28201 9750
lib specs 531 531 1656 377
total 4052 4082 29857 10127
approx-fixpoint No No 6 6 107 61
array No No 21 21 97 25
array-as-listinstance No No 0 8 45 18
array-copy No No 73 73 435 113
array-listops No No 1 1 18 9
assoclist No No 33 33 199 62
bag-basic No No 7 7 28 6
bag-union No No 46 46 233 74
cube No No 42 42 248 18
cube+array No No 3 3 24 9
either Yes No 0 0 0 0
filter-count No No 44 44 360 90
forall-indexWhere No No 23 23 189 22
gen-ring No No 0 0 0 0
gen-tord No No 0 0 0 0
gen-tord-min-max No No 0 0 0 0
gen-weakord No No 0 0 0 0
get-outside No No 0 0 0 0
inf-app-list No No 5 5 428 213
inf-app-list-old No No 5 5 441 210
infinite-append No No 12 12 772 365
infinite-append-old No No 9 9 689 323
infset-basic No No 67 67 210 11
infset-union No No 179 179 671 46
list No No 139 139 505 85
list-as-arrayinstance No No 0 18 237 108
list-data Yes No 30 30 77 2
list-del No No 315 315 1843 347
list-dup No No 101 101 624 146
list-getput No No 9 9 58 15
list-last No No 161 161 602 137
list-perm No No 150 150 899 274
list-set No No 136 136 767 144
map No No 80 80 461 140
map+set No No 42 42 187 54
map-ops No No 0 0 0 0
matrix No No 30 30 250 2
matrix+array No No 2 2 16 6
matrixops No No 21 21 237 123
mon-lim-filter-count No No 84 84 2166 1076
mon-lim-filter-count-old No No 84 84 2190 1089
monotone-set-fixpoint No No 14 14 127 66
natset No No 6 6 30 15
oarray-sort No No 0 2 10 3
olist No No 86 86 627 193
olist-min-max No No 108 108 875 155
olist-sort No No 27 27 98 38
omap No No 40 40 151 36
option No No 0 0 0 0
oset No No 113 113 366 85
path-reachable No No 67 67 1197 535
putoutside-id No No 0 0 0 0
ring No No 12 12 53 37
rowcol-upd No No 47 47 281 108
rtc No No 5 5 44 19
set-basic No No 101 101 489 90
set-union No No 211 211 856 140
stream No No 248 248 963 373
stream-basic Yes No 4 4 8 0
stream-old No No 222 222 1001 387
streamseq-mon-lim No No 9 9 595 322
streamseq-mon-lim-old No No 3 3 233 131
stut-mon No No 65 65 1544 663
stut-mon-old No No 65 65 1547 665
tord No No 3 3 8 2
tord-min-max No No 4 4 9 0
weakord No No 5 5 10 0
wellfounded No No 14 14 166 77
woarray No No 0 2 10 3
wolist No No 82 82 590 184
Ref No Yes 0 0 0 0
genlincell No Yes 0 0 0 0
lincell No Yes 0 0 0 0
nat No Yes 120 120 327 61
nat-basic No Yes 125 125 386 39
nat-inf No Yes 73 73 243 77
nat-mult No Yes 213 213 700 200
Lines et. al. of Specifications
spec-name data? lib? lines axioms operations sorts
all specs No No 3414 506 222 17
all lib specs No No 151 32 14 4
all nonlib specs No No 3263 474 208 13
all data specs No No 151 32 14 4
all nondata specs No No 3359 474 212 14
all data lib specs No No 0 0 0 0
all nondata lib specs No No 151 32 14 4
all data nonlib specs No No 55 32 10 3
all nondata nonlib specs No No 3208 442 198 10
approx-fixpoint No No 33 4 3 0
array No No 49 7 3 1
array-as-listinstance No No 14 0 0 0
array-copy No No 87 12 4 0
array-listops No No 35 5 3 0
assoclist No No 54 10 3 0
bag-basic No No 31 3 3 1
bag-union No No 56 11 7 0
cube No No 75 12 4 1
cube+array No No 49 6 0 0
either Yes No 15 10 3 1
filter-count No No 65 8 3 0
forall-indexWhere No No 40 7 3 0
gen-ring No No 6 0 0 0
gen-tord No No 6 0 0 0
gen-tord-min-max No No 6 0 0 0
gen-weakord No No 6 0 0 0
get-outside No No 15 1 0 0
inf-app-list No No 19 0 0 0
inf-app-list-old No No 19 0 0 0
infinite-append No No 23 0 0 0
infinite-append-old No No 21 0 0 0
infset-basic No No 47 6 6 1
infset-union No No 35 5 5 0
list No No 58 11 7 0
list-as-arrayinstance No No 59 0 0 0
list-data Yes No 23 12 4 1
list-del No No 103 22 5 0
list-dup No No 44 7 4 0
list-getput No No 35 4 0 0
list-last No No 75 14 5 0
list-perm No No 39 5 3 0
list-set No No 50 8 4 0
map No No 67 11 6 1
map+set No No 47 8 5 0
map-ops No No 30 4 2 0
matrix No No 60 9 3 1
matrix+array No No 31 4 0 0
matrixops No No 107 19 3 0
mon-lim-filter-count No No 72 11 5 0
mon-lim-filter-count-old No No 72 11 5 0
monotone-set-fixpoint No No 43 7 5 0
natset No No 18 1 1 0
oarray-sort No No 74 0 0 0
olist No No 59 11 4 0
olist-min-max No No 64 12 8 0
olist-sort No No 22 2 1 0
omap No No 33 4 1 0
option No No 35 9 4 1
oset No No 47 8 2 0
path-reachable No No 53 9 5 0
putoutside-id No No 20 2 0 0
ring No No 63 9 5 1
rowcol-upd No No 79 12 4 0
rtc No No 26 3 2 0
set-basic No No 47 6 5 1
set-union No No 55 9 8 0
stream No No 124 27 8 0
stream-basic Yes No 17 10 3 1
stream-old No No 121 26 7 0
streamseq-mon-lim No No 39 2 1 0
streamseq-mon-lim-old No No 37 2 1 0
stut-mon No No 81 7 5 0
stut-mon-old No No 81 7 5 0
tord No No 19 1 0 0
tord-min-max No No 21 2 2 0
weakord No No 24 3 1 1
wellfounded No No 61 5 5 0
woarray No No 63 0 0 0
wolist No No 59 11 4 0
Ref No Yes 11 0 1 1
genlincell No Yes 7 0 0 0
lincell No Yes 15 0 1 1
nat No Yes 25 5 3 0
nat-basic No Yes 28 12 3 1
nat-inf No Yes 47 13 5 1
nat-mult No Yes 18 2 1 0