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 import int.Int
  use import int.ComputerDivision
  use import int.Power
  use import list.List
  use import list.Append
  use import list.Length
  use import bintree.Tree
  use import bintree.Size
  use import bintree.Inorder
  use import bintree.InorderLength
  use import 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 in 0.41 s

ObligationsAlt-Ergo (0.99.1)CVC4 (1.4)
VC for tree_of_list_aux------
split_goal_wp
  1. postcondition---0.12
2. variant decrease0.02---
3. precondition0.03---
4. unreachable point0.01---
5. variant decrease0.01---
6. precondition0.01---
7. postcondition------
split_goal_wp
  1. postcondition0.00---
2. postcondition0.02---
3. postcondition---0.09
4. postcondition---0.08
VC for tree_of_list0.02---