Version 4.5 de l’Atelier B

Cette version est une version Free Edition, dont l’accès est libre, elle est donc directement téléchargeable.

Cette version corrige, de manière cumulative  depuis la version 4.2.1, 146 anomalies et améliore les fonctionnalités suivantes :

• Installation simplifiée sous linux
• Génération de PO
  • pour le B événementiel, les obligations de preuve de non-interblocage, non-divergence, faisabilité, exclusivité et couverture sont générées par le nouveau GOP
• Preuve automatique
  • outils d’interfaçage « IAPA » (sous linux uniquement) vers les prouveurs disponibles avec la plateforme Why3 
• Preuve interactive
  • Introduction des Tâcherons de preuve qui, grâce à l’utilisation de prouveurs SMT, permettent de définir des règles de preuve
  • Possibilité d’ajouter ses propres groupes de commande de preuve
  • Amélioration du typage des commandes de preuve
  • Ajout d’un timeout paramétrable aux commandes de preuve de la famille pp
  • Ajout d’une nouvelle commande de preuve at pour Apply Tactic
  • Ajout de fonctionnalités dans l’outil de preuve de règles
  • Intégration du model-checker ProB dans le prouveur interactif
• Support des tableaux indexés par des énumérés pour le générateur de code C4B
• Affichage des obligations de preuve dans l’éditeur
• Vérification des règles de codage au sein de l’Atelier B

Les fonctionnalités ajoutées aux versions 4.4.2 et 4.3 sont décrites dans leurs notes de version respectives (notes de version 4.4.2, notes de version 4.3).

De plus amples informations sont disponibles dans la note de version 4.5