examples/fill.mlw

   1
   2 (* Traversing a tree inorder, filling an array with the elements
   3    (from Rustan Leino's tutorial on Dafny at VSTTE 2012)
   4
   5    Author: Jean-Christophe Filliatre (CNRS)
   6 *)
   7
   8 module Fill
   9
  10   use int.Int
  11   use array.Array
  12
  13   type elt
  14   type tree = Null | Node tree elt tree
  15
  16   predicate contains (t: tree) (x: elt) = match t with
  17     | Null       -> false
  18     | Node l y r -> contains l x || x = y || contains r x
  19   end
  20
  21   let rec fill (t: tree) (a: array elt) (start: int) : int
  22     requires { 0 <= start <= length a }
  23     ensures  { start <= result <= length a }
  24     ensures  { forall i: int. 0 <= i < start -> a[i] = (old a)[i] }
  25     ensures  { forall i: int. start <= i < result -> contains t a[i] }
  26     variant  { t }
  27   = match t with
  28     | Null ->
  29         start
  30     | Node l x r ->
  31         let res = fill l a start in
  32         if res <> length a then begin
  33           a[res] <- x;
  34           fill r a (res + 1)
  35         end else
  36           res
  37      end
  38
  39 end