(* Two programs to compute the factorial.

   Note: function "fact" from module int.Fact (already imported)
   can be used in specifications.

   Questions :

   1. In module FactRecursive:

      a. Prove soundness of function fact_rec.

      b. Prove its termination.

   2. In module FactLoop

      a. Prove soundness of function fact_loop

      b. Prove its termination

      c. Change the code to use a for loop instead of a while loop.

*)

module FactRecursive

  use import int.Int
  use import int.Fact

  let rec fact_rec (n: int) : int
    requires { true }
    ensures  { result = fact n }
  =
    if n = 0 then 1 else n * fact_rec (n - 1)

end

module FactLoop

  use import int.Int
  use import int.Fact
  use import ref.Ref

  let fact_loop (n: int) : int
    requires { true }
    ensures  { result = fact n }
  = let m = ref 0 in
    let r = ref 1 in
    while !m < n do
      invariant { true }
      m := !m + 1;
      r := !r * !m
    done;
    !r

end