[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 0 7 73 37
lib specs 2461 2465 8914 2570
total 2461 2472 8987 2607
ASM No No 0 0 0 0
ASMAUX No No 0 0 0 0
Agent Yes No 0 0 0 0
Agentlist No No 0 0 0 0
Agents No No 0 0 0 0
Instance No No 0 0 0 0
Properties No No 0 7 73 37
Step No No 0 0 0 0
action Yes No 0 0 0 0
command Yes No 0 0 0 0
data Yes No 0 0 0 0
datafuns No No 0 0 0 0
domain Yes No 0 0 0 0
domains No No 0 0 0 0
domdefinitions No No 0 0 0 0
dominterference No No 0 0 0 0
eqd No No 0 0 0 0
exAgent No No 0 0 0 0
localMethods No No 0 0 0 0
name Yes No 0 0 0 0
namefuns No No 0 0 0 0
observeAlter No No 0 0 0 0
okaction No No 0 0 0 0
state No No 0 0 0 0
userMethods No No 0 0 0 0
AccessControl No Yes 2 2 23 14
MeydenIntrans No Yes 30 34 639 141
bool Yes Yes 0 0 0 0
char No Yes 0 0 0 0
elem No Yes 0 0 0 0
gen-command-list No Yes 0 0 0 0
gen-commands No Yes 0 0 0 0
gen-name No Yes 0 0 0 0
gen-secdomain No Yes 0 0 0 0
gen-secdomain-set No Yes 0 0 0 0
gen-systemstate No Yes 0 0 0 0
gen-value No Yes 0 0 0 0
int-abs No Yes 276 276 520 117
int-basic1 No Yes 51 51 121 42
int-basic2 No Yes 55 55 181 51
int-mult No Yes 295 295 1030 476
list No Yes 130 130 352 86
list-data Yes Yes 30 30 46 0
list-del No Yes 297 297 1357 306
list-dup No Yes 103 103 564 166
list-last No Yes 156 156 398 120
list-perm No Yes 105 105 818 271
list-set No Yes 128 128 596 137
nat No Yes 121 121 239 71
nat-basic1 Yes Yes 62 62 98 4
nat-basic2 No Yes 66 66 187 56
nat-mult No Yes 214 214 570 240
set-basic No Yes 96 96 390 84
set-union No Yes 186 186 619 124
string-append No Yes 15 15 30 9
string-data Yes Yes 4 4 7 0
string-less No Yes 39 39 129 55
Lines et. al. of Specifications
spec-name data? lib? lines axioms operations sorts
all specs No No 4285 4545 447 36
all lib specs No No 813 172 99 15
all nonlib specs No No 3472 4373 348 21
all data specs No No 56 58 28 8
all nondata specs No No 4010 485 154 14
all data lib specs No No 28 29 14 4
all nondata lib specs No No 785 143 85 11
all data nonlib specs No No 247 4031 279 18
all nondata nonlib specs No No 3225 342 69 3
ASM No No 838 0 0 0
ASMAUX No No 9 0 0 0
Agent Yes No 12 56 11 1
Agentlist No No 16 0 0 1
Agents No No 7 0 0 1
Instance No No 21 0 0 0
Properties No No 200 24 4 0
Step No No 34 4 0 0
action Yes No 8 6 4 1
command Yes No 52 1028 52 1
data Yes No 120 1922 147 13
datafuns No No 219 37 21 0
domain Yes No 12 78 14 1
domains No No 7 0 0 1
domdefinitions No No 464 75 5 0
dominterference No No 59 8 2 0
eqd No No 187 18 6 0
exAgent No No 308 85 12 0
localMethods No No 8 0 4 0
name Yes No 43 941 51 1
namefuns No No 5 0 2 0
observeAlter No No 277 16 3 0
okaction No No 375 52 1 0
state No No 170 21 5 0
userMethods No No 21 2 4 0
AccessControl No Yes 54 7 8 0
MeydenIntrans No Yes 83 12 6 0
bool Yes Yes 5 2 2 1
char No Yes 15 0 0 1
elem No Yes 6 0 0 1
gen-command-list No Yes 12 0 0 1
gen-commands No Yes 6 0 0 1
gen-name No Yes 6 0 0 1
gen-secdomain No Yes 9 0 0 1
gen-secdomain-set No Yes 7 0 0 1
gen-systemstate No Yes 11 0 1 1
gen-value No Yes 8 0 1 1
int-abs No Yes 27 7 6 0
int-basic1 No Yes 29 6 3 1
int-basic2 No Yes 9 3 1 0
int-mult No Yes 15 3 1 0
list No Yes 29 6 5 0
list-data Yes Yes 9 12 6 1
list-del No Yes 110 26 11 0
list-dup No Yes 30 7 4 0
list-last No Yes 54 11 8 0
list-perm No Yes 24 5 3 0
list-set No Yes 38 8 4 0
nat No Yes 15 5 4 0
nat-basic1 Yes Yes 6 9 3 1
nat-basic2 No Yes 13 5 1 0
nat-mult No Yes 8 2 1 0
set-basic No Yes 39 6 5 1
set-union No Yes 25 5 5 0
string-append No Yes 12 3 2 0
string-data Yes Yes 8 6 3 1
string-less No Yes 91 16 5 0