## Tree of array

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

**Authors:** Jean-Christophe Filliâtre

**Topics:** Array Data Structure / Trees / Algorithms

**Tools:** Why3

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

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

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

module TreeOfArray use int.Int use int.ComputerDivision use int.Power use array.Array use array.ToList use bintree.Tree use bintree.Size use bintree.Inorder use bintree.Height let rec tree_of_array_aux (a: array 'a) (lo hi: int) : tree 'a requires { 0 <= lo <= hi <= length a } variant { hi - lo } ensures { let n = hi - lo in size result = n && inorder result = to_list a lo hi && (n > 0 -> let h = height result in power 2 (h-1) <= n < power 2 h) } = if hi = lo then Empty else let mid = lo + div (hi - lo) 2 in let left = tree_of_array_aux a lo mid in let right = tree_of_array_aux a (mid+1) hi in Node left a[mid] right let tree_of_array (a: array 'a) : tree 'a ensures { inorder result = to_list a 0 (length a) } ensures { size result > 0 -> let h = height result in power 2 (h-1) <= size result < power 2 h } = tree_of_array_aux a 0 (length a) end

download ZIP archive

# Why3 Proof Results for Project "tree_of_array"

## Theory "tree_of_array.TreeOfArray": fully verified

Obligations | Alt-Ergo 2.2.0 | Alt-Ergo 2.4.1 | CVC4 1.6 | ||||||

VC for tree_of_array_aux | --- | --- | --- | ||||||

split_vc | |||||||||

precondition | --- | --- | 0.03 | ||||||

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

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

variant decrease | --- | --- | 0.04 | ||||||

precondition | --- | --- | 0.10 | ||||||

index in array bounds | --- | --- | 0.07 | ||||||

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

split_all_full | |||||||||

VC for tree_of_array_aux | 0.02 | --- | --- | ||||||

VC for tree_of_array_aux | --- | --- | --- | ||||||

split_all_full | |||||||||

VC for tree_of_array_aux | 0.31 | --- | --- | ||||||

VC for tree_of_array_aux | --- | --- | --- | ||||||

case hi=lo | |||||||||

true case | --- | --- | 0.04 | ||||||

false case | --- | --- | --- | ||||||

case hi=lo+1 | |||||||||

false case (true case) | --- | --- | --- | ||||||

split_all_full | |||||||||

false case (true case) | --- | 0.32 | --- | ||||||

false case | --- | --- | --- | ||||||

split_all_full | |||||||||

false case | 0.81 | --- | --- | ||||||

VC for tree_of_array_aux | --- | --- | --- | ||||||

case hi=lo | |||||||||

true case | --- | --- | 0.04 | ||||||

false case | --- | --- | --- | ||||||

case hi=lo+1 | |||||||||

false case (true case) | --- | --- | --- | ||||||

assert left=Empty | |||||||||

asserted formula | --- | --- | 0.08 | ||||||

false case (true case) | --- | --- | --- | ||||||

assert right=Empty | |||||||||

asserted formula | --- | --- | 0.06 | ||||||

false case (true case) | 0.03 | --- | --- | ||||||

false case | --- | --- | --- | ||||||

split_all_full | |||||||||

false case | 2.48 | --- | --- | ||||||

VC for tree_of_array | --- | --- | 0.04 |