Validation des règles de base de l'Atelier B

摘要

The B method enables us to build a correct program from an abstract specification expressing the requirements, by refining step by step the abstract specification. Each step must be validated by proof with the help, for example, of the Atelier B proof tool. The Atelier B proof tool uses proof tactics and basic rules. Several years ago, experts proved these rules manually. Our objective is to validate the basic rules in a formal way. This article provides a formalization of a subset of the B language within the Coq system. Then we propose a methodology to validate the basic rules of the Atelier B or more precisely a convenient subset of these rules.%La méthode B permet de construire par raffinement un programme correct à partir d'une spécification abstraite qui exprime les besoins. Chaque étape de raffinement est validée à condition que soient établies certaines propriétés. La preuve de ces propriétés se fait à l'aide d'un outil de preuve, le prouveur de l'Atelier B par exemple. Ce dernier utilise des tactiques de preuve et des règles de base. Notre objectif est de valider les règles de base de l'Atelier B. Ces règles ont été validées manuellement par le passé. Pour plus de confiance, nous avons choisi de les valider formellement, à l'aide du système Coq. L'article propose une formalisation en Coq d'un sous-ensemble du langage B. Nous proposons ensuite une méthode de validation des règles de base de l'Atelier B ou plus exactement d'un sous-ensemble bien choisi de ces règles.