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)Lecture notes (PDF)
Files used during the demos:
- demo_logic.why
- Checking a Large Routine (Turing, 1949)
- John McCarthy's 91 function
- Sorting a Boolean array
- Boyer and Moore's MJRTY algorithm
- Same fringe
- Ring buffer
- Hash tables
- Binary search
Exercises
To perform the exercises, you have to first install Why3 and one or several theorem provers. Relevant instructions are given on Why3's web site. Why3 is launched with the following command: why3ide file.mlwFor each exercise, a file is provided and must be completed. The various questions are given at the beginning of the file.
- Dijkstra's Dutch national flag problem: exo_flag.mlw (solution)
- Ring buffer: exo_buffer.mlw (solution)
- Inorder traversal of a tree: exo_fill.mlw (solution)
