# Merge sort as in Sedgewick

Fully automatic with Alt-Ergo, Yices, CVC4 et Z3

• some gym between permut and permut_sub
• strange lemmas, should be in why3lib

```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 = (<=)
use map.Occ as O

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

lemma permut_append: forall a1 a2: array int. forall l mid u: int.
l <= mid <= u -> permut a1 a2 l mid -> permut a1 a2 mid u -> permut a1 a2 l u

lemma occ_left_no_add: forall v: int, m: M.map int int, l u: int.
l < u -> M.get m l <> v -> O.occ v m l u = O.occ v m (l+1) u

lemma occ_left_add: forall v: int, m: M.map int int, l u: int.
l < u -> M.get m l = v -> O.occ v m l u = 1 + O.occ v m (l+1) u

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 { permut_sub (old a) a lo hi }
if lo + 1 < hi then
let m = div (lo+hi) 2 in
assert{ lo < m < hi };
'L1: mergesort1 a b lo m;
assert{ permut_sub (at a 'L1) a lo hi };
'L2: mergesort1 a b m hi;
'L3: assert { permut_sub (at a 'L1) a lo hi };
for i = lo to m-1 do
invariant { array_eq_sub b a lo i}
b[i] <- a[i]
done;
for j = m to hi-1 do
invariant { array_eq_sub_rev_offset b a m j (hi - j) }
invariant { array_eq_sub b a lo m }
invariant { forall v: int. O.occ v b.elts m j = O.occ v a.elts (m + hi - j) hi }
b[j] <- a[m + hi - 1 - j]
done;
assert{ permut a b lo m /\ permut a b m hi };
assert{ permut a b lo hi };
assert{ array_eq (at a 'L3) a } ;
'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{ forall v: int. O.occ v a.elts lo k = O.occ v b.elts lo !i + O.occ v b.elts !j hi }
invariant{ array_eq_sub (at a 'L4) a 0 lo /\ array_eq_sub (at a 'L4) a hi (length a) }
assert { !i < !j };
'L: if b[!i] < b[!j - 1] then
begin a[k] <- b[!i]; i := !i + 1 ;
assert{ O.occ b[!i-1] a.elts lo (k+1) = 1 + O.occ b[!i-1] (at a.elts 'L) lo k };
assert{ forall v: int. v <> b[!i-1] -> O.occ v a.elts lo (k+1) = O.occ v (at a.elts 'L) lo k }
end
else
begin j := !j - 1; a[k] <- b[!j] ;
assert{ O.occ b[!j] a.elts lo (k+1) = 1 + O.occ b[!j] (at a.elts 'L) lo k };
assert{ forall v: int. v <> b[!j] -> O.occ v a.elts lo (k+1) = O.occ v (at a.elts 'L) lo k }
end
done;
assert{ i = j };
assert{ permut a b lo hi };
assert{ permut_sub (at a 'L4) a lo hi}

let mergesort (a: array int) =
ensures { permut_all (old a) 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