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 |