# Merge sort as in Sedgewick

Semi automatic

• 2 lemmas to be proved in Coq
• see how to improve ?

```module MergeSort

use import int.Int
use import int.EuclideanDivision
use import int.Div2
use import ref.Ref
use import array.Array
use import array.IntArraySorted
use import array.ArrayPermut
use import array.ArrayEq
use map.Map as M
clone map.MapSorted as N with type elt = int, predicate le = (<=)

predicate map_eq_sub_rev_offset (a1 a2: M.map int int) (l u: int) (offset: int) =
forall i: int. l <= i < u -> M.get a1 i = M.get a2 (offset + l + u - 1 - i)

predicate array_eq_sub_rev_offset (a1 a2: array int) (l u: int) (offset: int) =
map_eq_sub_rev_offset a1.elts a2.elts l u offset

predicate map_dsorted_sub (a: M.map int int) (l u: int) =
forall i1 i2 : int. l <= i1 <= i2 < u -> M.get a i2 <= M.get a i1

predicate dsorted_sub (a: array int) (l u: int) =
map_dsorted_sub a.elts l u

predicate map_bitonic_sub (a: M.map int int) (l u: int) =  l < u ->
exists i: int. l <= i <= u /\ N.sorted_sub a l i /\ map_dsorted_sub a i u

predicate bitonic (a: array int) (l u: int) =
map_bitonic_sub a.elts l u

lemma map_bitonic_incr : forall a: M.map int int, l u: int.
map_bitonic_sub a l u -> map_bitonic_sub a (l+1) u

lemma map_bitonic_decr : forall a: M.map int int, l u: int.
map_bitonic_sub a l u -> map_bitonic_sub a l (u-1)

predicate modified_inside (a1 a2: array int) (l u: int) =
(Array.length a1 = Array.length a2) /\
array_eq_sub a1 a2 0 l /\ array_eq_sub a1 a2 u (Array.length a1)

let rec mergesort1 (a b: array int) (lo hi: int) =
requires {Array.length a = Array.length b /\
0 <= lo <= (Array.length a) /\ 0 <= hi <= (Array.length a) }
ensures { sorted_sub a lo hi /\ modified_inside (old a) a lo hi }
if lo + 1 < hi then
let m = div (lo+hi) 2 in
assert{ lo < m < hi};
mergesort1 a b lo m;
'L2: mergesort1 a b m hi;
assert { array_eq_sub (at a 'L2) a lo m};
for i = lo to m-1 do
invariant { array_eq_sub b a lo i}
b[i] <- a[i]
done;
assert{ array_eq_sub a b lo m};
assert{ sorted_sub b lo m};
for j = m to hi-1 do
invariant { array_eq_sub_rev_offset b a m j (hi - j)}
invariant { array_eq_sub a b lo m}
b[j] <- a[m + hi - 1 - j]
done;
assert{ array_eq_sub a b lo m};
assert{ sorted_sub b lo m};
assert{ array_eq_sub_rev_offset b a m hi 0};
assert{ dsorted_sub b m hi};
'L4: let i = ref lo in
let j = ref hi in
for k = lo to hi-1 do
invariant{ lo <= !i < hi /\ lo <= !j <= hi}
invariant{ k = !i + hi - !j}
invariant{ sorted_sub a lo k }
invariant{ forall k1 k2: int. lo <= k1 < k -> !i <= k2 < !j -> a[k1] <= b[k2] }
invariant{ bitonic b !i !j }
invariant{ modified_inside a (at a 'L4) lo hi }
assert { !i < !j };
if b[!i] < b[!j - 1] then
begin a[k] <- b[!i]; i := !i + 1 end
else
begin j := !j - 1; a[k] <- b[!j] end
done

let mergesort (a: array int) =
ensures { sorted a }
let n = Array.length a in
let b = Array.make n 0 in
mergesort1 a b 0 n

end
```

• Generated by why3doc 0.85