Preuve Formelle
Présentation de la Preuve Formelle
L'activité de preuve
formelle s'inscrit globalement dans l'activité de validation formelle qui
consiste à apporter l'assurance de la validité d'un théorème. La validation
peut mettre en oeuvre différentes techniques, les deux principales sont la
preuve formelle et le model checking.
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 (voir
l'intégralité) d'une preuve mais surtout de valider 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
nombre 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 oeuvre
des technique diverses (voir
Lien Méthodes Formelles).
La spécificité de la
méthode 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 :
-
une base de règles d'inférence associée à une
moteur contenant des heuristiques
-
un prouveur de type SAT
Différentes
interfaces ont été développées pour aider à l'écriture des preuves :
-
-
-
le prouveur de la plateforme Rodin
(lien)
