examples/braun_trees.mlw

   1
   2 (** Purely applicative heaps implemented with Braun trees.
   3
   4     Braun trees are binary trees where, for each node, the left subtree
   5     has the same size of the right subtree or is one element larger
   6     (predicate [inv]).
   7
   8     Consequently, a Braun tree has logarithmic height (lemma [inv_height]).
   9     The nice thing with Braun trees is that we do not need extra information
  10     to ensure logarithmic height.
  11
  12     We also prove an algorithm from Okasaki to compute the size of a braun
  13     tree in time O(log^2(n)) (function [fast_size]).
  14
  15     Author: Jean-Christophe Filliâtre (CNRS)
  16 *)
  17
  18 module BraunHeaps
  19
  20   use int.Int
  21   use bintree.Tree
  22   use export bintree.Size
  23   use export bintree.Occ
  24
  25   type elt
  26
  27   val predicate le elt elt
  28
  29   clone relations.TotalPreOrder with type t = elt, predicate rel = le, axiom .
  30
  31   (* [e] is no greater than the root of [t], if any *)
  32   let predicate le_root (e: elt) (t: tree elt) = match t with
  33     | Empty -> true
  34     | Node _ x _ -> le e x
  35   end
  36
  37   predicate heap (t: tree elt) = match t with
  38     | Empty      -> true
  39     | Node l x r -> le_root x l && heap l && le_root x r && heap r
  40   end
  41
  42   function minimum (tree elt) : elt
  43   axiom minimum_def: forall l x r. minimum (Node l x r) = x
  44
  45   predicate is_minimum (x: elt) (t: tree elt) =
  46     mem x t && forall e. mem e t -> le x e
  47
  48   (* the root is the smallest element *)
  49   let rec lemma root_is_min (t: tree elt) : unit
  50      requires { heap t && 0 < size t }
  51      ensures  { is_minimum (minimum t) t }
  52      variant  { t }
  53   = let Node l _ r = t in
  54     if not is_empty l then root_is_min l;
  55     if not is_empty r then root_is_min r
  56
  57   predicate inv (t: tree elt) = match t with
  58   | Empty      -> true
  59   | Node l _ r -> (size l = size r || size l = size r + 1) && inv l && inv r
  60   end
  61
  62   let constant empty : tree elt = Empty
  63     ensures { heap result }
  64     ensures { inv result }
  65     ensures { size result = 0 }
  66     ensures { forall e. not (mem e result) }
  67
  68   let get_min (t: tree elt) : elt
  69     requires { heap t && 0 < size t }
  70     ensures  { result = minimum t }
  71   =
  72     match t with
  73       | Empty      -> absurd
  74       | Node _ x _ -> x
  75     end
  76
  77   let rec add (x: elt) (t: tree elt) : tree elt
  78     requires { heap t }
  79     requires { inv t }
  80     variant  { t }
  81     ensures  { heap result }
  82     ensures  { inv result }
  83     ensures  { occ x result = occ x t + 1 }
  84     ensures  { forall e. e <> x -> occ e result = occ e t }
  85     ensures  { size result = size t + 1 }
  86   =
  87     match t with
  88     | Empty ->
  89         Node Empty x Empty
  90     | Node l y r ->
  91         if le x y then
  92           Node (add y r) x l
  93         else
  94           Node (add x r) y l
  95     end
  96
  97   let rec extract (t: tree elt) : (elt, tree elt)
  98      requires { heap t }
  99      requires { inv t }
 100      requires { 0 < size t }
 101      variant  { t }
 102      ensures  { let e, t' = result in
 103                 heap t' && inv t' && size t' = size t - 1 &&
 104                 occ e t' = occ e t - 1 &&
 105                 forall x. x <> e -> occ x t' = occ x t }
 106   =
 107     match t with
 108     | Empty ->
 109         absurd
 110     | Node Empty y r ->
 111         assert { r = Empty };
 112         y, Empty
 113     | Node l y r ->
 114         let x, l = extract l in
 115         x, Node r y l
 116     end
 117
 118   let rec replace_min (x: elt) (t: tree elt) : tree elt
 119     requires { heap t }
 120     requires { inv t }
 121     requires { 0 < size t }
 122     variant  { t }
 123     ensures  { heap result }
 124     ensures  { inv result }
 125     ensures  { if x = minimum t then occ x result = occ x t
 126                else occ x result = occ x t + 1 &&
 127                     occ (minimum t) result = occ (minimum t) t - 1 }
 128     ensures  { forall e. e <> x -> e <> minimum t -> occ e result = occ e t }
 129     ensures  { size result = size t }
 130   =
 131     match t with
 132     | Node l _ r ->
 133         if le_root x l && le_root x r then
 134           Node l x r
 135         else
 136           let lx = get_min l in
 137           if le_root lx r then
 138             (* lx <= x, rx necessarily *)
 139             Node (replace_min x l) lx r
 140           else
 141             (* rx <= x, lx necessarily *)
 142             Node l (get_min r) (replace_min x r)
 143     | Empty ->
 144         absurd
 145     end
 146
 147   let rec merge (l r: tree elt) : tree elt
 148     requires { heap l && heap r }
 149     requires { inv l && inv r }
 150     requires { size r <= size l <= size r + 1 }
 151     ensures  { heap result }
 152     ensures  { inv result }
 153     ensures  { forall e. occ e result = occ e l + occ e r }
 154     ensures  { size result = size l + size r }
 155     variant  { size l + size r }
 156   =
 157     match l, r with
 158     | _, Empty ->
 159         l
 160     | Node ll lx lr, Node _ ly _ ->
 161         if le lx ly then
 162           Node r lx (merge ll lr)
 163         else
 164           let x, l = extract l in
 165           Node (replace_min x r) ly l
 166     | Empty, _ ->
 167         absurd
 168     end
 169
 170   let remove_min (t: tree elt) : tree elt
 171     requires { heap t }
 172     requires { inv t }
 173     requires { 0 < size t }
 174     ensures  { heap result }
 175     ensures  { inv result }
 176     ensures  { occ (minimum t) result = occ (minimum t) t - 1 }
 177     ensures  { forall e. e <> minimum t -> occ e result = occ e t }
 178     ensures  { size result = size t - 1 }
 179   =
 180     match t with
 181       | Empty      -> absurd
 182       | Node l _ r -> merge l r
 183     end
 184
 185   (** The size of a Braun tree can be computed in time O(log^2(n))
 186
 187       from
 188         Three Algorithms on Braun Trees (Functional Pearl)
 189         Chris Okasaki
 190         J. Functional Programming 7 (6) 661–666, November 1997 *)
 191
 192   use int.ComputerDivision
 193
 194   let rec diff (m: int) (t: tree elt) : int
 195     requires { inv t }
 196     requires { 0 <= m <= size t <= m + 1 }
 197     variant  { t }
 198     ensures  { size t = m + result }
 199   = match t with
 200     | Empty ->
 201         0
 202     | Node l _ r ->
 203         if m = 0 then
 204           1
 205         else if mod m 2 = 1 then
 206           (* m = 2k + 1  *)
 207           diff (div m 2) l
 208         else
 209           (* m = 2k + 2 *)
 210           diff (div (m - 1) 2) r
 211     end
 212
 213   let rec fast_size (t: tree elt) : int
 214     requires { inv t}
 215     variant  { t }
 216     ensures  { result = size t }
 217   =
 218     match t with
 219     | Empty      -> 0
 220     | Node l _ r -> let m = fast_size r in 1 + 2 * m + diff m l
 221     end
 222
 223   (** A Braun tree has a logarithmic height *)
 224
 225   use bintree.Height
 226   use int.Power
 227
 228   let rec lemma size_height (t1 t2: tree elt)
 229     requires { inv t1 && inv t2 }
 230     variant  { size t1 + size t2 }
 231     ensures  { size t1 >= size t2 -> height t1 >= height t2 }
 232   = match t1, t2 with
 233     | Node l1 _ r1, Node l2 _ r2 ->
 234         size_height l1 l2;
 235         size_height r1 r2
 236     | _ ->
 237         ()
 238     end
 239
 240   let rec lemma inv_height (t: tree elt)
 241     requires { inv t }
 242     variant  { t }
 243     ensures  { size t > 0 ->
 244                let h = height t in power 2 (h-1) <= size t < power 2 h }
 245   = match t with
 246     | Empty | Node Empty _ _ ->
 247         ()
 248     | Node l _ r ->
 249         let h = height t in
 250         assert { height l = h-1 };
 251         inv_height l;
 252         inv_height r
 253     end
 254
 255 end