[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 499 507 3823 1645
lib specs 1050 1050 4381 876
total 3098 3114 16408 5042
aux No No 0 0 0 0
calculus No No 7 7 56 24
cell Yes No 1 1 2 1
cell-heap No No 0 0 0 0
cell-heap-aux No No 3 3 47 16
embed-aux No No 36 36 584 296
existential No No 2 2 24 11
gaux No No 0 0 0 0
gobj No No 0 0 0 0
gownership Yes No 0 0 0 0
gref No No 0 0 0 0
heap No No 74 74 428 164
heap-aux No No 99 99 314 67
heap-aux-inst No No 0 0 0 0
heap-fun No No 35 35 175 70
heap-mod No No 6 6 218 136
heap-sep No No 83 83 541 247
iter-n No No 9 9 72 30
iter-set No No 7 7 75 33
iter-store No No 8 8 70 34
linked-list No No 7 7 69 33
linked-list-aux No No 15 15 162 73
linked-list-seg No No 15 15 125 42
linked-tree No No 6 6 27 10
maplet No No 36 36 252 104
node Yes No 0 0 0 0
node-heap No No 0 0 0 0
obj No No 0 0 0 0
obj-aux Yes No 0 0 0 0
ops No No 0 0 0 0
ops-impl No No 0 0 0 0
ops-inst No No 0 8 39 6
ownership No No 0 0 0 0
reachable No No 0 0 0 0
ref No No 0 0 0 0
reflist No No 0 0 0 0
refobj No No 0 0 0 0
refset No No 0 0 0 0
rg No No 15 15 156 53
rtc-heap No No 0 0 0 0
rtc-ref No No 0 0 0 0
separation No No 15 15 102 46
separation-rg No No 20 20 285 149
tree Yes No 0 0 0 0
data No Yes 0 0 0 0
elem No Yes 0 0 0 0
elemdata No Yes 0 0 0 0
list No Yes 130 130 466 80
list-data Yes Yes 28 28 70 0
list-dup No Yes 101 101 624 146
list-last No Yes 163 163 628 148
nat No Yes 120 120 327 61
nat-basic No Yes 125 125 386 39
rtc No Yes 5 5 44 18
set-basic No Yes 99 99 486 91
set-union No Yes 201 201 893 153
store No Yes 78 78 457 140
aux 0 0 0 0
calculus 7 7 56 24
cell 1 1 2 1
cell-heap 0 0 0 0
cell-heap-aux 3 3 47 16
embed-aux 36 36 584 296
existential 2 2 24 11
gaux 0 0 0 0
gobj 0 0 0 0
gownership 0 0 0 0
gref 0 0 0 0
heap 74 74 428 164
heap-aux 99 99 314 67
heap-aux-inst 0 0 0 0
heap-fun 35 35 175 70
heap-mod 6 6 218 136
heap-sep 83 83 541 247
iter-n 9 9 72 30
iter-set 7 7 75 33
iter-store 8 8 70 34
linked-list 7 7 69 33
linked-list-aux 15 15 162 73
linked-list-seg 15 15 125 42
linked-tree 6 6 27 10
maplet 36 36 252 104
node 0 0 0 0
node-heap 0 0 0 0
obj 0 0 0 0
obj-aux 0 0 0 0
ops 0 0 0 0
ops-impl 0 0 0 0
ops-inst 0 8 39 6
ownership 0 0 0 0
reachable 0 0 0 0
ref 0 0 0 0
reflist 0 0 0 0
refobj 0 0 0 0
refset 0 0 0 0
rg 15 15 156 53
rtc-heap 0 0 0 0
rtc-ref 0 0 0 0
separation 15 15 102 46
separation-rg 20 20 285 149
tree 0 0 0 0
data 0 0 0 0
elem 0 0 0 0
elemdata 0 0 0 0
list 130 130 466 80
list-data 28 28 70 0
list-dup 101 101 624 146
list-last 163 163 628 148
nat 120 120 327 61
nat-basic 125 125 386 39
rtc 5 5 44 18
set-basic 99 99 486 91
set-union 201 201 893 153
store 78 78 457 140
Lines et. al. of Specifications
spec-name data? lib? lines axioms operations sorts
all specs No No 1469 245 136 21
all lib specs No No 315 82 42 6
all nonlib specs No No 1154 163 94 15
all data specs No No 46 24 8 2
all nondata specs No No 1363 173 111 15
all data lib specs No No 23 12 4 1
all nondata lib specs No No 292 70 38 5
all data nonlib specs No No 83 60 21 5
all nondata nonlib specs No No 1071 103 73 10
aux No No 7 0 0 1
calculus No No 7 0 0 0
cell Yes No 18 11 5 1
cell-heap No No 15 0 0 1
cell-heap-aux No No 24 0 0 1
embed-aux No No 22 1 1 0
existential No No 18 1 1 0
gaux No No 9 0 0 0
gobj No No 9 0 0 0
gownership Yes No 14 5 3 1
gref No No 9 0 0 0
heap No No 77 23 13 1
heap-aux No No 215 7 7 0
heap-aux-inst No No 50 0 0 0
heap-fun No No 24 3 2 0
heap-mod No No 28 4 4 0
heap-sep No No 65 16 16 0
iter-n No No 16 2 1 0
iter-set No No 23 4 2 0
iter-store No No 28 4 2 0
linked-list No No 20 2 1 0
linked-list-aux No No 31 4 3 0
linked-list-seg No No 40 5 3 0
linked-tree No No 19 2 1 0
maplet No No 32 6 6 0
node Yes No 17 18 7 1
node-heap No No 15 0 0 1
obj No No 5 0 0 1
obj-aux Yes No 12 5 3 1
ops No No 26 8 0 0
ops-impl No No 35 2 0 0
ops-inst No No 9 0 0 0
ownership No No 8 0 0 1
reachable No No 13 1 1 0
ref No No 6 0 1 1
reflist No No 33 0 0 1
refobj No No 6 0 0 0
refset No No 20 0 0 1
rg No No 32 3 3 0
rtc-heap No No 14 0 0 0
rtc-ref No No 14 0 0 0
separation No No 18 2 2 0
separation-rg No No 29 3 3 0
tree Yes No 22 21 3 1
data No Yes 5 0 0 1
elem No Yes 7 0 0 1
elemdata No Yes 6 0 0 0
list No Yes 32 7 5 0
list-data Yes Yes 23 12 4 1
list-dup No Yes 32 7 4 0
list-last No Yes 53 14 5 0
nat No Yes 16 5 3 0
nat-basic No Yes 20 12 3 1
rtc No Yes 17 3 2 0
set-basic No Yes 35 6 5 1
set-union No Yes 22 5 5 0
store No Yes 47 11 6 1