Inductive correctness proofs


We will use the term verification to refer to a process that generates high assurance that code works on all inputs and in all environments. Testing is a good, cost-effective way of getting assurance, but it is not a verification process in this sense because there is no guarantee that the coverage of the tests is sufficient for all uses of the code. Verification generates a proof (sometimes only implicitly) that all inputs will result in outputs that conform to the specification. In this lecture, we look at verification based on explicitly but informally proving correctness of the code. Later we'll see a more formal approach to proving correctness.

Verification tends to be expensive and to require thinking carefully about and deeply understanding the code to be verified. In practice, it tends to be applied to code that is important and relatively short. Verification is particularly valuable for critical systems where testing is less effective. Because their execution is not determistic, concurrent programs are hard to test and sometimes subtle bugs can only be found by attempting to verify the code formally. In fact, tools to help prove programs correct have been getting increasingly effective and some large systems have been fully verified, including compilers, processors and processor emulators, and key pieces of operating systems.

Another benefit to studying verification is that when you understand what it takes to prove code correct, it will help you reason about your own code (or others') and to write code that is correct more often, based on specs that are more precise and useful.

In recent years, techniques have been developed that combine ideas from verification and testing have been developed that can sometimes give the best of both worlds. These ideas, model checking and abstract interpretation, can give the same level of assurance as formal verification at lower cost, or more assurance than testing at similar cost. However, in the next couple of lectures, we'll look at verification in the classic sense.

Example : proof of an inductive sort

We want to prove the correctness of the following insertion sort algorithm. The sorting uses a function insert that inserts one element into a sorted list, and a helper function isort' that merges an unsorted list  into a sorted one, by inserting one element at a time into the sorted part. Functions insert and isort' are both recursive.

let rec insert(e, l): int list =
  match l with
     [] -> [e]
  | x::xs -> if e < x then e::l else x::(insert(e,xs))
let rec isort' (l1, l2): int list = match l1 with [] -> l2 | x::xs -> isort'(xs, insert(x, l2))
let isort(l: int list): int list = isort'(l, [])

We will prove that isort works correctly for lists of arbitrary size. The proof consists of three steps: first prove that insert is correct, then  prove that isort' is correct, and finally prove that isort is correct.  Each step relies on the result from the previous step. The first two steps require proofs by induction (because the functions in question are recursive). The last step is straightforward.

Correctness proof for insert

We want to prove that for any element e and any list l: 1) the resulting list  insert(e, l) is sorted; and 2) that the resulting list insert(e,l) contains all of the elements of l, plus element e.

The notion that a list l is sorted, written sorted(l), is defined as usual:  sorted(l) is true if l has at most one element; and sorted(x::xs) holds if x <= e for all elements e being members of xs, and sorted(xs) holds.

The proof is by induction on length of list l. The proof follows the usual format of a proof by induction, i.e., specifying what property we want to prove, what we are inducting on, showing the base case, the inductive step, and clearly specifying when we apply the induction hypothesis (carefully indicating why we can apply it, and showing the lists to which it is applied! ).

Proving correctness of isort'

let isort' (l1: int list, l2:int list) =
  match l1 with
    [] -> l2
  | x::xs -> isort'(xs, insert(x, l2))

We will now prove by induction on the length of l1 that isort' works correctly, following the same proof format.

Proving the correctness of isort

It is now straightforward to prove that isort works correctly. We want to show that for any list l, isort(l) is sorted and
elements(isort(l)) = elements(l).

The evaluation of isort(l) is:


(by substitution)
-> isort'(l, [])

Let l' be the result of evaluating isort'(l, []). From the correctness proof for isort', we know that l' is sorted and elements(l') = elements(l) U elements([]) = elements(l) U Â = elements(l). Hence the final result is sorted and contains all elements of l, Q.E.D..

Modular verification

In our proof that insert met its spec, we assumed that the implementation of > met its spec. This was good because we didn't have to look at the code of >. This was an example of modular verification, in which we were able to verify one small unit of code at a time. Function specifications, abstraction functions, and rep invariants make it possible to verify modules one function at a time, without looking at the code of other functions. If modules have no cyclic dependencies, which OCaml enforces, then the proof of each module can be constructed assuming that every other module satisfies the specs in its interface. The proof of the entire software system is then built from the bottom up.