Recitation 17: Verification Examples

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:

isort(l)

(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..