skew_heaps.mlw 4.99 KB
Newer Older
1

2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 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
module Heap

  use import int.Int

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

  type t

  function size t : int

  function occ elt t : int

  predicate mem (x: elt) (t: t) = occ x t > 0

  function minimum t : elt

  predicate is_minimum (x: elt) (t: t) =
    mem x t && forall e. mem e t -> le x e

  axiom min_is_min:
    forall t: t. 0 < size t -> is_minimum (minimum t) t

  val empty () : t
    ensures { size result = 0 }
    ensures { forall e. not (mem e result) }

  val size (t: t) : int
    ensures { result = size t }

  val is_empty (t: t) : bool
    ensures { result <-> size t = 0 }

  val get_min (t: t) : elt
    requires { 0 < size t }
    ensures  { result = minimum t }

  val merge (t1 t2: t) : t
    ensures  { forall e. occ e result = occ e t1 + occ e t2 }
    ensures  { size result = size t1 + size t2 }

  val add (x: elt) (t: t) : t
    ensures  { occ x result = occ x t + 1 }
    ensures  { forall e. e <> x -> occ e result = occ e t }
    ensures  { size result = size t + 1 }

  val remove_min (t: t) : t
    requires { 0 < size t }
    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 }

end

57 58 59
module SkewHeaps

  use import bintree.Tree
60 61
  use export bintree.Size
  use export bintree.Occ
62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79

  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

80 81 82
  function minimum (tree elt) : elt
  axiom minimum_def: forall l x r. minimum (Node l x r) = x

83 84 85 86
  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 *)
87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111
  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 }
112
  =
113
    size t
114 115

  let get_min (t: tree elt) : elt
116 117
    requires { heap t && 0 < size t }
    ensures  { result = minimum t }
118 119 120 121 122 123 124 125 126 127
  =
    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 }
128
    ensures  { size result = size t1 + size t2 }
129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144
    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 }
145 146
    ensures  { forall e. e <> x -> occ e result = occ e t }
    ensures  { size result = size t + 1 }
147 148 149
  =
    merge (Node Empty x Empty) t

150 151
  let remove_min (t: tree elt) : tree elt
    requires { heap t && 0 < size t }
152
    ensures  { heap result }
153 154 155
    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 }
156 157 158 159 160 161 162
  =
    match t with
      | Empty      -> absurd
      | Node l _ r -> merge l r
    end

end
163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201

(* 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