## Mergesort (queues)

Sorting queues using mergesort.

Authors: Jean-Christophe Filliâtre

Topics: Sorting Algorithms

Tools: Why3

see also the index (by topic, by tool, by reference, by year)

# Sorting a queue using mergesort

Author: Jean-Christophe FilliĆ¢tre (CNRS)

```module MergesortQueue

use int.Int
use list.List
use list.Mem
use list.Length
use list.Append
use list.Permut
use queue.Queue

type elt
val predicate le elt elt
clone relations.TotalPreOrder with
type t = elt, predicate rel = le, axiom .
clone export list.Sorted with
type t = elt, predicate le  = le, goal Transitive.Trans

let merge (q1: t elt) (q2: t elt) (q: t elt)
requires { q.elts = Nil /\ sorted q1.elts /\ sorted q2.elts }
ensures  { sorted q.elts }
ensures  { permut q.elts (old q1.elts ++ old q2.elts) }
= while length q1 > 0 || length q2 > 0 do
invariant { sorted q1.elts /\ sorted q2.elts /\ sorted q.elts }
invariant { forall x y: elt. mem x q.elts -> mem y q1.elts -> le x y }
invariant { forall x y: elt. mem x q.elts -> mem y q2.elts -> le x y }
invariant { permut (q.elts ++ q1.elts ++ q2.elts)
(old (q1.elts ++ q2.elts)) }
variant { length q1 + length q2 }
if length q1 = 0 then
push (safe_pop q2) q
else if length q2 = 0 then
push (safe_pop q1) q
else
let x1 = safe_peek q1 in
let x2 = safe_peek q2 in
if le x1 x2 then
push (safe_pop q1) q
else
push (safe_pop q2) q
done

let rec mergesort (q: t elt) : unit
ensures { sorted q.elts /\ permut q.elts (old q.elts) }
variant { length q }
= if length q > 1 then begin
let q1 = create () : t elt in
let q2 = create () : t elt in
while not (is_empty q) do
invariant { permut (q1.elts ++ q2.elts ++ q.elts) (old q.elts) }
invariant { length q1 = length q2 \/
length q = 0 /\ length q1 = length q2 +1 }
variant   { length q }
let x = safe_pop q in push x q1;
if not (is_empty q) then let x = safe_pop q in push x q2
done;
assert { q.elts = Nil };
assert { permut (q1.elts ++ q2.elts) (old q.elts) };
mergesort q1;
mergesort q2;
merge q1 q2 q
end else
assert { q.elts = Nil \/ exists x: elt. q.elts = Cons x Nil }

end
```