Wiki Agenda Contact Version française

Braun Trees

Purely applicative heaps implemented with Braun trees


Authors: Jean-Christophe Filliâtre

Topics: Data Structures

Tools: Why3

see also the index (by topic, by tool, by reference, by year)



Purely applicative heaps implemented with Braun trees.

Braun trees are binary trees where, for each node, the left subtree has the same size of the right subtree or is one element larger (predicate inv).

Consequently, a Braun tree has logarithmic height (lemma inv_height). The nice thing with Braun trees is that we do not need extra information to ensure logarithmic height.

We also prove an algorithm from Okasaki to compute the size of a braun tree in time O(log^2(n)) (function fast_size).

Author: Jean-Christophe Filliâtre (CNRS)

module BraunHeaps

  use import int.Int
  use import bintree.Tree
  use export bintree.Size
  use export bintree.Occ

  type elt

  predicate le elt elt
  clone relations.TotalPreOrder with type t = elt, predicate rel = le

  (* [e] is no greater than the root of [t], if any *)
  predicate le_root (e: elt) (t: tree elt) = match t with
    | Empty -> true
    | Node _ x _ -> le e x
  end

  predicate heap (t: tree elt) = match t with
    | Empty      -> true
    | Node l x r -> le_root x l && heap l && le_root x r && heap r
  end

  function minimum (tree elt) : elt
  axiom minimum_def: forall l x r. minimum (Node l x r) = x

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

  (* the root is the smallest element *)
  let rec lemma root_is_min (t: tree elt) : unit
     requires { heap t && 0 < size t }
     ensures  { is_minimum (minimum t) t }
     variant  { t }
  = match t with
    | Empty -> absurd
    | Node l _ r ->
        if l <> Empty then root_is_min l;
        if r <> Empty then root_is_min r
    end

  predicate inv (t: tree elt) = match t with
  | Empty      -> true
  | Node l _ r -> (size l = size r || size l = size r + 1) && inv l && inv r
  end

  let empty () : tree elt
    ensures { heap result }
    ensures { inv result }
    ensures { size result = 0 }
    ensures { forall e. not (mem e result) }
    = Empty

  let is_empty (t: tree elt) : bool
    ensures { result <-> size t = 0 }
  =
    t = Empty

  let size (t: tree elt) : int
    ensures { result = size t }
  =
    size t

  let get_min (t: tree elt) : elt
    requires { heap t && 0 < size t }
    ensures  { result = minimum t }
  =
    match t with
      | Empty      -> absurd
      | Node _ x _ -> x
    end

  let rec add (x: elt) (t: tree elt) : tree elt
    requires { heap t }
    requires { inv t }
    variant  { t }
    ensures  { heap result }
    ensures  { inv result }
    ensures  { occ x result = occ x t + 1 }
    ensures  { forall e. e <> x -> occ e result = occ e t }
    ensures  { size result = size t + 1 }
  =
    match t with
    | Empty ->
        Node Empty x Empty
    | Node l y r ->
        if le x y then
          Node (add y r) x l
        else
          Node (add x r) y l
    end

  let rec extract (t: tree elt) : (elt, tree elt)
     requires { heap t }
     requires { inv t }
     requires { 0 < size t }
     variant  { t }
     ensures  { let (e, t') = result in
                heap t' && inv t' && size t' = size t - 1 &&
                occ e t' = occ e t - 1 &&
                forall x. x <> e -> occ x t' = occ x t }
  =
    match t with
    | Empty ->
        absurd
    | Node Empty y r ->
        assert { r = Empty };
        (y, Empty)
    | Node l y r ->
        let (x, l) = extract l in
        (x, Node r y l)
    end

  let rec replace_min (x: elt) (t: tree elt)
    requires { heap t }
    requires { inv t }
    requires { 0 < size t }
    variant  { t }
    ensures  { heap result }
    ensures  { inv result }
    ensures  { if x = minimum t then occ x result = occ x t
               else occ x result = occ x t + 1 &&
                    occ (minimum t) result = occ (minimum t) t - 1 }
    ensures  { forall e. e <> x -> e <> minimum t -> occ e result = occ e t }
    ensures  { size result = size t }
  =
    match t with
    | Node l _ r ->
        if le_root x l && le_root x r then
          Node l x r
        else
          let lx = get_min l in
          if le_root lx r then
            (* lx <= x, rx necessarily *)
            Node (replace_min x l) lx r
          else
            (* rx <= x, lx necessarily *)
            Node l (get_min r) (replace_min x r)
    | Empty ->
        absurd
    end

  let rec merge (l r: tree elt) : tree elt
    requires { heap l && heap r }
    requires { inv l && inv r }
    requires { size r <= size l <= size r + 1 }
    ensures  { heap result }
    ensures  { inv result }
    ensures  { forall e. occ e result = occ e l + occ e r }
    ensures  { size result = size l + size r }
    variant  { size l + size r }
  =
    match l, r with
    | _, Empty ->
        l
    | Node ll lx lr, Node _ ly _ ->
        if le lx ly then
          Node r lx (merge ll lr)
        else
          let (x, l) = extract l in
          Node (replace_min x r) ly l
    | Empty, _ ->
        absurd
    end

  let remove_min (t: tree elt) : tree elt
    requires { heap t }
    requires { inv t }
    requires { 0 < size t }
    ensures  { heap result }
    ensures  { inv result }
    ensures  { occ (minimum t) result = occ (minimum t) t - 1 }
    ensures  { forall e. e <> minimum t -> occ e result = occ e t }
    ensures  { size result = size t - 1 }
  =
    match t with
      | Empty      -> absurd
      | Node l _ r -> merge l r
    end

The size of a Braun tree can be computed in time O(log^2(n))

from Three Algorithms on Braun Trees (Functional Pearl) Chris Okasaki J. Functional Programming 7 (6) 661–666, November 1997

  use import int.ComputerDivision

  let rec diff (m: int) (t: tree elt)
    requires { inv t }
    requires { 0 <= m <= size t <= m + 1 }
    variant  { t }
    ensures  { size t = m + result }
  = match t with
    | Empty ->
        0
    | Node l _ r ->
        if m = 0 then
          1
        else if mod m 2 = 1 then
          (* m = 2k + 1  *)
          diff (div m 2) l
        else
          (* m = 2k + 2 *)
          diff (div (m - 1) 2) r
    end

  let rec fast_size (t: tree elt) : int
    requires { inv t}
    variant  { t }
    ensures  { result = size t }
  =
    match t with
    | Empty -> 0
    | Node l _ r -> let m = fast_size r in 1 + 2 * m + diff m l
    end

A Braun tree has a logarithmic height

  use import bintree.Height
  use import int.Power

  let rec lemma size_height (t1 t2: tree elt)
    requires { inv t1 && inv t2 }
    variant  { size t1 + size t2 }
    ensures  { size t1 >= size t2 -> height t1 >= height t2 }
  = match t1, t2 with
    | Node l1 _ r1, Node l2 _ r2 ->
        size_height l1 l2;
        size_height r1 r2
    | _ ->
        ()
    end

  let rec lemma inv_height (t: tree elt)
    requires { inv t }
    variant  { t }
    ensures  { size t > 0 ->
               let h = height t in power 2 (h-1) <= size t < power 2 h }
  = match t with
    | Empty | Node Empty _ _ ->
        ()
    | Node l _ r ->
        let h = height t in
        assert { height l = h-1 };
        inv_height l;
        inv_height r
    end

end

download ZIP archive

Why3 Proof Results for Project "braun_trees"

Theory "braun_trees.BraunHeaps": fully verified in 15.74 s

ObligationsAlt-Ergo (0.99.1)CVC4 (1.4)
VC for root_is_min---0.10
VC for empty0.00---
VC for is_empty0.01---
VC for size0.02---
VC for get_min0.00---
VC for add------
split_goal_wp
  1. postcondition0.00---
2. postcondition0.02---
3. postcondition0.02---
4. postcondition0.01---
5. postcondition0.01---
6. variant decrease0.02---
7. precondition0.02---
8. precondition0.01---
9. postcondition---0.89
10. postcondition0.09---
11. postcondition0.04---
12. postcondition0.03---
13. postcondition0.01---
14. variant decrease0.02---
15. precondition0.01---
16. precondition0.01---
17. postcondition---0.04
18. postcondition0.07---
19. postcondition0.02---
20. postcondition0.04---
21. postcondition0.00---
VC for extract------
split_goal_wp
  1. unreachable point0.01---
2. assertion0.02---
3. postcondition0.02---
4. variant decrease0.01---
5. precondition0.01---
6. precondition0.01---
7. precondition0.02---
8. postcondition---1.50
VC for replace_min------
split_goal_wp
  1. postcondition0.15---
2. postcondition0.01---
3. postcondition0.13---
4. postcondition0.01---
5. postcondition0.01---
6. precondition0.03---
7. variant decrease0.03---
8. precondition0.02---
9. precondition0.02---
10. precondition0.01---
11. postcondition---0.45
12. postcondition0.52---
13. postcondition---0.04
14. postcondition1.47---
15. postcondition0.50---
16. variant decrease0.01---
17. precondition0.02---
18. precondition0.02---
19. precondition0.01---
20. precondition0.04---
21. postcondition---1.64
22. postcondition0.40---
23. postcondition---0.03
24. postcondition0.90---
25. postcondition0.20---
26. unreachable point0.00---
VC for merge------
split_goal_wp
  1. postcondition0.01---
2. postcondition0.01---
3. postcondition0.01---
4. postcondition0.01---
5. postcondition0.01---
6. postcondition0.02---
7. postcondition0.01---
8. postcondition0.02---
9. variant decrease0.01---
10. precondition0.02---
11. precondition0.02---
12. precondition0.07---
13. postcondition---0.09
14. postcondition0.02---
15. postcondition0.32---
16. postcondition0.03---
17. precondition0.01---
18. precondition0.02---
19. precondition0.00---
20. precondition0.01---
21. precondition0.01---
22. precondition0.04---
23. postcondition---0.25
24. postcondition0.02---
25. postcondition0.63---
26. postcondition0.02---
27. unreachable point0.01---
VC for remove_min0.03---
VC for diff------
split_goal_wp
  1. postcondition0.02---
2. postcondition0.01---
3. variant decrease0.02---
4. precondition0.02---
5. precondition0.05---
6. postcondition0.07---
7. variant decrease0.01---
8. precondition0.02---
9. precondition0.74---
10. postcondition1.95---
VC for fast_size------
split_goal_wp
  1. postcondition0.00---
2. variant decrease0.02---
3. precondition0.02---
4. precondition0.01---
5. precondition0.02---
6. postcondition0.00---
VC for size_height------
split_goal_wp
  1. variant decrease0.03---
2. precondition0.01---
3. variant decrease0.02---
4. precondition0.02---
5. postcondition0.26---
6. postcondition0.02---
7. postcondition0.00---
VC for inv_height------
split_goal_wp
  1. postcondition0.02---
2. postcondition0.38---
3. assertion0.39---
4. variant decrease0.02---
5. precondition0.02---
6. variant decrease0.00---
7. precondition0.02---
8. postcondition---0.04