## Insertion sort (arrays)

Sorting an array of integers using insertion sort.

Authors: Jean-Christophe Filliâtre

Tools: Why3

see also the index (by topic, by tool, by reference, by year)

Insertion sort.

Surprinsingly, the verification of insertion sort is more difficult than the proof of other, more efficient, sorting algorithms.

One reason is that insertion sort proceeds by shifting elements, which means that, within the inner loop, the array is *not* a permutation of the initial array. Below we make use of the functional array update a[j <- v] to state that, if ever we put back `v` at index `j`, we get an array that is a permutation of the original array.

```module InsertionSort

use int.Int
use array.Array
use array.IntArraySorted
use array.ArrayPermut
use array.ArrayEq

let insertion_sort (a: array int) : unit
ensures { sorted a }
ensures { permut_all (old a) a }
= for i = 1 to length a - 1 do
(* a[0..i[ is sorted; now insert a[i] *)
invariant { sorted_sub a 0 i /\ permut_all (old a) a }
let v = a[i] in
let ref j = i in
while j > 0 && a[j - 1] > v do
invariant { 0 <= j <= i }
invariant { permut_all (old a) a[j <- v] }
invariant { forall k1 k2.
0 <= k1 <= k2 <= i -> k1 <> j -> k2 <> j -> a[k1] <= a[k2] }
invariant { forall k. j+1 <= k <= i -> v < a[k] }
variant { j }
label L in
a[j] <- a[j - 1];
assert { exchange (a at L)[j <- v] a[j-1 <- v] (j - 1) j };
j <- j - 1
done;
assert { forall k. 0 <= k < j -> a[k] <= v };
a[j] <- v
done

let test1 () =
let a = make 3 0 in
a[0] <- 7; a[1] <- 3; a[2] <- 1;
insertion_sort a;
a

let test2 () ensures { result.length = 8 } =
let a = make 8 0 in
a[0] <- 53; a[1] <- 91; a[2] <- 17; a[3] <- -5;
a[4] <- 413; a[5] <- 42; a[6] <- 69; a[7] <- 6;
insertion_sort a;
a

exception BenchFailure

let bench () raises { BenchFailure -> true } =
let a = test2 () in
if a[0] <> -5 then raise BenchFailure;
if a[1] <> 6 then raise BenchFailure;
if a[2] <> 17 then raise BenchFailure;
if a[3] <> 42 then raise BenchFailure;
if a[4] <> 53 then raise BenchFailure;
if a[5] <> 69 then raise BenchFailure;
if a[6] <> 91 then raise BenchFailure;
if a[7] <> 413 then raise BenchFailure;
a

end

module InsertionSortGen

use int.Int
use array.Array
use array.ArrayPermut
use array.ArrayEq

type elt

val predicate le elt elt

clone map.MapSorted as M with type elt = elt, predicate le = le

axiom le_refl: forall x:elt. le x x

axiom le_asym: forall x y:elt. not (le x y) -> le y x

axiom le_trans: forall x y z:elt. le x y /\ le y z -> le x z

predicate sorted_sub (a : array elt) (l u : int) =
M.sorted_sub a.elts l u

predicate sorted (a : array elt) =
M.sorted_sub a.elts 0 a.length

let insertion_sort (a: array elt) : unit
ensures { sorted a }
ensures { permut_all (old a) a }
= for i = 1 to length a - 1 do
(* a[0..i[ is sorted; now insert a[i] *)
invariant { sorted_sub a 0 i }
invariant { permut_all (old a) a }
let v = a[i] in
let ref j = i in
while j > 0 && not (le a[j - 1] v) do
invariant { 0 <= j <= i }
invariant { permut_all (old a) a[j <- v] }
invariant { forall k1 k2.
0 <= k1 <= k2 <= i -> k1 <> j -> k2 <> j -> le a[k1] a[k2] }
invariant { forall k. j+1 <= k <= i -> le v a[k] }
variant { j }
label L in
a[j] <- a[j - 1];
assert { exchange (a at L)[j <- v] a[j-1 <- v] (j - 1) j };
j <- j - 1
done;
assert { forall k. 0 <= k < j -> le a[k] v };
a[j] <- v
done

end

```

Using swaps (instead of shifting) is less efficient but at least we can expect the loop invariant for the inner loop to be simpler. And indeed it is.

The invariant below was suggested by Xavier Leroy (Collège de France).

Without surprise, the proof of the permutation property is also simpler.

```module InsertionSortSwaps

use int.Int
use array.Array
use array.ArraySwap
use array.ArrayPermut

let insertion_sort (a: array int) : unit
ensures { forall p q. 0 <= p <= q < length a -> a[p] <= a[q] }
ensures { permut_all (old a) a }
= for i = 1 to length a - 1 do
invariant { forall p q. 0 <= p <= q < i -> a[p] <= a[q] }
invariant { permut_all (old a) a }
let ref j = i in
while j > 0 && a[j - 1] > a[j] do
invariant { 0 <= j <= i }
invariant { permut_all (old a) a }
invariant { forall p q. 0 <= p <= q <= i -> q <> j -> a[p] <= a[q] }
variant   { j }
swap a (j - 1) j;
j <- j - 1
done
done

end
```