leftist_heap.mlw 5.71 KB
Newer Older
1 2 3 4 5 6 7 8 9

(** Leftist heaps (Clark Allan Crane, 1972 && Donald E. Knuth, 1973).

    Purely applicative implementation, following Okasaki's implementation
    in his book "Purely Functional Data Structures" (Section 3.1).

    Author: Mário Pereira (Université Paris Sud)
*)

10 11
module Heap

12
  use int.Int
13 14 15 16

  type elt
  predicate le elt elt

17
  clone relations.TotalPreOrder with
18
    type t = elt, predicate rel = le, axiom .
19 20 21

  type heap

22
  val function size heap : int
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 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71

  function occ elt heap : int

  predicate mem (x: elt) (h: heap) = occ x h > 0

  function minimum heap : elt

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

  axiom min_def:
    forall h. 0 < size h -> is_minimum (minimum h) h

  val empty () : heap
    ensures { size result = 0 }
    ensures { forall x. occ x result = 0 }

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

  val merge (h1 h2: heap) : heap
    ensures { forall x. occ x result = occ x h1 + occ x h2 }
    ensures { size result = size h1 + size h2 }

  val insert (x: elt) (h: heap) : heap
    ensures { occ x result = occ x h + 1 }
    ensures { forall y. y <> x -> occ y h = occ y result }
    ensures { size result = size h + 1 }

  val find_min (h: heap) : elt
    requires { size h > 0 }
    ensures  { result = minimum h }

  val delete_min (h: heap) : heap
    requires { size h > 0 }
    ensures  { let x = minimum h in occ x result = occ x h - 1 }
    ensures  { forall y. y <> minimum h -> occ y result = occ y h }
    ensures  { size result = size h - 1 }

end

module TreeRank

  type tree 'a = E | N int (tree 'a) 'a (tree 'a)

end

module Size

72 73
  use TreeRank
  use int.Int
74

75
  let rec function size (t: tree 'a) : int = match t with
76 77 78 79 80 81 82 83 84 85 86
    | E -> 0
    | N _ l _ r -> 1 + size l + size r
    end

  lemma size_nonneg: forall t: tree 'a. 0 <= size t
  lemma size_empty: forall t: tree 'a. 0 = size t <-> t = E

end

module Occ

87 88
  use TreeRank
  use int.Int
89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105

  function occ (x: 'a) (t: tree 'a) : int = match t with
    | E -> 0
    | N _ l e r -> (if x = e then 1 else 0) + occ x l + occ x r
    end

  lemma occ_nonneg:
    forall x:'a, t. 0 <= occ x t

  predicate mem (x: 'a) (t: tree 'a) =
    0 < occ x t

end

module LeftistHeap

  type elt
106
  val predicate le elt elt
107
  clone relations.TotalPreOrder with
108
    type t = elt, predicate rel = le, axiom .
109

110
  use TreeRank
111 112
  use export Size
  use export Occ
113 114
  use int.Int
  use int.MinMax
115 116 117 118

  type t = tree elt

  (* [e] is no greater than the root of [h], if any *)
Mário Pereira's avatar
Mário Pereira committed
119
  predicate le_root (e: elt) (h: t) = match h with
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
    | E -> true
    | N _ _ x _ -> le e x
    end

  lemma le_root_trans:
    forall x y h. le x y -> le_root y h -> le_root x h

  (* [h] is a heap *)
  predicate is_heap (h: t) = match h with
    | E -> true
    | N _ l x r -> le_root x l && is_heap l && le_root x r && is_heap r
    end

  function minimum t : elt
  axiom minimum_def: forall l x r s. minimum (N s l x r) = x

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

  let rec lemma root_is_miminum (h: t) : unit
    requires { is_heap h && 0 < size h }
    ensures  { is_minimum (minimum h) h }
    variant  { h }
  = match h with
    | E -> absurd
    | N _ l _ r ->
Mário Pereira's avatar
Mário Pereira committed
146 147
       match l with E -> () | _ -> root_is_miminum l end;
       match r with E -> () | _ -> root_is_miminum r end
148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173
    end

  function rank (h: t) : int = match h with
    | E -> 0
    | N _ l _ r -> 1 + min (rank l) (rank r)
    end

  predicate leftist (h: t) = match h with
    | E -> true
    | N s l _ r ->
       s = rank h &&
       leftist l && leftist r &&
       rank l >= rank r
    end

   predicate leftist_heap (h: t) =
    is_heap h && leftist h

  let empty () : t
    ensures { size result = 0 }
    ensures { forall x. occ x result = 0 }
    ensures { leftist_heap result }
  = E

  let is_empty (h: t) : bool
    ensures { result <-> size h = 0 }
174
  = match h with E -> true | N _ _ _ _ -> false end
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 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237

  let rank (h: t) : int
    requires { leftist_heap h }
    ensures  { result = rank h }
  = match h with
    | E -> 0
    | N r _ _ _ -> r
    end

  let make_n (x: elt) (l r: t) : t
    requires { leftist_heap r && leftist_heap l }
    requires { le_root x l && le_root x r }
    ensures  { leftist_heap result }
    ensures  { minimum result = x }
    ensures  { size result = 1 + size l + size r }
    ensures  { occ x result = 1 + occ x l + occ x r }
    ensures  { forall y. x <> y -> occ y result = occ y l + occ y r }
  = if rank l >= rank r then N (rank r + 1) l x r
    else N (rank l + 1) r x l

  let rec merge (h1 h2: t) : t
    requires { leftist_heap h1 && leftist_heap h2 }
    ensures  { size result = size h1 + size h2 }
    ensures  { forall x. occ x result = occ x h1 + occ x h2 }
    ensures  { leftist_heap result }
    variant  { size h1 + size h2 }
  = match h1, h2 with
    | h, E | E, h -> h
    | N _ l1 x1 r1, N _ l2 x2 r2 ->
       if le x1 x2 then make_n x1 l1 (merge r1 h2)
       else make_n x2 l2 (merge h1 r2)
    end

  let insert (x: elt) (h: t) : t
    requires { leftist_heap h }
    ensures  { leftist_heap result }
    ensures  { occ x result = occ x h + 1 }
    ensures  { forall y. x <> y -> occ y result = occ y h }
    ensures  { size result = size h + 1 }
  = merge (N 1 E x E) h

  let find_min (h: t) : elt
    requires { leftist_heap h }
    requires { 0 < size h }
    ensures  { result = minimum h }
  = match h with
    | E -> absurd
    | N _ _ x _ -> x
    end

  let delete_min (h: t) : t
    requires { 0 < size h }
    requires { leftist_heap h }
    ensures  { occ (minimum h) result = occ (minimum h) h - 1 }
    ensures  { forall x. x <> minimum h -> occ x result = occ x h }
    ensures  { size result = size h - 1 }
    ensures  { leftist_heap result }
  = match h with
    | E -> absurd
    | N _ l _ r -> merge l r
    end

end