AbstractThis 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.).
(video: talk at Mathematic Park, in French)
Lecture notes (PDF)
Files used during the demos:
- Checking a Large Routine (Turing, 1949)
- John McCarthy's 91 function
- Boyer and Moore's MJRTY algorithm
- Same fringe
- Ring buffer
- Hash tables
- Binary search
LabTo 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.
- Euclidean division: exo_eucl_div.mlw (solution)
- Factorial: exo_fact.mlw (solution)
- Fast exponentiation: exo_power.mlw (solution)
- Two way sort: exo_two_way.mlw (solution)
- Dijkstra's Dutch national flag: exo_flag.mlw (solution)
- Ring buffer: exo_buffer.mlw (solution)
- Inorder traversal of a tree: exo_fill.mlw (solution)