(** {1 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 not (is_empty q1 && is_empty q2) 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 is_empty q1 then push (safe_pop q2) q else if is_empty q2 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 Peano.gt (length q) Peano.one 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