(* (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 both the precondition and the
postcondition.)
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". You have to give predicate
"contains" below a suitable definition.
4. Prove termination of function "fill".
*)
use int.Int
use array.Array
type elt
type tree = Null | Node tree elt tree
(* element x belongs to tree t *)
predicate contains (t: tree) (x: elt) =
false (* to be updated at step 3 *)
let rec fill (t: tree) (a: array elt) (start: int) : int
requires { 0 <= length a }
diverges
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