Wiki Agenda Contact Version française

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 import int.Int
  use import list.List
  use import list.Mem
  use import list.Length
  use import list.Append
  use import list.Permut
  use import queue.Queue

  type elt
  predicate le elt elt
  clone relations.TotalPreOrder with type t = elt, predicate rel = le
  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) }
  = 'L:
    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)
                         (at q1.elts 'L ++ at q2.elts 'L) }
      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 }
  = 'L:
    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) (at q.elts 'L) }
        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) (at q.elts 'L) };
      mergesort q1;
      mergesort q2;
      merge q1 q2 q
    end else
      assert { q.elts = Nil \/ exists x: elt. q.elts = Cons x Nil }

end

download ZIP archive