mergesort_queue.mlw 2.2 KB
Newer Older
Jean-Christophe's avatar
Jean-Christophe committed
1

2 3 4 5
(** {1 Sorting a queue using mergesort}

    Author: Jean-Christophe Filliâtre (CNRS) *)

Jean-Christophe's avatar
Jean-Christophe committed
6 7 8
module MergesortQueue

  use import int.Int
9
  use import list.List
10
  use import list.Mem
Jean-Christophe's avatar
Jean-Christophe committed
11 12 13
  use import list.Length
  use import list.Append
  use import list.Permut
14
  use import queue.Queue
Jean-Christophe's avatar
Jean-Christophe committed
15 16

  type elt
17
  val predicate le elt elt
18
  clone import relations.TotalPreOrder with
19 20 21
    type t = elt, predicate rel = le, axiom .
  clone export list.Sorted with
    type t = elt, predicate le  = le, goal Transitive.Trans
Jean-Christophe's avatar
Jean-Christophe committed
22

23
  let merge (q1: t elt) (q2: t elt) (q: t elt)
24 25 26
    requires { q.elts = Nil /\ sorted q1.elts /\ sorted q2.elts }
    ensures  { sorted q.elts }
    ensures  { permut q.elts (old q1.elts ++ old q2.elts) }
27
  = while length q1 > 0 || length q2 > 0 do
28 29 30
      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 }
Jean-Christophe's avatar
Jean-Christophe committed
31
      invariant { permut (q.elts ++ q1.elts ++ q2.elts)
32
                         (old (q1.elts ++ q2.elts)) }
33
      variant { length q1 + length q2 }
Jean-Christophe's avatar
Jean-Christophe committed
34
      if length q1 = 0 then
35
        push (safe_pop q2) q
Jean-Christophe's avatar
Jean-Christophe committed
36
      else if length q2 = 0 then
37
        push (safe_pop q1) q
Jean-Christophe's avatar
Jean-Christophe committed
38
      else
39 40 41 42 43 44
        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
Jean-Christophe's avatar
Jean-Christophe committed
45 46
    done

47 48 49
  let rec mergesort (q: t elt) : unit
    ensures { sorted q.elts /\ permut q.elts (old q.elts) }
    variant { length q }
50
  = if length q > 1 then begin
Jean-Christophe's avatar
Jean-Christophe committed
51 52 53
      let q1 = create () : t elt in
      let q2 = create () : t elt in
      while not (is_empty q) do
54
        invariant { permut (q1.elts ++ q2.elts ++ q.elts) (old q.elts) }
55 56 57 58 59
        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
Jean-Christophe's avatar
Jean-Christophe committed
60 61
      done;
      assert { q.elts = Nil };
62
      assert { permut (q1.elts ++ q2.elts) (old q.elts) };
Jean-Christophe's avatar
Jean-Christophe committed
63 64 65
      mergesort q1;
      mergesort q2;
      merge q1 q2 q
66 67
    end else
      assert { q.elts = Nil \/ exists x: elt. q.elts = Cons x Nil }
Jean-Christophe's avatar
Jean-Christophe committed
68 69

end