The ProVal team was stopped at the end of August 2012, and reborn into a new team
Toccata
These pages do not evolve anymore, please follow the link above for up-to-date informations about our team.
Traversing a tree inorder, filling an array
From Rustan Leino's tutorial on Dafny at VSTTE 2012
Authors: Jean-Christophe Filliâtre
Tools: Why3
(* From Rustan Leino's tutorial on Dafny at VSTTE 2012 *) 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 (* the size of a tree, to prove termination *) function size (t: tree) : int = match t with | Null -> 0 | Node l _ r -> size l + size r + 1 end lemma size_nonneg: forall t: tree. size t >= 0 let rec fill (t: tree) (a: array elt) (start: int) : int variant { size t } 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] } = 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