[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 244 275 3240 1117
lib specs 1564 1564 6046 1554
total 1808 1839 9286 2671
AccessControl No No 2 2 23 14
AccessControl4Vars No No 2 2 15 7
AccessControl4VarsTrans No No 0 0 0 0
AccessControlTrans No No 0 0 0 0
AccessControlWithState No No 0 1 9 4
BSPs No No 5 5 56 23
LanguageBasedNIFIntrans No No 3 8 45 27
LanguageBasedNIFTrans No No 1 6 42 24
MAKS-BSD No No 3 3 46 22
MAKS-BSD-unwinding No No 0 0 0 0
MAKS-BSRA No No 4 4 82 39
MAKS-BSRA-unwinding No No 0 0 0 0
Meyden4VarsIntrans No No 18 27 431 103
Meyden4VarsTrans No No 10 17 157 79
MeydenIntrans No No 30 34 639 141
MeydenIntransWithState No No 21 21 462 78
MeydenTrans No No 11 11 104 51
PurgeIntrans No No 15 15 171 71
PurgeTrans No No 5 5 50 27
PurgeTransNoInitialstate No No 6 6 66 28
event No No 0 0 0 0
eventfuns No No 33 33 193 84
eventfunsHO No No 37 37 247 102
gen-CongIntrans No No 3 3 3 3
gen-CongTrans No No 0 0 0 0
gen-CongTrans-wf No No 0 0 0 0
gen-RMAIntrans No No 14 14 143 66
gen-RMATrans No No 7 7 94 48
gen-command-list No No 0 0 0 0
gen-commands No No 0 0 0 0
gen-execute No No 0 0 0 0
gen-name No No 0 0 0 0
gen-names No No 0 0 0 0
gen-output No No 0 0 0 0
gen-secdomain No No 0 0 0 0
gen-secdomain-set No No 0 0 0 0
gen-sys-out No No 0 0 0 0
gen-systemstate No No 0 0 0 0
gen-value No No 0 0 0 0
state No No 0 0 0 0
trace No No 0 0 0 0
unwinding No No 13 13 160 75
view Yes No 1 1 2 1
xview 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
gelem No Yes 0 0 0 0
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
oelem No Yes 8 8 11 3
pair Yes Yes 0 0 0 0
set-basic No Yes 96 96 390 84
set-union No Yes 186 186 619 124
store No Yes 76 76 371 126
Lines et. al. of Specifications
spec-name data? lib? lines axioms operations sorts
all specs No No 2253 377 248 23
all lib specs No No 498 125 72 8
all nonlib specs No No 1755 252 176 15
all data specs No No 42 52 24 6
all nondata specs No No 2215 342 230 18
all data lib specs No No 21 26 12 3
all nondata lib specs No No 477 99 60 5
all data nonlib specs No No 17 9 6 2
all nondata nonlib specs No No 1738 243 170 13
AccessControl No No 54 7 8 0
AccessControl4Vars No No 103 11 10 0
AccessControl4VarsTrans No No 14 2 0 0
AccessControlTrans No No 9 1 0 0
AccessControlWithState No No 96 14 11 0
BSPs No No 86 6 6 0
LanguageBasedNIFIntrans No No 68 10 3 0
LanguageBasedNIFTrans No No 62 9 2 0
MAKS-BSD No No 16 1 1 0
MAKS-BSD-unwinding No No 30 2 4 0
MAKS-BSRA No No 17 1 1 0
MAKS-BSRA-unwinding No No 50 4 6 0
Meyden4VarsIntrans No No 131 17 5 0
Meyden4VarsTrans No No 85 13 5 0
MeydenIntrans No No 83 12 6 0
MeydenIntransWithState No No 52 8 5 0
MeydenTrans No No 29 6 5 0
PurgeIntrans No No 49 10 7 0
PurgeTrans No No 33 9 7 0
PurgeTransNoInitialstate No No 33 9 7 0
event No No 6 0 0 1
eventfuns No No 56 15 13 0
eventfunsHO No No 82 17 15 0
gen-CongIntrans No No 46 10 3 0
gen-CongTrans No No 37 8 3 0
gen-CongTrans-wf No No 39 7 4 0
gen-RMAIntrans No No 88 15 12 0
gen-RMATrans No No 80 14 10 0
gen-command-list No No 12 0 0 1
gen-commands No No 6 0 0 1
gen-execute No No 12 0 3 0
gen-name No No 6 0 0 1
gen-names No No 7 0 0 1
gen-output No No 6 0 0 1
gen-secdomain No No 9 0 0 1
gen-secdomain-set No No 7 0 0 1
gen-sys-out No No 9 0 0 1
gen-systemstate No No 11 0 1 1
gen-value No No 8 0 1 1
state No No 11 0 1 1
trace No No 16 0 0 1
unwinding No No 84 5 5 0
view Yes No 5 4 3 1
xview Yes No 12 5 3 1
data No Yes 6 0 0 1
elem No Yes 6 0 0 1
elemdata No Yes 2 0 0 0
gelem No Yes 8 0 0 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
oelem No Yes 15 3 1 0
pair Yes Yes 6 5 3 1
set-basic No Yes 39 6 5 1
set-union No Yes 25 5 5 0
store No Yes 63 12 9 2