examples/pairing_heap_bin.mlw

   1
   2 (** Pairing heaps (M. Fredman, R. Sedgewick, D. Sleator, R. Tarjan, 1986).
   3
   4     Author: Mário Pereira (Université Paris Sud)
   5
   6     This is a re-implementation of pairing heaps as binary trees.
   7     See also pairing_heap.mlw in the gallery.
   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 bintree.Tree
  70
  71   type elt
  72   type heap = E | T elt (tree elt)
  73
  74 end
  75
  76 module Size
  77
  78   use HeapType
  79   use int.Int
  80   use bintree.Tree
  81   use bintree.Size as T
  82
  83   let function size (h: heap) : int = match h with
  84     | E -> 0
  85     | T _ r -> 1 + T.size r
  86     end
  87
  88   let lemma size_nonneg (h: heap) : unit
  89     ensures { size h >= 0 }
  90   = match h with
  91     | E -> ()
  92     | T _ r -> assert { T.size r >= 0 }
  93     end
  94
  95   lemma size_empty: forall h.
  96     size h = 0 <-> h = E
  97
  98 end
  99
 100 module Occ
 101
 102   use HeapType
 103   use int.Int
 104   use bintree.Tree
 105   use bintree.Occ as T
 106
 107   function occ (x: elt) (h: heap) : int = match h with
 108     | E -> 0
 109     | T e r -> (if x = e then 1 else 0) + T.occ x r
 110     end
 111
 112   let lemma occ_nonneg (x: elt) (h: heap) : unit
 113     ensures { occ x h >= 0 }
 114   = match h with
 115     | E -> ()
 116     | T _ r -> assert { T.occ x r >= 0 }
 117     end
 118
 119   predicate mem (x: elt) (h: heap) =
 120     0 < occ x h
 121
 122 end
 123
 124 module PairingHeap
 125
 126   use int.Int
 127   use bintree.Tree
 128   use bintree.Occ as T
 129   use bintree.Size as TS
 130   use HeapType
 131   use Size
 132   use Occ
 133
 134   val predicate le elt elt
 135   clone relations.TotalPreOrder with
 136     type t = elt, predicate rel = le, axiom .
 137
 138   predicate le_root (e: elt) (h: heap) = match h with
 139     | E -> true
 140     | T x _ -> le e x
 141     end
 142
 143   lemma le_root_trans:
 144     forall x y h. le x y -> le_root y h -> le_root x h
 145
 146   predicate le_root_tree (e: elt) (t: tree elt) = match t with
 147     | Empty -> true
 148     | Node _ x r -> le e x && le_root_tree e r
 149     end
 150
 151   lemma le_root_tree_trans:
 152     forall x y t. le x y -> le_root_tree y t -> le_root_tree x t
 153
 154   predicate heap_tree (t: tree elt) = match t with
 155     | Empty -> true
 156     | Node l x r -> le_root_tree x l && heap_tree l && heap_tree r
 157     end
 158
 159   predicate heap (h: heap) = match h with
 160     | E -> true
 161     | T x r -> le_root_tree x r && heap_tree r
 162     end
 163
 164   function minimum (h: heap) : elt
 165   axiom minimum_def: forall x r. minimum (T x r) = x
 166
 167   predicate is_minimum (x: elt) (h: heap) =
 168     mem x h && forall e. mem e h -> le x e
 169
 170   let rec lemma mem_heap_tree (t: tree elt)
 171     requires { heap_tree t }
 172     ensures  { forall x. le_root_tree x t -> forall y. T.mem y t -> le x y }
 173     variant  { t }
 174   = match t with
 175     | Empty -> ()
 176     | Node l _ r ->
 177        mem_heap_tree l;
 178        mem_heap_tree r
 179     end
 180
 181   let lemma mem_heap (h: heap)
 182     requires { heap h }
 183     ensures  { forall x. le_root x h -> forall y. mem y h -> le x y }
 184   = match h with
 185     | E -> ()
 186     | T _ r -> mem_heap_tree r
 187     end
 188
 189   lemma root_is_minimum: forall h.
 190     heap h -> 0 < size h -> is_minimum (minimum h) h
 191
 192   let constant empty : heap = E
 193     ensures { heap result }
 194     ensures { size result = 0 }
 195     ensures { forall e. not (mem e result) }
 196
 197   let is_empty (h: heap) : bool
 198     ensures { result <-> size h = 0 }
 199   = match h with E -> true | _ -> false end
 200
 201   let size (h: heap) : int
 202     ensures { result = size h }
 203   = size h
 204
 205   let merge (h1 h2: heap) : heap
 206     requires { heap h1 && heap h2 }
 207     ensures  { heap result }
 208     ensures  { size result = size h1 + size h2 }
 209     ensures  { forall x. occ x result = occ x h1 + occ x h2 }
 210   = match h1, h2 with
 211     | E, h | h, E -> h
 212     | T x1 r1, T x2 r2 ->
 213        if le x1 x2 then
 214          T x1 (Node r2 x2 r1)
 215        else
 216          T x2 (Node r1 x1 r2)
 217     end
 218
 219   let insert (x: elt) (h: heap) : heap
 220     requires { heap h }
 221     ensures  { heap result }
 222     ensures  { occ x result = occ x h + 1 }
 223     ensures  { forall y. x <> y -> occ y result = occ y h }
 224     ensures  { size result = size h + 1 }
 225   = merge (T x Empty) h
 226
 227   let find_min (h: heap) : elt
 228     requires { heap h && 0 < size h }
 229     ensures  { result = minimum h }
 230   = match h with
 231     | E -> absurd
 232     | T x _ -> x
 233     end
 234
 235   let rec merge_pairs (t: tree elt) : heap
 236     requires { heap_tree t }
 237     ensures  { heap result }
 238     ensures  { size result = TS.size t }
 239     ensures  { forall x. occ x result = T.occ x t }
 240     variant  { TS.size t }
 241   = match t with
 242     | Empty -> E
 243     | Node l x Empty -> T x l
 244     | Node l x (Node l2 y r) ->
 245        let h = T x l in
 246        let h' = T y l2 in
 247        merge (merge h h') (merge_pairs r)
 248     end
 249
 250   let delete_min (h: heap) : heap
 251     requires { heap h && 0 < size h }
 252     ensures  { heap result }
 253     ensures  { occ (minimum h) result = occ (minimum h) h - 1 }
 254     ensures  { forall e. e <> minimum h -> occ e result = occ e h }
 255     ensures  { size result = size h - 1 }
 256   = match h with
 257     | E -> absurd
 258     | T _ l -> merge_pairs l
 259     end
 260
 261 end