Spécifications et développements structurés dans la méthode B
Un des points forts de la méthode B est de permettre de composer les spécifications et
leurs développements, ceci dans le cadre opérationnel d’un langage. Le principe adopté est de
pouvoir composer, en même temps, les preuves d’invariants et les preuves de raffinements. Cet
article décrit les formes de structuration permises par la méthode B, les restrictions nécessaires,
et justifie la correction de l’approche. Ces aspects ne sont pas entièrement couverts par le BBook,
en particulier lorsqu’il y a partage de variables.
The possibility to build specifications and development by composition is one of the
main characteristics of the B method. The proof process becomes compositional : invariant and
refinement proofs can be also composed. This article describes which forms of structuration are
allowed, and the necessary restrictions. The correctness of the approach is justified. Some of
these aspects are not covered in the B-Book, in particular when specifications and developments
share variables.
M.POTET
Reçu le 30 novembre 2001.
Accepté le 15 juillet 2002.
Méthode B, modularité, compositionnalité des preuves
B-method, modularity, proof composionality
Français
|
