[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 16 59 1011 109
lib specs 1437 1462 6054 1623
total 1453 1521 7065 1732
aleb Yes No 1 1 2 1
avolume No No 0 0 0 0
ebm-avol-asm No No 0 21 188 11
ebm-vol-abs No No 5 5 32 10
ebm-vol-asm No No 0 11 171 5
ebm-vol-inv No No 9 9 44 11
ebm-vol-refine No No 1 12 574 71
abstract-volume No Yes 0 0 0 0
abstract-volumes No Yes 0 0 0 0
align No Yes 77 77 377 89
array No Yes 14 14 46 11
array-copy No Yes 53 53 277 85
array-splice No Yes 84 84 752 300
buffer No Yes 2 2 9 5
data No Yes 0 0 0 0
default-volid No Yes 0 0 0 0
ebm-asm No Yes 0 25 356 39
ebm-base No Yes 9 9 88 26
elem No Yes 0 0 0 0
elemdata No Yes 0 0 0 0
eraseblock No Yes 54 54 214 77
error Yes Yes 0 0 0 0
error-class No Yes 19 19 36 9
gelem No Yes 0 0 0 0
leb Yes Yes 0 0 0 0
min-max No Yes 30 30 65 7
nat No Yes 120 120 302 69
nat-basic No Yes 129 129 356 39
nat-div No Yes 139 139 488 165
nat-mult No Yes 213 213 648 238
nat-set No Yes 6 6 36 18
oelem No Yes 8 8 18 3
oset No Yes 111 111 328 76
set-basic No Yes 96 96 444 86
set-union No Yes 197 197 770 140
store No Yes 76 76 444 141
volid No Yes 0 0 0 0
Lines et. al. of Specifications
spec-name data? lib? lines axioms operations sorts
all specs No No 1907 263 89 15
all lib specs No No 1372 246 82 13
all nonlib specs No No 535 17 7 2
all data specs No No 98 278 40 4
all nondata specs No No 1842 114 66 12
all data lib specs No No 49 139 20 2
all nondata lib specs No No 1323 107 62 11
all data nonlib specs No No 16 10 3 1
all nondata nonlib specs No No 519 7 4 1
aleb Yes No 16 10 3 1
avolume No No 40 0 0 1
ebm-avol-asm No No 201 0 0 0
ebm-vol-abs No No 34 5 2 0
ebm-vol-asm No No 173 0 0 0
ebm-vol-inv No No 44 2 2 0
ebm-vol-refine No No 27 0 0 0
abstract-volume No Yes 32 0 0 1
abstract-volumes No Yes 30 0 0 1
align No Yes 30 3 3 0
array No Yes 48 5 2 1
array-copy No Yes 100 14 4 0
array-splice No Yes 68 10 8 0
buffer No Yes 40 0 0 1
data No Yes 23 0 0 1
default-volid No Yes 22 0 1 0
ebm-asm No Yes 267 0 0 0
ebm-base No Yes 63 7 5 0
elem No Yes 22 0 0 1
elemdata No Yes 23 0 0 0
eraseblock No Yes 56 11 10 0
error Yes Yes 32 121 16 1
error-class No Yes 39 1 1 0
gelem No Yes 26 0 0 0
leb Yes Yes 17 18 4 1
min-max No Yes 26 2 2 0
nat No Yes 31 5 3 0
nat-basic No Yes 42 12 3 1
nat-div No Yes 32 2 0 0
nat-mult No Yes 23 2 1 0
nat-set No Yes 34 0 0 1
oelem No Yes 27 3 1 0
oset No Yes 61 8 2 0
set-basic No Yes 42 6 5 1
set-union No Yes 35 5 5 0
store No Yes 58 11 6 1
volid No Yes 23 0 0 1