examples/mergesort_queue.mlw

   1
   2 (** {1 Sorting a queue using mergesort}
   3
   4     Author: Jean-Christophe Filliâtre (CNRS) *)
   5
   6 module MergesortQueue
   7
   8   use int.Int
   9   use seq.Seq
  10   use seq.Mem
  11   use seq.FreeMonoid
  12   use seq.Occ
  13   use seq.Permut
  14   use queue.Queue
  15
  16   type elt
  17   val predicate le elt elt
  18   clone relations.TotalPreOrder with
  19     type t = elt, predicate rel = le, axiom .
  20   clone export seq.Sorted with
  21     type t = elt, predicate le = le, goal .
  22
  23   let merge (q1: t elt) (q2: t elt) (q: t elt)
  24     requires { q = empty /\ sorted q1 /\ sorted q2 }
  25     ensures  { sorted q }
  26     ensures  { length q = length (old q1) + length (old q2) }
  27     ensures  { forall x. occ_all x q = occ_all x (old q1) + occ_all x (old q2) }
  28   = while not (is_empty q1 && is_empty q2) do
  29       invariant { sorted q1 /\ sorted q2 /\ sorted q }
  30       invariant { forall x y: elt. mem x q -> mem y q1 -> le x y }
  31       invariant { forall x y: elt. mem x q -> mem y q2 -> le x y }
  32       invariant { length q + length q1 + length q2 = length (old q1) + length (old q2) }
  33       invariant { forall x. occ_all x q + occ_all x q1 + occ_all x q2
  34                           = occ_all x (old q1) + occ_all x (old q2) }
  35       variant   { length q1 + length q2 }
  36       if is_empty q1 then
  37         push (safe_pop q2) q
  38       else if is_empty q2 then
  39         push (safe_pop q1) q
  40       else
  41         let x1 = safe_peek q1 in
  42         let x2 = safe_peek q2 in
  43         if le x1 x2 then
  44           push (safe_pop q1) q
  45         else
  46           push (safe_pop q2) q
  47     done
  48
  49   let rec mergesort (q: t elt) : unit
  50     ensures { sorted q /\ permut_all q (old q) }
  51     variant { length q }
  52   = if Peano.gt (length q) Peano.one then begin
  53       let q1 = create () : t elt in
  54       let q2 = create () : t elt in
  55       while not (is_empty q) do
  56         invariant { forall x. occ_all x q1 + occ_all x q2 + occ_all x q = occ_all x (old q) }
  57         invariant { length (old q) = length q1 + length q2 + length q }
  58         invariant { length q1 = length q2 \/
  59                     length q = 0 /\ length q1 = length q2 + 1 }
  60         variant   { length q }
  61         let x = safe_pop q in push x q1;
  62         if not (is_empty q) then let x = safe_pop q in push x q2
  63       done;
  64       assert { q = empty };
  65       assert { forall x. occ_all x q1 + occ_all x q2 = occ_all x (old q) };
  66       mergesort q1;
  67       mergesort q2;
  68       merge q1 q2 q
  69     end else
  70       assert { q = empty \/ exists x: elt. q = cons x empty }
  71
  72 end