examples/leftist_heap.mlw

   1
   2 (** Leftist heaps (Clark Allan Crane, 1972 && Donald E. Knuth, 1973).
   3
   4     Purely applicative implementation, following Okasaki's implementation
   5     in his book "Purely Functional Data Structures" (Section 3.1).
   6
   7     Author: Mário Pereira (Université Paris Sud)
   8 *)
   9
  10 module Heap
  11
  12   use int.Int
  13
  14   type elt
  15   predicate le elt elt
  16
  17   clone relations.TotalPreOrder with
  18     type t = elt, predicate rel = le, axiom .
  19
  20   type heap
  21
  22   val 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 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 merge (h1 h2: heap) : heap
  44     ensures { forall x. occ x result = occ x h1 + occ x h2 }
  45     ensures { size result = size h1 + size h2 }
  46
  47   val insert (x: elt) (h: heap) : heap
  48     ensures { occ x result = occ x h + 1 }
  49     ensures { forall y. y <> x -> occ y h = occ y result }
  50     ensures { size result = size h + 1 }
  51
  52   val find_min (h: heap) : elt
  53     requires { size h > 0 }
  54     ensures  { result = minimum h }
  55
  56   val delete_min (h: heap) : heap
  57     requires { size h > 0 }
  58     ensures  { let x = minimum h in occ x result = occ x h - 1 }
  59     ensures  { forall y. y <> minimum h -> occ y result = occ y h }
  60     ensures  { size result = size h - 1 }
  61
  62 end
  63
  64 module TreeRank
  65
  66   type tree 'a = E | N int (tree 'a) 'a (tree 'a)
  67
  68 end
  69
  70 module Size
  71
  72   use TreeRank
  73   use int.Int
  74
  75   let rec function size (t: tree 'a) : int = match t with
  76     | E -> 0
  77     | N _ l _ r -> 1 + size l + size r
  78     end
  79
  80   lemma size_nonneg: forall t: tree 'a. 0 <= size t
  81   lemma size_empty: forall t: tree 'a. 0 = size t <-> t = E
  82
  83 end
  84
  85 module Occ
  86
  87   use TreeRank
  88   use int.Int
  89
  90   function occ (x: 'a) (t: tree 'a) : int = match t with
  91     | E -> 0
  92     | N _ l e r -> (if x = e then 1 else 0) + occ x l + occ x r
  93     end
  94
  95   lemma occ_nonneg:
  96     forall x:'a, t. 0 <= occ x t
  97
  98   predicate mem (x: 'a) (t: tree 'a) =
  99     0 < occ x t
 100
 101 end
 102
 103 module LeftistHeap
 104
 105   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   use export Size
 112   use export Occ
 113   use int.Int
 114   use int.MinMax
 115
 116   type t = tree elt
 117
 118   (* [e] is no greater than the root of [h], if any *)
 119   predicate le_root (e: elt) (h: t) = match h with
 120     | E -> true
 121     | N _ _ x _ -> le e x
 122     end
 123
 124   lemma le_root_trans:
 125     forall x y h. le x y -> le_root y h -> le_root x h
 126
 127   (* [h] is a heap *)
 128   predicate is_heap (h: t) = match h with
 129     | E -> true
 130     | N _ l x r -> le_root x l && is_heap l && le_root x r && is_heap r
 131     end
 132
 133   function minimum t : elt
 134   axiom minimum_def: forall l x r s. minimum (N s l x r) = x
 135
 136   predicate is_minimum (x: elt) (h: t) =
 137     mem x h && forall e. mem e h -> le x e
 138
 139   let rec lemma root_is_miminum (h: t) : unit
 140     requires { is_heap h && 0 < size h }
 141     ensures  { is_minimum (minimum h) h }
 142     variant  { h }
 143   = match h with
 144     | E -> absurd
 145     | N _ l _ r ->
 146        match l with E -> () | _ -> root_is_miminum l end;
 147        match r with E -> () | _ -> root_is_miminum r end
 148     end
 149
 150   function rank (h: t) : int = match h with
 151     | E -> 0
 152     | N _ l _ r -> 1 + min (rank l) (rank r)
 153     end
 154
 155   predicate leftist (h: t) = match h with
 156     | E -> true
 157     | N s l _ r ->
 158        s = rank h &&
 159        leftist l && leftist r &&
 160        rank l >= rank r
 161     end
 162
 163    predicate leftist_heap (h: t) =
 164     is_heap h && leftist h
 165
 166   let empty : t = E
 167     ensures { size result = 0 }
 168     ensures { forall x. occ x result = 0 }
 169     ensures { leftist_heap result }
 170
 171   let is_empty (h: t) : bool
 172     ensures { result <-> size h = 0 }
 173   = match h with E -> true | N _ _ _ _ -> false end
 174
 175   let rank (h: t) : int
 176     requires { leftist_heap h }
 177     ensures  { result = rank h }
 178   = match h with
 179     | E -> 0
 180     | N r _ _ _ -> r
 181     end
 182
 183   let make_n (x: elt) (l r: t) : t
 184     requires { leftist_heap r && leftist_heap l }
 185     requires { le_root x l && le_root x r }
 186     ensures  { leftist_heap result }
 187     ensures  { minimum result = x }
 188     ensures  { size result = 1 + size l + size r }
 189     ensures  { occ x result = 1 + occ x l + occ x r }
 190     ensures  { forall y. x <> y -> occ y result = occ y l + occ y r }
 191   = if rank l >= rank r then N (rank r + 1) l x r
 192     else N (rank l + 1) r x l
 193
 194   let rec merge (h1 h2: t) : t
 195     requires { leftist_heap h1 && leftist_heap h2 }
 196     ensures  { size result = size h1 + size h2 }
 197     ensures  { forall x. occ x result = occ x h1 + occ x h2 }
 198     ensures  { leftist_heap result }
 199     variant  { size h1 + size h2 }
 200   = match h1, h2 with
 201     | h, E | E, h -> h
 202     | N _ l1 x1 r1, N _ l2 x2 r2 ->
 203        if le x1 x2 then make_n x1 l1 (merge r1 h2)
 204        else make_n x2 l2 (merge h1 r2)
 205     end
 206
 207   let insert (x: elt) (h: t) : t
 208     requires { leftist_heap h }
 209     ensures  { leftist_heap result }
 210     ensures  { occ x result = occ x h + 1 }
 211     ensures  { forall y. x <> y -> occ y result = occ y h }
 212     ensures  { size result = size h + 1 }
 213   = merge (N 1 E x E) h
 214
 215   let find_min (h: t) : elt
 216     requires { leftist_heap h }
 217     requires { 0 < size h }
 218     ensures  { result = minimum h }
 219   = match h with
 220     | E -> absurd
 221     | N _ _ x _ -> x
 222     end
 223
 224   let delete_min (h: t) : t
 225     requires { 0 < size h }
 226     requires { leftist_heap h }
 227     ensures  { occ (minimum h) result = occ (minimum h) h - 1 }
 228     ensures  { forall x. x <> minimum h -> occ x result = occ x h }
 229     ensures  { size result = size h - 1 }
 230     ensures  { leftist_heap result }
 231   = match h with
 232     | E -> absurd
 233     | N _ l _ r -> merge l r
 234     end
 235
 236 end