Historique des Versions de l'Atelier B

Versions...

• Atelier B 4.0
• Atelier B 4.0 beta
• Atelier B 3.7.2
• Atelier B 3.7.1
• Atelier B 3.7.

Atelier B 4.0

Date de diffusion :février 2009

Nouvelles Fonctionnalités / Caractéristiques :

• Disponibilité de l'outil sous Linux, Solaris, Mac OS X et Windows grâce au développement de l'interface graphique dans l'environnement Qt et au portage des outils du coeur de l'Atelier B.
• Nouvelle interface graphique proposant notamment :
• une vue tout-en-un des projets et de leurs états, une meilleure intégration des messages d'erreur
• l'intégration d'un répartiteur de tâches : les tâches de développement (vérification de type, génération des obligations de preuve, preuve automatique, génération de code) peuvent être réparties sur un parc de serveurs. L'interface permet d'ajouter de supprimer et d'interrompre ces tâches.
• une interface de preuve repensée avec une meilleure gestion de l'arbre de preuve, l'accès simplifié aux commandes de preuve, à l'ajout de règles utilisateurs, à l'analyse syntaxique de formules.
• un éditeur avec navigation et complétion automatique supportant le langage B et le B événementiel
• Intégration de la preuve de bonne définition des modèles : création automatique et intégrée d'un projet de bonne définition associé à un projet principal permettant de valider la bonne définition des modèles.
• Intégration d'outils de preuve de règles ajoutés plus performants
• Ajout d'un outil de raffinement automatique (BART)
• Ajout d'un traducteur d'implémentations B0 vers le langage (ComenC)
• Support du B événementiel avec contrôles syntaxiques et génération d'obligations de preuve spécifiques.
• Ajout d'un moyen d'interfaçage simple et efficace avec des outils externes

Atelier B 4.0 beta

Date de diffusion : septembre 2008

Nouvelles Fonctionnalités / Caractéristiques :

• Mac OS X et Windows supportés (en plus de Linux et Solaris)
• Nouvelle interface graphique proposant:
• l'intégration des fonctionnalités du paralléliseur (application visant a optimiser les temps de traitement des projets B par une utilisation transparente, distante et parallèle de l'Atelier B.)
• une interface de preuve repensée
• un éditeur avec navigation et complétion automatique
• Intégration de la preuve de bonne définition des modèles
• Ajout d'un outil de raffinement automatique (BART)

Atelier B 3.7.2

Date de diffusion : mai 2008

Nouvelles Fonctionnalités / Caractéristiques :

La future version 3.7.2 est actuellement en développement et a été annoncée pour mai 2008. Elle inclue le traducteur ComenC. Il s'agit d'un nouveau traducteur pour le langage B qui permet de traduire des implémentations B0 vers le langage C.

Atelier B 3.7.1

Date de diffusion : 07/03/2008

Nouvelles Fonctionnalités / Caractéristiques :

La version 3.7.1 corrige certaines anomalies présentes dans la version 3.7.Les corrections apportées sont les suivantes :

• Interface graphique: lors de la sortie de l'interface de preuve, la boite de dialogue demandant si la démonstration devait être sauvée bloquait l'interface.
• Interface EMACSPRI: des problèmes de compatibilité avec la version 3.7 ont été corrigés.
• Prouveur: la commande "search rule" recherche maintenant correctement les règles dans les fichiers .pmm.
• Type checker: Lors du collage de constante abstraites par homonymie, le type-checker levait une erreur, alors que cette construction est autorisée par le langage B.
• Mode trace de règles utilisateur: dans certains cas, l'utilisation du mode trace de règles utilisateur pouvait faire boucler le prouveur
• La machine BASIC_IO du projet LIBRARY ne permettait pas la génération de code.

Atelier B 3.7

Date de diffusion : 18/07/2007

Nouvelles Fonctionnalités / Caractéristiques :

L’Atelier B 3.7 apporte de nombreuses améliorations aux fonctionnalités majeures de l'Atelier B afin de faciliter le travail du développeur :

• interface utilisateur : non limitation des noms de projet, amélioration de la commande make, meilleur archivage des projets, modification du bandeau, rafraichissement de la liste des projets et des composants, état des composants non prouvés, état de composant non prouvé et de projet incomplet, ajout/suppression de composants, filtre sur la liste des projets, gestion des fichiers pmm, archivage des fichiers spécifiques, ressources graphiques par utilisateur.
• preuve : paramétrage d’un temps de coupure des outils de preuve, ajout de nouvelles commandes et alias, mécanismes du moniteur de preuve plus efficaces, concaténation des théories User_Pass, mode trace pour l'application des règles de l’utilisateur, facilitation de la réutilisation de démonstrations, générateur d’obligations de preuve optimisé.
• système : passage de la base de données des projets en mode texte (format xml), modification du système de licence, amélioration de la gestion des dépendances, gestion des bibliothèques du projet en local.