|
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
|
|
On parle souvent du langage B événementiel 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. Des outils permettent de passer de ce langage au langage
accepté par l'Atelier B. Le projet Européen Rodin en cours a pour but de
consolider ce langage et de fournir des outils ouverts capables d'accepter ce
langage.
|
| |
|
B procédural
|
|
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.
|
| |
|
B classique
|
|
Comme pour le B procédural, le B classique évoque le B
existant avant le B procédural.
|
| |
|
B Rodin
|
|
Il s'agit du langage B évènementiel définit dans le cadre du projet Rodin.
|
| |
|
B# (Bsharp)
|
|
Terme désuet, désignant le langage B Rodin, un peu évoqué
mais qui n'est plus utilisé à ce jour.
|
