- Examples from the book:
- LinearSearch.pi, which decides whether an array contains a given integer. Solution for proof of partial correctness. Solution for proof of termination.
- Bubblesort.pi, which sorts an array of integers. Solution for proof of partial correctness. Solution for proof of termination.
- BinarySearch.pi, which decides whether a sorted array contains a given integer faster than LinearSearch.pi can do it. Solution for proof of partial correctness.

- Exercises from the book:
- Abs.pi.
- Acerkmann.pi (for proof of termination).
- InsertionSort.pi, another sorting algorithm.
- MergeSort.pi, a faster and more interesting sorting algorithm. More challenging to prove correct.
- QuickSort.pi, a faster and more interesting sorting algorithm. Much more challenging to prove correct. Partial solution.
- UnsortedUnion.pi, which computes the union of two arrays in the obvious way.
- SortedUnion.pi, which computes the union of two sorted arrays in a fairly obvious way.