## Build a balanced tree from a list

Build a tree of logarithmic height from a list, in linear time, while preserving the order of elements

Authors: Jean-Christophe Filliâtre

Topics: Data Structures

Tools: Why3

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

Build a tree of logarithmic height from a list, in linear time, while preserving the order of elements

Author: Jean-Christophe FilliĆ¢tre (CNRS)

module TreeOfList

use int.Int
use int.ComputerDivision
use int.Power
use list.List
use list.Append
use list.Length
use bintree.Tree
use bintree.Size
use bintree.Inorder
use bintree.InorderLength
use bintree.Height

type elt

let rec tree_of_list_aux (n: int) (l: list elt) : (tree elt, list elt)
requires { 0 <= n <= length l }
variant  { n }
ensures  { let t, l' = result in
inorder t ++ l' = l && size t = n &&
(n > 0 -> let h = height t in power 2 (h-1) <= n < power 2 h) }
=
if n = 0 then
Empty, l
else
let n = n - 1 in
let n1 = div n 2 in
let left, l = tree_of_list_aux n1 l in
match l with
| Nil -> absurd
| Cons x l -> let right, l = tree_of_list_aux (n - n1) l in
Node left x right, l
end

let tree_of_list (l: list elt) : tree elt
ensures { inorder result = l }
ensures { size result > 0 -> let h = height result in
power 2 (h-1) <= size result < power 2 h }
=
let t, l = tree_of_list_aux (length l) l in
assert { l = Nil };
t

end

download ZIP archive

# Why3 Proof Results for Project "tree_of_list"

## Theory "tree_of_list.TreeOfList": fully verified

 Obligations Alt-Ergo 2.4.2 CVC4 1.6 CVC5 1.0.5 VC for tree_of_list_aux --- --- --- split_vc precondition --- --- 0.04 variant decrease --- --- 0.05 precondition --- --- 0.05 unreachable point --- --- 0.07 variant decrease --- --- 0.07 precondition --- --- 0.07 postcondition --- --- --- split_vc postcondition --- --- 0.18 postcondition --- --- 0.09 postcondition --- --- 0.39 postcondition --- --- --- split_vc postcondition --- --- 0.04 postcondition --- --- --- split_vc postcondition 0.37 --- --- VC for tree_of_list --- 0.08 ---