Version – Atelier B 4.0.2

Date de diffusion : janvier 2010
Nouvelles Fonctionnalités / Caractéristiques :

L’Atelier B 4.0.2 a été mis à disposition le 07 Janvier 2011 et peut être téléchargé par les possesseurs d’un contrat de maintenance Atelier B 4. Cette version corrige 84 anomalies et propose 14 améliorations. Parmi celles-ci, on notera :

• Le prouveur interactif affiche désormais les branches de preuve en attente. Il est alors possible de savoir avec précision où l’on en est de la démonstration interactive.
• Génération des obligations de preuve de couverture et d’exclusivité : ces obligations de preuve permettent de démontrer la vivacité (couverture) d’un modèle événementiel, et d’affirmer ou d’infirmer qu’au plus un événement est ouvert dans chaque état d’un modèle événementiel.
• Outil de validation des règles mathématiques ajoutées par l’utilisateur. Cet outil propose une interface unique pour la gestion et la validation des règles mathématiques. Il est par ailleurs possible de saisir des démonstrations manuelles qui seront sauvegardées dans le corps du fichier pmm sous la forme de commentaires. L’outil fournit une vue synthétique par projet et par composant, ainsi que la possibilité de générer un rapport de validation.
• Correcteur orthographique pour les commentaires de l’éditeur de modèles B : les mots mal orthographiés sont identifiés. Un menu contextuel permet de choisir une correction parmi plusieurs possibilités. Les langages pré-installés sont l’Anglais (GB, US) et le Français (France, Belgique, Canada).
• Support pour les nombres littéraux en hexadécimal.
• Les règles mathématiques affichées dans la vue « Theory List » sont maintenant triées en fonction selon leur applicabilité (les gardes qui sont vérifiées sont affichées en gras)
• L’éditeur de modèles B indique désormais si le fichier en cours d’édition a été modifié par ailleurs.
• Ajout d’une fonctionnalité de recherche dans tous les fichiers du projet, de type grep.