examples/tree_of_array.mlw

   1
   2 (** Build a tree of logarithmic height from an array, in linear time,
   3     while preserving the order of elements
   4
   5     Author: Jean-Christophe Filliâtre (CNRS)
   6 *)
   7
   8 module TreeOfArray
   9
  10   use int.Int
  11   use int.ComputerDivision
  12   use int.Power
  13   use array.Array
  14   use array.ToList
  15   use bintree.Tree
  16   use bintree.Size
  17   use bintree.Inorder
  18   use bintree.Height
  19
  20   let rec tree_of_array_aux (a: array 'a) (lo hi: int) : tree 'a
  21     requires { 0 <= lo <= hi <= length a }
  22     variant  { hi - lo }
  23     ensures  { let n = hi - lo in
  24                size result = n && inorder result = to_list a lo hi &&
  25                (n > 0 ->
  26                   let h = height result in power 2 (h-1) <= n < power 2 h) }
  27   =
  28     if hi = lo then
  29       Empty
  30     else
  31       let mid = lo + div (hi - lo) 2 in
  32       let left = tree_of_array_aux a lo mid in
  33       let right = tree_of_array_aux a (mid+1) hi in
  34       Node left a[mid] right
  35
  36   let tree_of_array (a: array 'a) : tree 'a
  37     ensures { inorder result = to_list a 0 (length a) }
  38     ensures { size result > 0 -> let h = height result in
  39                 power 2 (h-1) <= size result < power 2 h }
  40   =
  41     tree_of_array_aux a 0 (length a)
  42
  43 end