Preuve formelle
L’activité de preuve formelle s’inscrit obligatoirement dans l’activité de validation formelle qui consiste à apporter l’assurance de la validité d’un théorème. La validation peut mettre en œuvre différentes techniques, les deux principales sont la preuve formelle et le model checking.
PRÉSENTATION DE LA PREUVE FORMELLE
La “Preuve formelle” consiste à démontrer des théorèmes à l’aide d’un assistant à la preuve. Ces outils permettent, pour certains, d’exécuter automatiquement des parties (voire l’intégralité) d’une preuve, mais surtout valider l’intégralité de la preuve faite par l’utilisateur de manière à ce qu’on ne prouve pas un théorème de manière erronée. Un assistant à la preuve est un outil auquel est associé un langage de description de théorèmes et un langage de description de preuves (qui peut être le même ou pas).
Il existe un certain nombres d’assistants à la preuve qui ont été développés et qui sont utilisés soit dans le monde académique, soit dans l’industrie. Ils peuvent mettre en œuvre des techniques diverses (voir les Méthodes Formelles sur Wikipédia).
La spécificité de la méthode formelle B est que les lemmes qui doivent être prouvés sont produits par un outil (générateur d’obligation de preuve) dans un langage correspondant à la logique du premier ordre associée à la théorie des ensembles.
Les outils de preuve utilisés dans le cadre de la méthode comprennent :
1- Une base de règles d’inférence associée à un moteur contenant des heuristiques
2- Un prouveur de type SAT
DIFFÉRENTES INTERFACES ONT ÉTÉ DÉVELOPPÉES
POUR AIDER À L’ÉCRITURE DES PREUVES :
1- L’atelier B
2- ProB
3-Le prouveur de la plateforme Rodin (update site: https://www.atelierb.eu/update_site/atelierb_provers)
| Plug-in name | Version | Status | MCV | Release Date |
| Atelier-B provers | 2.3.0 | Available | 3.3.0 | 02 Dec 2020 |