Documentation En Ligne

ATELIER B

Guide d'Installation

Ce guide fournit les instructions pour installer l’Atelier B 4.7.1 Community Edition. Il couvre les plateformes Windows, Linux et MacOS.

B, EVENT-B

Manuel de Référence du Langage B

Le Manuel de Référence du Langage B décrit le langage B supporté par l’outil Atelier B version 4.7.1. Il est principalement destiné aux utilisateurs qui réalisent des développements selon la méthode B, mais aussi à tous ceux qui souhaitent découvrir les possibilités du langage B.

Table des Opérateurs et Mots-Clés du Langage B

Cette table contient les opérateurs et mots-clés du langage B, leur représentation ASCII et mathématique, ainsi que leur niveau de priorité.

Contrôleur de types: Manuel des Messages d'Erreur

Ce manuel présente les différents messages d’erreur et d’avertissement du Contrôleur de types. Son but est de préciser l’origine des erreurs pour chaque message afin d’aider l’utilisateur : une fois la cause correctement ciblée, il est plus facile de corriger sa spécification.
Pour des informations complètes et détaillées, il est recommndé de se reporter au Manuel de Référence du Langage B.

PREUVE

Atelier B Open Resources

Ce GitHuB contient:

Un très grand nombre d’obligations de preuve stockées dans des fichiers POG
Une traduction en SMTLib-2.6 de ces obligations de preuve, stockées dans des fichiers SMTLIB-2.6. La traduction a été réalisée avec ppTransSmt.

GÉNÉRATION DE CODE

EXTENSIONS

L’Atelier B est un outil extensible. Il est possible de connecter des outils tiers qui s’interfacent avec les fichiers utilisés et/ou généré par l’Atelier B, au travers de points d’extension. Ces points d’extension permettent d’ajouter des menus à l’interface utilisateur de l’Atelier B. Enfin les formats de fichier utilisés pour stocker les modèles ainsi les obligations de preuve, ainsi que pour interagir avec des prouveurs tiers, sont tous publics et basés sur XML.

Documentation du Schéma BXML

Ce document décrit le format BXML qui est une représentation XML d’un composant B ou Event-B.

Documentation du Schéma PO XML

Ce document décrit et illustre le format POG: une représentation XML des obligations de preuve d’un composant B ou Event-B.

Documentation du Schéma XML Mécanisme de Preuve

Ce schéma définit le format des mécanismes de preuve. Dans l’Atelier B, les mécanismes de preuve sont des descriptions de la manière dont les programmes de preuve automatique (prouveurs) devraient être appliqués aux obligations de preuve.