## 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. *)

module InsertionSort

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

let insertion_sort (a: array int)
ensures { sorted a /\ 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 j = ref 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: int.
0 <= k1 <= k2 <= i -> k1 <> !j -> k2 <> !j -> a[k1] <= a[k2] }
invariant { forall k: int. !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: int. 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 ref.Ref
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)
ensures { sorted a /\ 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 j = ref 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: int.
0 <= k1 <= k2 <= i -> k1 <> !j -> k2 <> !j -> le a[k1] a[k2] }
invariant { forall k: int. !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: int. 0 <= k < !j -> le a[k] v };
a[!j] <- v
done

end
```