B, Les Différents Langages

Cette page recense différents termes qui ont trait à ce que l'on appelle la "méthode B".

La méthode B évoluant, certains termes usuels perdent de leur sens d'origine. Nous éprouvons le besoin de compléter certaines définitions déjà données sur Wikipedia.

B - Le langage B - La méthode B - L'Atelier B - B système - B événementiel (Event-B) - B Process - B logiciel - B classique - B Rodin - B# (Bsharp)

B

B évoque, dans le domaine des méthodes formelles, le langage "B", la méthode "B", le livre de référence : le B Book. Son ancêtre est Z, langage de spécification à base de notations mathématiques. B comprend en plus le raffinement et la preuve, deux techniques faisant partie intégrante de B.

Le langage B

Langage faisant référence à la théorie des ensembles et à la logique des prédicats, comprenant également une syntaxe pour décrire des "substitutions", des opérations, et les liens entre les machines, raffinements et implémentations. La description du langage et celle du raffinement et de la preuve associé au langage sont décrits dans le B Book. Voir également http://www.atelierb.eu/ressources/manref1.8.6.fr.zip

La méthode B

Ce terme est en général mal compris à cause du terme méthode. La "méthode B" évoque traditionnellement l'ensemble comprenant : le langage B, le raffinement, la preuve, et les outils associés. Aussi, contrairement aux langages informatiques habituels, B est associé à une démarche constructive qui permet, à partir des spécifications, de les raffiner jusqu'à un niveau semblable à un code. Cette démarche comprend la preuve de cohérence de l'ensemble.

Mais cette démarche n'est pas une méthode au sens où il n'y a pas de mode d'emploi standard à l'application de B.

La méthode B est donc : "une démarche de construction prouvée (dite correcte), sur la base du langage B, du raffinement et de la preuve".

L'atelier B

Outil support de la méthode B, et intégrant la possibilité de traduire des raffinements en un code informatique. Il accepte le langage B tel que décrit dans le B Book.

B système

Ce terme évoque l'utilisation de la méthode B pour spécifier un système, autrement dit spécifier autre chose qu'un logiciel (le logiciel peut évidemment faire partie d'un système).

B événementiel (Event-B)

On parle souvent du langage B événementiel (ou Event-B) pour parler du langage utilisé pour décrire un système à l'aide d'évènements. À ce langage sont associés le raffinement et la preuve. C'est une utilisation de la méthode B. Ce langage a été défini récemment par l'inventeur de la méthode B, Jean-Raymond Abrial. Event-B est d'ailleurs supporté par l'Atelier B et le projet Européen Rodin, deux outils ayant pour but de consolider ce langage et de fournir des outils ouverts capables d'accepter ce langage.

B Process

Ce terme impropre (car le B ne comprend pas de procédure) évoque le langage B définit dans le B Book. En effet des niveaux de raffinements peuvent être traduits en des procédures informatiques. Ce terme a été utilisé avec l'apparition du B évènementiel, pour éviter la confusion avec celui-ci.

B logiciel

Évoque le langage B décrit dans le B book, utilisé pour réaliser des logiciels. Pour une spécification donnée lorsque tous les raffinements ont été réalisés et que la preuve est réalisée, une traduction peut être faire dans le langage informatique de son choix.

On oppose B logiciel et B système. B logiciel pour faire du logiciel, B système pour faire du système.