Quelques chiffres

Dans l'étude de cas effectuée ici, seules les machines abstraites te2, ThreeConst et TabOfTabs ainsi que les raffinements successifs et l'implantation de te2 ont été présentés. Cependant, il existe aussi une autre machine abstraite nommée principal laquelle ne fait qu'importer (dans son implantation) les machines te2 et ThreeConst. De plus, on a aussi un raffinement de TabOfTabs ainsi que les implantations respectives de principal, de ThreeConst et de TabOfTabs.

Nombre dec composants :

*Machines*	*Raffinements*	*Implémentation*
principal.mch te2.mch ThreeConst.mch TabOfTabs.mch	te2-1.ref te2-2.ref te2-31.ref TabOfTabs-11.ref	principal-i.imp te2-i.imp ThreeConst-i.imp TabOfTabs-1-i.imp
4	4	4

Soit 12 composants.

Ces résultats sont obtenus avec la version 3.5 de l'atelier B.

Nombre de lignes de B

Le modèle B compte environ 1580 lignes de B.

Les obligations de preuve

Composants

Preuves triviales *

Obligations de preuve non triviales

principal

te2

ThreeConst

TabOfTabs

te2-1

te2-2

te2-31

TabOfTabs-11

principal-i

te2-i

ThreeConst-i

TabOfTabs-1-i

3
375
5
46
508
344
337
87
6
601
6
66

TOTAL : 2066

0
42
0
16
58
12
21
14
0
271
27
110

TOTAL : 571

Cette étude a été prouvée à 100%.

* Une preuve triviale est une preuve directement démontrées par l'Atelier B. Aucun travail de preuve n'est à réaliser pour de telles obligations de preuve.