(* (Exercise borrowed from Rustan Leino's Dafny tutorial at VSTTE 2012)

   Function "fill" below stores the elements of tree "t" in array "a",
   according to some inorder traversal, starting at array index "start",
   as long as there is room in the array. It returns the array position
   immediately right of the last element of "t" stored in "a".

   Questions:

   1. Prove safety i.e. the absence of array access out of bounds.
      (You have to strengthen the precondition.)

   2. Show that, after the execution of "fill", the elements in
      a[0..start[ have not been modified.

   3. Show that, after the execution of "fill", the elements in
      a[start..result[ belong to tree "t" (using predicate
      "contains" below).

   4. Prove termination of function "fill".

*)

module Fill

  use import int.Int
  use import array.Array

  type elt
  type tree = Null | Node tree elt tree

  predicate contains (t: tree) (x: elt) = match t with
    | Null       -> false
    | Node l y r -> contains l x || x = y || contains r x
  end

  let rec fill (t: tree) (a: array elt) (start: int) : int
    requires { 0 <= length a }
    ensures  { true }
  =
    match t with
    | Null ->
        start
    | Node l x r ->
        let res = fill l a start in
        if res <> length a then begin
          a[res] <- x;
          fill r a (res + 1)
        end else
          res
     end

end