Wiki Agenda Contact Version française

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

ObligationsAlt-Ergo 2.2.0CVC4 1.6Eprover 2.0
VC tree_of_array_aux---------
split_vc
VC tree_of_array_aux.0---0.03---
VC tree_of_array_aux.1---0.07---
VC tree_of_array_aux.2---0.06---
VC tree_of_array_aux.3---0.04---
VC tree_of_array_aux.4---0.10---
VC tree_of_array_aux.5---0.07---
VC tree_of_array_aux.6---------
split_all_full
VC tree_of_array_aux.6.00.02------
VC tree_of_array_aux.6.1---------
split_all_full
VC tree_of_array_aux.6.1.01.27------
VC tree_of_array_aux.6.2---------
case hi=lo
VC tree_of_array_aux.6.2.0---0.04---
VC tree_of_array_aux.6.2.1---------
case hi=lo+1
VC tree_of_array_aux.6.2.1.0---------
split_all_full
VC tree_of_array_aux.6.2.1.0.0------2.07
VC tree_of_array_aux.6.2.1.1---------
split_all_full
VC tree_of_array_aux.6.2.1.1.01.09------
VC tree_of_array_aux.6.3---------
case hi=lo
VC tree_of_array_aux.6.3.0---0.04---
VC tree_of_array_aux.6.3.1---------
case hi=lo+1
VC tree_of_array_aux.6.3.1.0---------
assert left=Empty
VC tree_of_array_aux.6.3.1.0.0---0.08---
VC tree_of_array_aux.6.3.1.0.1---------
assert right=Empty
VC tree_of_array_aux.6.3.1.0.1.0---0.06---
VC tree_of_array_aux.6.3.1.0.1.10.03------
VC tree_of_array_aux.6.3.1.1---------
split_all_full
VC tree_of_array_aux.6.3.1.1.01.83------
VC tree_of_array---0.04---