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.
Offline Material
Online Material
- Example: Account
- Exercise: Clock
- Example: Max in array
- Exercise: Linear Search
- Exercise: Binary Search
- Exercise: Recursive Binary Search
- Exercise: Permutation
- Exercise: Gnome Sort
- Exercise: Insertion Sort
- Example: Binary tree
- Exercise: Ring Buffer