use int.Int type list 'a = Nil | Cons 'a (list 'a) function append (l1:list 'a) (l2:list 'a) : list 'a = match l1 with | Nil -> l2 | Cons x l -> Cons x (append l l2) end let rec lemma append_nil (l:list 'a) : unit ensures { append l Nil = l } = match l with | Nil -> () | Cons _ r -> append_nil r end let rec lemma append_assoc ( l1 l2 l3:list 'a) : unit ensures { append (append l1 l2) l3 = append l1 (append l2 l3) } = match l1 with | Nil -> () | Cons _ r -> append_assoc r l2 l3 end function length (l:list 'a) : int = match l with | Nil -> 0 | Cons _ r -> 1 + length r end (* lemma length_nonneg: forall l:list 'a. length l >= 0 *) function rev (l:list 'a) : list 'a = match l with | Nil -> Nil | Cons x r -> append (rev r) (Cons x Nil) end val ref l : list int let rec rev_append (r:list int) : unit variant { r } writes { l } ensures { l = append (rev r) (old l) } = match r with | Nil -> () | Cons x r -> l <- Cons x l; rev_append r end let reverse (r:list int) : unit writes { l } ensures { l = rev r } = l <- Nil; rev_append r (* Local Variables: compile-command: "why3 ide rev.mlw" End: *)