Abstract

This lecture is an introduction to deductive program verification and to the tool
Why3. This tool provides an imperative programming language (with polymorphism, algebraic data types, pattern matching, exceptions, references, arrays, etc.), a specification language that is an extension of first-order logic, and a technology to verify programs using interactive and automated theorem provers (Coq, Alt-Ergo, Z3, CVC3, etc.). Through many examples, this lecture introduces elementary concepts of program verification (pre- and postconditions, loop invariants, variants, ghost code, etc.) as well as techniques (specification, termination proofs, modeling of data structures, etc.).

Material

Slides (PDF)

(video: talk at Mathematic Park, in French)

Lecture notes (PDF)

Files used during the demos:

Lab

To perform the exercises, you have to first install Why3 (version 0.85) and one or several theorem provers (at least Alt-Ergo version 0.95.2). Installation instructions are given on
this page.

Why3 is launched with the following command: why3 ide file.mlw For each exercise, a file is provided and must be completed. The various questions are given at the beginning of the file.

  1. Euclidean division: exo_eucl_div.mlw (solution)
  2. Factorial: exo_fact.mlw (solution)
  3. Fast exponentiation: exo_power.mlw (solution)
  4. Two way sort: exo_two_way.mlw (solution)
  5. Dijkstra's Dutch national flag: exo_flag.mlw (solution)
  6. Ring buffer: exo_buffer.mlw (solution)
  7. Inorder traversal of a tree: exo_fill.mlw (solution)

 


INRIA Saclay - Île-de-France                           CNRS