Date de diffusion : décembre 2012 Nouvelles Fonctionnalités / Caractéristiques :
L’Atelier B 4.1.0 a été mis à disposition de tous le 11 Décembre 2012.
Cette version corrige 385 anomalies (37 pour la version 4.0.1, 79 pour la version 4.0.2 et 269 pour la version 4.1.0) et propose 56 améliorations (5 pour la version 4.0.1, 13 pour la version 4.0.2 et 38 pour la version 4.1.0). Parmi celles-ci, on notera :
Ajout du type de projet « validation de données »
Support amélioré des entiers : choix de la valeur maximale implémentable (MAXINT) sur 16, 32 ou 64 bits, les littéraux entiers ne sont plus limités (BIGINT).
Support des nombres réels
Support expérimental des nombres flottants
Support des nombres littéraux en hexadécimal.
Nouveau générateur de code C, C4B, avec profils de traduction et génération de makefile
Localisation de l’interface graphique en Anglais, Français, Japonais et Portugais.
Support de l’unicode. Les identificateurs, chaines de caractères et commentaires peuvent contenir des caractères non ASCII.
Ajout d’une vue graphique pour le status des composants (points de vue preuve, obligations de preuve).
Exécution de tâches de preuve multiples en parallèle : déclencher la même action de preuve plusieurs fois conduira à l’exécution en parallèles de ces actions. Des informations supplémentaires (ordre d’exécution des actions sont affichées sur la vue graphique).
Amélioration de l’éditeur textuel intégré : Ctrl-D pour supprimer une ligne, meilleure indentation, ajout de la liste des fichiers ouverts récemment, paramètrage de la colorisation syntaxique, navigation dans le modèle (saut vers la définition, vers l’abstraction, vers le rafinement).
Ajout d’une fonctionnalité de recherche dans tous les fichiers du projet, de type grep, autorisant l’emploi d’expression régulière
Outil de preuve de règles : amélioration de la signalisation de l’état de vérification des règles
Affichage des règles rechargées lors de l’utilisation de la commande « pc »
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 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).
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.
