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 :

Les notes de cours.

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

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)

 


INRIA Saclay - Île-de-France                           CNRS