examples/pairing_heap.mlw

   1
   2 (** Pairing heaps (M. Fredman, R. Sedgewick, D. Sleator, R. Tarjan, 1986).
   3
   4     Purely applicative implementation, following Okasaki's implementation
   5     in his book "Purely Functional Data Structures" (Section 5.5).
   6
   7     Author: Mário Pereira (Université Paris Sud)
   8 *)
   9
  10 module Heap
  11
  12   use int.Int
  13
  14   type elt
  15   val predicate le elt elt
  16
  17   clone relations.TotalPreOrder with
  18     type t = elt, predicate rel = le, axiom .
  19
  20   type heap
  21
  22   function size heap : int
  23
  24   function occ elt heap : int
  25
  26   predicate mem (x: elt) (h: heap) = occ x h > 0
  27
  28   function minimum heap : elt
  29
  30   predicate is_minimum (x: elt) (h: heap) =
  31     mem x h && forall e. mem e h -> le x e
  32
  33   axiom min_def:
  34     forall h. 0 < size h -> is_minimum (minimum h) h
  35
  36   val constant empty : heap
  37     ensures { size result = 0 }
  38     ensures { forall x. occ x result = 0 }
  39
  40   val is_empty (h: heap) : bool
  41     ensures { result <-> size h = 0 }
  42
  43   val size (h: heap) : int
  44     ensures { result = size h }
  45
  46   val merge (h1 h2: heap) : heap
  47     ensures { forall x. occ x result = occ x h1 + occ x h2 }
  48     ensures { size result = size h1 + size h2 }
  49
  50   val insert (x: elt) (h: heap) : heap
  51     ensures { occ x result = occ x h + 1 }
  52     ensures { forall y. y <> x -> occ y h = occ y result }
  53     ensures { size result = size h + 1 }
  54
  55   val find_min (h: heap) : elt
  56     requires { size h > 0 }
  57     ensures  { result = minimum h }
  58
  59   val delete_min (h: heap) : heap
  60     requires { size h > 0 }
  61     ensures  { let x = minimum h in occ x result = occ x h - 1 }
  62     ensures  { forall y. y <> minimum h -> occ y result = occ y h }
  63     ensures  { size result = size h - 1 }
  64
  65 end
  66
  67 module HeapType
  68
  69   use list.List
  70
  71   type elt
  72
  73   type raw_heap = E | H tree
  74   with tree     = T elt (list tree)
  75
  76 end
  77
  78 module Size
  79
  80   use HeapType
  81   use int.Int
  82   use list.List
  83
  84   function size_heap (h: raw_heap) : int = match h with
  85     | E -> 0
  86     | H t -> size_tree t
  87     end
  88   with size_tree (t: tree) : int = match t with
  89     | T _ l -> 1 + size_list l
  90     end
  91   with size_list (l: list tree) : int = match l with
  92     | Nil -> 0
  93     | Cons t l -> size_tree t + size_list l
  94     end
  95
  96   let rec lemma size_nonneg (h: raw_heap)
  97     ensures { size_heap h >= 0 }
  98     variant { h }
  99   = match h with
 100     | E -> ()
 101     | H t -> size_tree_nonneg t
 102     end
 103   with lemma size_tree_nonneg (t: tree)
 104     ensures { size_tree t >= 0 }
 105     variant { t }
 106   = match t with T _ l -> size_list_nonneg l end
 107   with lemma size_list_nonneg (l: list tree)
 108     ensures { size_list l >= 0 }
 109     variant { l }
 110   = match l with
 111     | Nil -> ()
 112     | Cons t r ->
 113        size_tree_nonneg t; size_list_nonneg r
 114     end
 115
 116   let lemma size_empty (h: raw_heap)
 117     ensures { size_heap h = 0 <-> h = E }
 118   = match h with
 119     | E -> ()
 120     | H t -> size_tree_nonneg t
 121     end
 122
 123 end
 124
 125 module Occ
 126
 127   use HeapType
 128   use int.Int
 129   use list.List
 130
 131   function occ_heap (x: elt) (h: raw_heap) : int = match h with
 132     | E -> 0
 133     | H t -> occ_tree x t
 134     end
 135   with occ_tree (x: elt) (t: tree) : int = match t with
 136     | T e l -> (if x = e then 1 else 0) + occ_list x l
 137     end
 138   with occ_list (x: elt) (l: list tree) : int = match l with
 139     | Nil -> 0
 140     | Cons t r -> occ_tree x t + occ_list x r
 141     end
 142
 143   let rec lemma occ_nonneg (x: elt) (h: raw_heap)
 144     ensures { occ_heap x h >= 0 }
 145     variant { h }
 146   = match h with
 147     | E -> ()
 148     | H t -> occ_tree_nonneg x t
 149     end
 150   with lemma occ_tree_nonneg (x: elt) (t: tree)
 151     ensures { occ_tree x t >= 0 }
 152     variant { t }
 153   = match t with T _ l -> occ_list_nonneg x l end
 154   with lemma occ_list_nonneg (x: elt) (l: list tree)
 155     ensures { occ_list x l >= 0 }
 156     variant { l }
 157   = match l with
 158     | Nil -> ()
 159     | Cons t r ->
 160        occ_tree_nonneg x t; occ_list_nonneg x r
 161     end
 162
 163   predicate mem (x: elt) (h: raw_heap) =
 164     0 < occ_heap x h
 165
 166   predicate mem_tree (x: elt) (t: tree) =
 167     0 < occ_tree x t
 168
 169   predicate mem_list (x: elt) (l: list tree) =
 170     0 < occ_list x l
 171
 172 end
 173
 174 module PairingHeap
 175
 176   use int.Int
 177   use export HeapType
 178   use export Size
 179   use export Occ
 180   use list.List
 181   use list.Length
 182
 183   val predicate le elt elt
 184   clone relations.TotalPreOrder with
 185     type t = elt, predicate rel = le, axiom .
 186
 187   (* [e] is no greater than the root of [h], if any *)
 188   predicate le_tree (e: elt) (t: tree) = match t with
 189     | T x _ -> le e x
 190     end
 191
 192   predicate le_root (e: elt) (h: raw_heap) = match h with
 193     | E -> true
 194     | H t -> le_tree e t
 195     end
 196
 197   lemma le_root_trans:
 198     forall x y h. le x y -> le_root y h -> le_root x h
 199
 200   (* [e] is no greater than the roots of the trees in [l] *)
 201   predicate le_roots (e: elt) (l: list tree) = match l with
 202     | Nil -> true
 203     | Cons t r -> le_tree e t && le_roots e r
 204     end
 205
 206   lemma le_roots_trans:
 207     forall x y l. le x y -> le_roots y l -> le_roots x l
 208
 209   predicate heap (h: raw_heap) = match h with
 210     | E -> true
 211     | H t -> heap_tree t
 212     end
 213   with heap_tree (t: tree) = match t with
 214     | T x l -> le_roots x l && heap_list l
 215     end
 216   with heap_list (l: list tree) = match l with
 217     | Nil -> true
 218     | Cons t r -> heap_tree t && heap_list r
 219     end
 220
 221   type heap = { h: raw_heap }
 222     invariant { heap h }
 223     by { h = E }
 224
 225   function size (hh: heap) : int = size_heap hh.h
 226   function occ (e: elt) (hh: heap) : int = occ_heap e hh.h
 227
 228   let rec lemma heap_mem (h: raw_heap)
 229     requires { heap h }
 230     variant  { h }
 231     ensures  { forall x. le_root x h -> forall y. mem y h -> le x y }
 232   = match h with
 233     | E -> ()
 234     | H t -> heap_mem_tree t
 235     end
 236   with heap_mem_tree (t: tree)
 237     requires { heap_tree t }
 238     variant  { t }
 239     ensures  { forall x. le_tree x t -> forall y. mem_tree y t -> le x y }
 240   = match t with T _ l -> heap_mem_list l end
 241   with heap_mem_list (l: list tree)
 242     requires { heap_list l }
 243     variant  { l }
 244     ensures  { forall x. le_roots x l -> forall y. mem_list y l -> le x y }
 245   = match l with
 246     | Nil -> ()
 247     | Cons t r ->
 248        heap_mem_tree t;
 249        heap_mem_list r
 250     end
 251
 252   predicate is_minimum_tree (x: elt) (t: tree) =
 253     mem_tree x t && forall e. mem_tree e t -> le x e
 254
 255   predicate is_minimum (x: elt) (h: raw_heap) =
 256     mem x h && forall e. mem e h -> le x e
 257
 258   function minimum_tree tree : elt
 259   axiom minimum_tree_def: forall x l. minimum_tree (T x l) = x
 260
 261   function minimum raw_heap : elt
 262   axiom minimum_def: forall t. minimum (H t) = minimum_tree t
 263
 264   function minimum_heap (hh: heap) : elt =
 265     minimum hh.h
 266
 267   let lemma root_is_minimum (h: raw_heap)
 268     requires { 0 < size_heap h }
 269     requires { heap h }
 270     ensures  { is_minimum (minimum h) h }
 271   = match h with
 272     | E -> absurd
 273     | H (T e l) -> occ_list_nonneg e l
 274     end
 275
 276   let constant empty : heap = { h = E }
 277     ensures { size_heap result.h = 0 }
 278     ensures { forall e. not (mem e result.h) }
 279
 280   let is_empty (hh: heap) : bool
 281     ensures { result <-> size_heap hh.h = 0 }
 282   = match hh.h with E -> true | _ -> false end
 283
 284   let merge (h1 h2: heap) : heap
 285     ensures  { size_heap result.h = size_heap h1.h + size_heap h2.h }
 286     ensures  { forall x. occ_heap x result.h
 287                        = occ_heap x h1.h + occ_heap x h2.h }
 288   = match h1.h, h2.h with
 289     | E, h | h, E -> { h = h }
 290     | H (T x1 l1), H (T x2 l2) ->
 291        if le x1 x2 then
 292          { h = H (T x1 (Cons (T x2 l2) l1)) }
 293        else
 294          { h = H (T x2 (Cons (T x1 l1) l2)) }
 295     end
 296
 297   let insert (x: elt) (hh: heap) : heap
 298     ensures  { size_heap result.h = size_heap hh.h + 1 }
 299     ensures  { occ_heap x result.h = occ_heap x hh.h + 1 }
 300     ensures  { forall y. x <> y -> occ_heap y result.h = occ_heap y hh.h }
 301   = merge { h = H (T x Nil) } hh
 302
 303   let find_min (hh: heap) : elt
 304     requires { 0 < size_heap hh.h }
 305     ensures  { result = minimum hh.h }
 306   = match hh.h with
 307     | E -> absurd
 308     | H (T x _) -> x
 309     end
 310
 311   let rec merge_pairs (l: list tree) : heap
 312     requires { heap_list l }
 313     ensures  { size_heap result.h = size_list l }
 314     ensures  { forall x. occ_heap x result.h = occ_list x l }
 315     variant  { length l }
 316   = match l with
 317     | Nil -> { h = E }
 318     | Cons t Nil -> { h = H t }
 319     | Cons t1 (Cons t2 r) ->
 320        let h1 = { h = H t1 } in
 321        let h2 = { h = H t2 } in
 322        merge (merge h1 h2) (merge_pairs r)
 323     end
 324
 325   let delete_min (hh: heap) : heap
 326     requires { 0 < size_heap hh.h }
 327     ensures  { occ_heap (minimum hh.h) result.h =
 328                occ_heap (minimum hh.h) hh.h - 1 }
 329     ensures  { forall y. y <> minimum hh.h ->
 330                  occ_heap y result.h = occ_heap y hh.h }
 331     ensures  { size_heap result.h = size_heap hh.h - 1 }
 332   = match hh.h with
 333     | E -> absurd
 334     | H (T _ l) ->
 335        merge_pairs l
 336     end
 337
 338 end
 339
 340 module Correct
 341
 342   use PairingHeap
 343   use Size
 344
 345   clone Heap with
 346     type elt, type heap, val le,
 347     function size, function occ,
 348     function minimum = minimum_heap,
 349     val empty,  val is_empty, val merge,
 350     val insert, val find_min, val delete_min
 351
 352 end