Vérification déductive de programmes avec Why3

Cours à l'EJCP 2012

Résumé

Ce cours est une introduction à la preuve de programmes en général, et à l'outil Why3 en particulier. L'outil Why3 permet d'écrire des programmes dans un langage très proche d'OCaml (polymorphisme, types algébriques, filtrage, exceptions, références, tableaux, etc.), de leur donner une spécification dans une logique du premier ordre, et de prouver leur correction à l'aide de démonstrateurs interactifs ou automatiques (Coq, Alt-Ergo, Z3, CVC3, etc.). Au travers de nombreux exemples, ce cours introduit des concepts élémentaires de preuve de programmes (pré- et postcondition, invariant de boucle, variant) mais aussi des techniques (spécification, preuve de terminaison, modélisation de structures de données).

Matériel

Les transparents du cours :

• pleine page pour lecture ;
• par huit et sans animation pour impression.

Les notes de cours.

Les fichiers de démonstration utilisés dans les transparents et dans les notes de cours :

• demo_logic.why
• Checking a Large Routine (Turing, 1949)
• La fonction 91 de John McCarthy
• Tri d'un tableau de booléens
• Le problème de la même frange (same fringe)
• Tables de hachage
• Recherche dichotomique dans un tableau trié

Exercices

Pour faire les exercices, il faut installer Why3 et un ou plusieurs démonstrateurs. Les instructions pour cela sont sur le site de Why3. On lance Why3 avec la commande : why3ide fichier.mlw

Pour chaque exercice, un fichier est fourni qu'il s'agit de compléter. Les différentes questions se trouvent au début du fichier.

1. le drapeau hollandais de Dijkstra : exo_flag.mlw (solution)
2. parcours infixe d'un arbre : exo_fill.mlw (solution)

 

---