mergesort_queue.mlw 1.63 KB
Newer Older
Jean-Christophe's avatar
Jean-Christophe committed
1 2 3 4 5 6 7

module MergesortQueue

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

  type elt
  predicate le elt elt

  axiom total_preorder1:
    forall x y: elt. le x y \/ le y x
  axiom total_preorder2:
    forall x y z: elt. le x y -> le y z -> le x z

  clone import list.Sorted with type t = elt, predicate le = le

20 21 22 23
  let merge (q1: t elt) (q2: t elt) (q: t elt)
    requires { q.elts = Nil (* /\ sorted q1.elts /\ sorted q2.elts *) }
    ensures { permut q.elts (old q1.elts ++ old q2.elts) }
  = 'L:
Jean-Christophe's avatar
Jean-Christophe committed
24 25 26 27 28 29 30 31 32 33 34 35 36 37 38
    while length q1 > 0 || length q2 > 0 do
      invariant { permut (q.elts ++ q1.elts ++ q2.elts)
                         (at q1.elts 'L ++ at q2.elts 'L) }
      variant { length q1.elts + length q2.elts }
      if length q1 = 0 then
        push (pop q2) q
      else if length q2 = 0 then
        push (pop q1) q
      else
        let x1 = peek q1 in
        let x2 = peek q2 in
        if le x1 x2 then push (pop q1) q else push (pop q2) q
    done

(*
39 40 41 42
  let rec mergesort (q: t elt)
    requires { }
    ensures { (* sorted q.elts /\ *) permut q.elts (old q.elts) }
  = 'L:
Jean-Christophe's avatar
Jean-Christophe committed
43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60
    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) }
        variant { length q.elts }
        let x = pop q in push x q1;
        if not (is_empty q) then let x = 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
*)

end