ACCUEIL

Consignes aux
auteurs et coordonnateurs
Nos règles d'éthique
Auteurs : soumettez
votre article en ligne
Autres revues >>

Technique et Science Informatiques

0752-4072
Revue des sciences et technologies de l'information
 

 ARTICLE VOL 22/1 - 2003  - pp.61-88  - doi:10.3166/tsi.22.61-88
TITRE
Spécifications et développements structurés dans la méthode B

RÉSUMÉ
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.

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

AUTEUR(S)
Marie-Laure POTET

Reçu le 30 novembre 2001.    Accepté le 15 juillet 2002.

MOTS-CLÉS
Méthode B, modularité, compositionnalité des preuves

KEYWORDS
B-method, modularity, proof composionality

LANGUE DE L'ARTICLE
Français

 PRIX
• Abonné (hors accès direct) : 12.5 €
• Non abonné : 25.0 €
|
|
--> Tous les articles sont dans un format PDF protégé par tatouage 
   
ACCÉDER A L'ARTICLE COMPLET  (310 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

CONTACTS
Comité de
rédaction
Conditions
générales de vente

 English version >> 
Lavoisier