fill.mlw 954 Bytes
Newer Older
1

2 3 4 5 6
(* Traversing a tree inorder, filling an array with the elements
   (from Rustan Leino's tutorial on Dafny at VSTTE 2012)

   Author: Jean-Christophe Filliatre (CNRS)
*)
7 8 9

module Fill

10 11
  use int.Int
  use array.Array
12

13 14
  type elt
  type tree = Null | Node tree elt tree
15

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

21
  let rec fill (t: tree) (a: array elt) (start: int) : int
22 23 24 25
    requires { 0 <= start <= length a }
    ensures  { start <= result <= length a }
    ensures  { forall i: int. 0 <= i < start -> a[i] = (old a)[i] }
    ensures  { forall i: int. start <= i < result -> contains t a[i] }
26
    variant  { t }
27
  = match t with
28 29 30 31 32 33 34 35 36 37 38 39
    | 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