Wiki Agenda Contact Version française

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

ObligationsAlt-Ergo 2.4.2CVC4 1.6CVC5 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
postcondition0.37------
VC for tree_of_list---0.08---