## 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 int.Int use bintree.Tree use export bintree.Size use export bintree.Occ type elt val predicate le elt elt clone relations.TotalPreOrder with type t = elt, predicate rel = le, axiom . (* [e] is no greater than the root of [t], if any *) let 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 } = let Node l _ r = t in if not is_empty l then root_is_min l; if not is_empty r then root_is_min r 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 constant empty : tree elt = Empty ensures { heap result } ensures { inv result } ensures { size result = 0 } ensures { forall e. not (mem e result) } 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) : 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 int.ComputerDivision let rec diff (m: int) (t: tree elt) : int 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 bintree.Height use 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

Obligations | Alt-Ergo 2.0.0 | Alt-Ergo 2.3.1 | CVC4 1.5 | CVC4 1.7 | ||

VC for root_is_min | 0.70 | --- | --- | --- | ||

VC for empty | 0.00 | --- | --- | --- | ||

VC for get_min | --- | 0.00 | --- | --- | ||

VC for add | --- | --- | --- | --- | ||

split_vc | ||||||

variant decrease | --- | --- | --- | 0.06 | ||

precondition | --- | --- | --- | 0.04 | ||

precondition | --- | --- | --- | 0.05 | ||

variant decrease | --- | --- | --- | 0.07 | ||

precondition | --- | --- | --- | 0.04 | ||

precondition | --- | --- | --- | 0.06 | ||

postcondition | --- | --- | --- | --- | ||

split_vc | ||||||

postcondition | --- | --- | --- | 0.05 | ||

postcondition | --- | 1.13 | --- | --- | ||

postcondition | --- | --- | --- | --- | ||

split_vc | ||||||

postcondition | --- | --- | --- | 0.06 | ||

postcondition | --- | --- | --- | 0.07 | ||

postcondition | --- | --- | --- | --- | ||

split_vc | ||||||

postcondition | --- | --- | --- | 0.07 | ||

postcondition | --- | --- | --- | 0.09 | ||

postcondition | --- | --- | --- | --- | ||

split_vc | ||||||

postcondition | --- | --- | --- | 0.07 | ||

postcondition | --- | --- | --- | 0.08 | ||

postcondition | --- | --- | --- | --- | ||

split_vc | ||||||

postcondition | --- | --- | --- | 0.06 | ||

postcondition | --- | --- | --- | 0.07 | ||

VC for extract | --- | 2.36 | --- | --- | ||

VC for replace_min | --- | --- | --- | --- | ||

split_goal_right | ||||||

precondition | --- | 0.01 | --- | --- | ||

variant decrease | --- | 0.01 | --- | --- | ||

precondition | --- | 0.01 | --- | --- | ||

precondition | --- | 0.01 | --- | --- | ||

precondition | --- | 0.02 | --- | --- | ||

variant decrease | --- | 0.01 | --- | --- | ||

precondition | --- | 0.01 | --- | --- | ||

precondition | --- | 0.01 | --- | --- | ||

precondition | --- | 0.02 | --- | --- | ||

precondition | --- | 0.01 | --- | --- | ||

unreachable point | --- | 0.00 | --- | --- | ||

postcondition | --- | 6.36 | --- | 0.38 | ||

postcondition | --- | 0.08 | --- | --- | ||

postcondition | --- | 0.25 | --- | --- | ||

postcondition | --- | 0.16 | --- | --- | ||

postcondition | --- | 0.02 | --- | --- | ||

VC for merge | --- | --- | --- | --- | ||

split_goal_right | ||||||

variant decrease | --- | 0.01 | --- | --- | ||

precondition | --- | 0.00 | --- | --- | ||

precondition | --- | 0.01 | --- | --- | ||

precondition | --- | 0.02 | --- | --- | ||

precondition | --- | 0.00 | --- | --- | ||

precondition | --- | 0.00 | --- | --- | ||

precondition | --- | 0.01 | --- | --- | ||

precondition | --- | 0.01 | --- | --- | ||

precondition | --- | 0.00 | --- | --- | ||

precondition | --- | 0.01 | --- | --- | ||

unreachable point | --- | 0.00 | --- | --- | ||

postcondition | --- | --- | --- | 0.46 | ||

postcondition | --- | 0.21 | --- | --- | ||

postcondition | --- | 0.42 | --- | --- | ||

postcondition | --- | 0.24 | --- | --- | ||

VC for remove_min | --- | 0.03 | --- | --- | ||

VC for diff | --- | 0.55 | --- | --- | ||

VC for fast_size | --- | 0.02 | --- | --- | ||

VC for size_height | --- | 0.12 | --- | --- | ||

VC for inv_height | --- | --- | --- | --- | ||

split_goal_right | ||||||

assertion | --- | 0.06 | --- | --- | ||

variant decrease | --- | 0.01 | --- | --- | ||

precondition | --- | 0.01 | --- | --- | ||

variant decrease | --- | 0.01 | --- | --- | ||

precondition | --- | 0.01 | --- | --- | ||

postcondition | --- | --- | 0.07 | --- |