Introduction
AutoProof is an auto-active verifier for the Eiffel programming language; it proves functional correctness of Eiffel programs annotated with contracts. The goal of this tutorial is to show how to verify Eiffel programs with AutoProof through hands-on exercises.
Preparations
The tutorial is available as a PDF document. The exercises can either be done locally on your machine using EVE or using the online version of AutoProof.
To use AutoProof locally you can install the latest EVE build on your machine and download the examples and exercises from this page. Although it is possible to do the verification exercises online, some options are not available on the web.
Note: on Linux, Mono is used to run Boogie. On Ubuntu you can install the package mono-complete.
Material for Download
Material for the Web
- Example: Account
- Exercise: Clock (solution)
- Example: Max in array
- Exercise: Linear Search (solution)
- Exercise: Binary Search (solution)
- Exercise: Recursive Binary Search (solution)
- Exercise: Permutation (solution)
- Exercise: Gnome Sort (solution)
- Exercise: Insertion Sort (solution)
- Example: Binary tree
- Exercise: Ring Buffer (solution)