Quelques chiffres

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

Nombre dec composants :

*Machines*	*Raffinements*	*Implémentation*
ctx.mch logiciel.mch materiel.mch reseau.mch portes.mch	portes-1.ref portes-2.ref portes-3.ref portes-4.ref	portes-5.imp
5	4	1

Soit 10 composants.

Nombre de lignes de B

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

Les obligations de preuve

Composants

Preuves triviales *

Obligations de preuve non triviales

Preuves prouvées
automatiquement Preuves prouvées
interactivement

ctx

logiciel

matériel

reseau

portes

portes-1

portes-2

portes-3

portes-4

portes-5

1
89
66
228
30
110
271
314
518
439

2066

0	0
9	0
7	0
15	2
2	1
0	1
15	8
15	24
28	27
21	10

112

Cette étude à été prouvée à 100%.
60% des Obligations de Preuves non triviales ont été démontrées par le prouveur automatique.
Les 40% restantes ont été très facile à démontrer à l'aide du prouveur de prédicats.

* 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.