# Insertion sort is stable

• fully automatic
• but why3 0.82 cannot prove invariant 'stable a' in inner loop. Need twice inlined manually!!

```module InsertionSortStable

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

type eltpair 'a 'b = {v: 'a; attr: 'b}

predicate sorted_sub (a : array (eltpair int int)) (l u: int) =
forall i1 i2 : int.
l <= i1 <= i2 < u -> a[i1].v <= a[i2].v

predicate sorted (a : array (eltpair int int)) = sorted_sub a 0 (length a)

predicate stable_sub (a : array (eltpair int int)) (l u: int) =
forall i1 i2 : int.
l <= i1 <= i2 < u -> a[i1].v = a[i2].v -> a[i1].attr <= a[i2].attr

predicate stable (a : array (eltpair int int)) = stable_sub a 0 (length a)

let swap (a: array (eltpair int 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 insertionSortStable (a: array (eltpair int int)) =
requires { stable a }
ensures { stable a }
'L:
for i = 1 to length a - 1 do
invariant { stable a }
let j = ref i in
while !j > 0 && a[!j - 1].v > a[!j].v do
invariant { 0 <= !j <= i }
(*   invariant { stable a }  *)
invariant {forall i1 i2 : int. 0 <= i1 <= i2 < (length a) -> a[i1].v = a[i2].v -> a[i1].attr <= a[i2].attr }
swap a (!j-1) !j;
j := !j - 1
done
done

end
```

• Generated by why3doc 0.85