Les différents langages B
Cette page recense différents termes qui ont trait à ce que l’on appelle la “méthode formelle 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 Wikipédia.
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 des liens entre les machines, raffinements et implémentations. La description du langage et celle du raffinement et de la preuve associée au langage sont décrits dans le B Book.
LA MÉTHODE B
Ce terme est en général mal compris à cause du terme. 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 ».
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 PROCESS
Ce terme impropre (car le B ne comprend pas de procédure) évoque le langage B défini 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 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 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 faite 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.
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 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 CLASSIQUE
Le terme « B classique » est utilisé pour désigner le langage B décrit dans le B Book et le manuel de référence du langage B.
B# (BSHARP)
Terme désuet, désignant le langage B Rodin, un peu évoqué mais qui n’est plus utilisé à ce jour.
B RODIN
Il s’agit du langage B événementiel défini dans le cadre du projet Rodin.