## 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.2.0 | CVC4 1.6 | ||

VC tree_of_list_aux | --- | --- | ||

split_vc | ||||

VC tree_of_list_aux.0 | --- | 0.02 | ||

VC tree_of_list_aux.1 | --- | 0.07 | ||

VC tree_of_list_aux.2 | --- | 0.05 | ||

VC tree_of_list_aux.3 | --- | 0.05 | ||

VC tree_of_list_aux.4 | --- | 0.05 | ||

VC tree_of_list_aux.5 | 0.01 | --- | ||

VC tree_of_list_aux.6 | --- | --- | ||

destruct_alg_subst l'1 | ||||

VC tree_of_list_aux.6.0 | --- | 0.04 | ||

VC tree_of_list_aux.6.1 | --- | 0.22 | ||

VC tree_of_list | --- | 0.08 |