mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
73 lines
2.4 KiB
Plaintext
73 lines
2.4 KiB
Plaintext
|
|
(** {1 Sorting a queue using mergesort}
|
|
|
|
Author: Jean-Christophe Filliâtre (CNRS) *)
|
|
|
|
module MergesortQueue
|
|
|
|
use int.Int
|
|
use seq.Seq
|
|
use seq.Mem
|
|
use seq.FreeMonoid
|
|
use seq.Occ
|
|
use seq.Permut
|
|
use queue.Queue
|
|
|
|
type elt
|
|
val predicate le elt elt
|
|
clone relations.TotalPreOrder with
|
|
type t = elt, predicate rel = le, axiom .
|
|
clone export seq.Sorted with
|
|
type t = elt, predicate le = le, goal .
|
|
|
|
let merge (q1: t elt) (q2: t elt) (q: t elt)
|
|
requires { q = empty /\ sorted q1 /\ sorted q2 }
|
|
ensures { sorted q }
|
|
ensures { length q = length (old q1) + length (old q2) }
|
|
ensures { forall x. occ_all x q = occ_all x (old q1) + occ_all x (old q2) }
|
|
= while not (is_empty q1 && is_empty q2) do
|
|
invariant { sorted q1 /\ sorted q2 /\ sorted q }
|
|
invariant { forall x y: elt. mem x q -> mem y q1 -> le x y }
|
|
invariant { forall x y: elt. mem x q -> mem y q2 -> le x y }
|
|
invariant { length q + length q1 + length q2 = length (old q1) + length (old q2) }
|
|
invariant { forall x. occ_all x q + occ_all x q1 + occ_all x q2
|
|
= occ_all x (old q1) + occ_all x (old q2) }
|
|
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 /\ permut_all q (old q) }
|
|
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 { forall x. occ_all x q1 + occ_all x q2 + occ_all x q = occ_all x (old q) }
|
|
invariant { length (old q) = length q1 + length q2 + length q }
|
|
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 = empty };
|
|
assert { forall x. occ_all x q1 + occ_all x q2 = occ_all x (old q) };
|
|
mergesort q1;
|
|
mergesort q2;
|
|
merge q1 q2 q
|
|
end else
|
|
assert { q = empty \/ exists x: elt. q = cons x empty }
|
|
|
|
end
|