(** {1 MPRI lecture 2-36-1 "Proof of Programs"} *)

(** {2 Factorial: recursive specification, iterative implementation} *)

use int.Int

let rec function fact (n:int) : int
  requires { n >= 0 }
  variant { n }
= if n=0 then 1 else n * fact (n-1)


let fact_imp (x:int) : int
    requires { x >= 0 }
    ensures { result = fact x }
  = let ref y = 0 in
    let ref res = 1 in
    while y < x do
      invariant { 0 <= y <= x }
      invariant { res = fact y }
      variant { x - y }
      y <- y + 1;
      res <- res * y
    done;
    res


(*
Local Variables:
compile-command: "why3 ide fact_sol.mlw"
End:
*)