[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 specs5757418101
lib specs3933931358335
total4504501776436
oarrayNoNo0000
oarray-permNoNo232320160
oarray-sortedNoNo1414588
obagNoNo0000
pair-insertion-sortNoNo4411625
sort-invariantsNoNo1616438
arrayNoYes21217820
array-copyNoYes6767334103
bag-basicNoYes77246
bag-unionNoYes454525398
elemNoYes0000
natNoYes12012029666
nat-basicNoYes12512535539
oelemNoYes88183

Lines et. al. of Specifications

spec-name data? lib? lines axioms operations sorts
all specsNoNo55963316
all lib specsNoNo35854244
all nonlib specsNoNo201972
all data specsNoNo0000
all nondata specsNoNo55963316
all data lib specsNoNo0000
all nondata lib specsNoNo35854244
all data nonlib specsNoNo0000
all nondata nonlib specsNoNo201972
oarrayNoNo9001
oarray-permNoNo28310
oarray-sortedNoNo35220
obagNoNo9001
pair-insertion-sortNoNo66000
sort-invariantsNoNo54440
arrayNoYes48521
array-copyNoYes1031550
bag-basicNoYes36331
bag-unionNoYes491170
elemNoYes22001
natNoYes31530
nat-basicNoYes421231
oelemNoYes27310