Examples of Correctness Proofs

This module is a very brief review of proofs of correctness of nondeterministic iterations by using invariants and loop variants (also called variant functions).

Invariants

An invariant of a do-od loop is a predicate that holds initially and after every iteration of the loop. We prove that a predicate \(I\) is an invariant of a loop by showing that:

1. \(I\) holds initially, and
2. if \(I\) holds before the execution of any guarded command of the loop then \(I\) continues to hold when the command terminates, i.e., we prove the following Hoare triple for every guarded command \(g \rightarrow c\) of the loop.

   \(\{I\} \; g \rightarrow c \; \{I\}\)

If a loop terminates then \(I\) holds upon termination and all guards evaluate to false.

Variant Functions

We prove that loops terminate by using loop variants, also called variant functions. A variant function is a function from states of a system to a well-founded set. A well-founded set is a set on which we can carry out proofs by induction. In this course we generally use well-founded sets that are integers or vectors of integers that are bounded below.

We prove that execution of a loop terminates by proving that the execution of any command whose guard evaluates to true reduces the value of a variant function \(f\). Since \(f\) is bounded below it cannot decrease forever. Therefore the computation terminates, and when it does all guards evaluate to false.

Let \(I\) be an invariant of a loop. Then \(I \wedge g\) holds prior to execution of any guarded command \(g \rightarrow c\) because guard \(g\) is true. We prove that the execution of any command with a true guard reduces the variant function by proving the following Hoare triple for each guarded command \(g \rightarrow c\).

\(\forall k: \quad \{(f = k) \wedge I \wedge g\} \; c \; \{f < k\} \)

Examples of Correctness Proofs

The remainder of this module consists of self tests of correctness proofs of nondeterministic iterations. The self tests, with solutions, cover the following problems:

1. Sorting
2. Shortest paths in a graph
3. Distributed averaging
4. Formation of objects in flight
5. Earliest meeting time of concurrent agents

The concepts used in proving correctness of sequential algorithms are also used in proving distributed algorithms.

---

K. Mani Chandy, Emeritus Simon Ramo Professor, California Institute of Technology