# Insertion sort -- with swap

Fully automatic with Alt-Ergo

• but needs 'permut' assert in inner loop !!

module InsertionSort

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

let swap (a: array int) (i: int) (j: int) =
requires { 0 <= i < length a /\ 0 <= j < length a }
ensures { exchange (old a) a i j }
let v = a[i] in
a[i] <- a[j];
a[j] <- v

let insertion_sort (a: array int) =
ensures { sorted a /\ permut_all (old a) a }
'L:
for i = 1 to length a - 1 do
invariant { sorted_sub a 0 i /\ permut_all (at a 'L) a }
let j = ref i in
'L1:
while !j > 0 && a[!j - 1] > a[!j] do
invariant { 0 <= !j <= i }
invariant { permut_all (at a 'L) a}
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 -> a[!j] < a[k] }
variant { !j }
swap a (!j-1) !j;
assert { permut_all (at a 'L1) a } ;
j := !j - 1
done
done

end

• Generated by why3doc 0.85