(* (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
(*
Local Variables:
compile-command: "why3 ide exo_fill.mlw"
End:
*)