6 Conclusion
La méthode B introduit un langage logique rigoureux pour représenter
les programmes (substitutions généralisées) et les propriétés de ces
programmes. Elle utilise une notion simple de Machine Abstraite
qui est assez voisine de la notion d'objet en programmation mais
qui intègre de plus la notion d'Invariant qui assure la
préservation de propriétés des variables d'état de la machine quelles
que soient les opérations appliquées.
Les gros développements logiciel se construisent en combinant des
machines abstraites élémentaires ou en utilisant la relation de
raffinement entre machines.
Des outils permettent de développer des systèmes en utilisant la
méthode B. Ces outils offrent différentes fonctionnalités :
-
Analyse syntaxique des machines.
- Vérification de la bonne formation des propriétés et programmes
(chaque variable est associée à un univers).
- Génération des obligations de preuve (préservation des
invariants, respect de la sémantique des programmes lors du
raffinement, ...).
- Preuves automatiques ou interactives.
- Animation des machines afin de vérifier la pertinence des
spécifications.
- Génération de code à partir des machines d'implantations.
- Documentation des développements.
Cette méthode a pu être appliquée avec succès dans des applications
industrielles critiques.