Le B Workbook est maintenant disponible sur le GitHub de CLEARSY : (https://github.com/CLEARSY/BWORKBOOK).
Après plusieurs mois de travail collaboratif, cette première version (122 pages) peut maintenant être utilisée comme ressource pour la formation aux méthodes formelles et pour l’enseignement de la méthode B.
Nous remercions chaleureusement les contributeurs et relecteurs d’Europe et d’Amérique du Sud qui ont rendu cette version possible.
✅ Le B Workbook propose actuellement 7 exercices de complexité croissante, fournissant une introduction pas à pas à l’Atelier B.
Il couvre les principales phases du développement : spécification formelle, implémentation, preuve, génération de code et compilation de l’exécutable final.
Chaque exercice est accompagné de
- des fichiers de modélisation
- des fichiers de preuve avec des démonstrations automatiques
- code source manuel complémentaire et Makefile pour les environnements Unix (Windows WSL, Linux, MacOS)
- des instructions pour animer les modèles avec ProB.
🔎 Une prochaine itération (prévue pour 2026) élargira le champ d’application avec de nouveaux exercices sur :
- la modélisation Event-B
- l’animation graphique avec VisB
- la génération de code Rust
- les preuves interactives, les tactiques de preuve et l’écriture de règles.
🌍 En attendant, nous acceptons les rapports d’erreurs, les suggestions et les nouvelles idées d’exercices via GitHub.