skew_heaps.mlw 3.71 KB
Newer Older
1 2 3 4

module SkewHeaps

  use import bintree.Tree
5 6
  use export bintree.Size
  use export bintree.Occ
7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24

  type elt

  predicate le elt elt
  clone relations.TotalPreOrder with type t = elt, predicate rel = le

  (* [e] is no greater than the root of [t], if any *)
  predicate le_root (e: elt) (t: tree elt) = match t with
    | Empty      -> true
    | Node _ x _ -> le e x
  end

  (* [t] is a heap *)
  predicate heap (t: tree elt) = match t with
    | Empty      -> true
    | Node l x r -> le_root x l && heap l && le_root x r && heap r
  end

25 26 27
  function minimum (tree elt) : elt
  axiom minimum_def: forall l x r. minimum (Node l x r) = x

28 29 30 31
  predicate is_minimum (x: elt) (t: tree elt) =
    mem x t && forall e. mem e t -> le x e

  (* the root is the smallest element *)
32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56
  let rec lemma root_is_min (t: tree elt) : unit
     requires { heap t && 0 < size t }
     ensures  { is_minimum (minimum t) t }
     variant  { size t }
  = match t with
    | Empty -> absurd
    | Node l _ r ->
        if l <> Empty then root_is_min l;
        if r <> Empty then root_is_min r
    end

  let empty () : tree elt
    ensures { heap result }
    ensures { size result = 0 }
    ensures { forall e. not (mem e result) }
  =
    Empty

  let is_empty (t: tree elt) : bool
    ensures { result <-> size t = 0 }
  =
    t = Empty

  let size (t: tree elt) : int
    ensures { result = size t }
57
  =
58
    size t
59 60

  let get_min (t: tree elt) : elt
61 62
    requires { heap t && 0 < size t }
    ensures  { result = minimum t }
63 64 65 66 67 68 69 70 71 72
  =
    match t with
      | Empty      -> absurd
      | Node _ x _ -> x
    end

  let rec merge (t1 t2: tree elt) : tree elt
    requires { heap t1 && heap t2 }
    ensures  { heap result }
    ensures  { forall e. occ e result = occ e t1 + occ e t2 }
73
    ensures  { size result = size t1 + size t2 }
74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89
    variant  { size t1 + size t2 }
  =
    match t1, t2 with
    | Empty, _ -> t2
    | _, Empty -> t1
    | Node l1 x1 r1, Node l2 x2 r2 ->
       if le x1 x2 then
         Node (merge r1 t2) x1 l1
       else
         Node (merge r2 t1) x2 l2
    end

  let add (x: elt) (t: tree elt) : tree elt
    requires { heap t }
    ensures  { heap result }
    ensures  { occ x result = occ x t + 1 }
90 91
    ensures  { forall e. e <> x -> occ e result = occ e t }
    ensures  { size result = size t + 1 }
92 93 94
  =
    merge (Node Empty x Empty) t

95 96
  let remove_min (t: tree elt) : tree elt
    requires { heap t && 0 < size t }
97
    ensures  { heap result }
98 99 100
    ensures  { occ (minimum t) result = occ (minimum t) t - 1 }
    ensures  { forall e. e <> minimum t -> occ e result = occ e t }
    ensures  { size result = size t - 1 }
101 102 103 104 105 106 107
  =
    match t with
      | Empty      -> absurd
      | Node l _ r -> merge l r
    end

end
108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146

(* application *)

module HeapSort

  use import SkewHeaps
  use import int.Int
  use import ref.Ref
  use import array.Array
  use import array.ArrayPermut
  clone export array.Sorted with type elt = elt, predicate le = le
  use import map.Occ as M
  use import bintree.Occ as H

  let heapsort (a: array elt) : unit
    ensures { sorted a }
    ensures { permut_all (old a) a }
  =
    let n = length a in
    let t = ref (empty ()) in
    for i = 0 to n - 1 do
      invariant { heap !t && size !t = i }
      invariant { forall e.
                  M.occ e a.elts i n + H.occ e !t = M.occ e a.elts 0 n }
      t := add a[i] !t;
      assert { M.occ a[i] a.elts i n = 1 + M.occ a[i] a.elts (i+1) n }
    done;
    'I:
    for i = 0 to n - 1 do
      invariant { sorted_sub a 0 i }
      invariant { heap !t && size !t = n - i }
      invariant { forall j. 0 <= j < i -> forall e. mem e !t -> le a[j] e }
      invariant { forall e.
                  M.occ e a.elts 0 i + H.occ e !t = M.occ e (at a.elts 'I) 0 n }
      a[i] <- get_min !t;
      t := remove_min !t
    done

end