(* Spécification de la fonction factorielle *)

theory Factorielle

   use int.Int

   function factorielle( n : int ) : int

   axiom factorielle_zero : (factorielle zero) = one

   axiom factorielle_succ : forall n : int. (n > 0) -> (factorielle n) = (n * (factorielle (n - 1)))

end

(* Implémentation de la fonction factorielle par un algorithme descendant *)

module FactorielleDescendant

  use int.Int
  use Factorielle
  use ref.Refint

  let factorielle_descendant (n: int) : int
    requires { 0 <= n }
    ensures  { result = (factorielle n) }
  =
    let i = ref n in
    let r = ref 1 in
    while  (0 < !i) do
      invariant { !r * factorielle !i = factorielle n && 0 <= !i }
      variant   { !i }
      r := !i * !r;
      i := !i - 1
    done;
    !r

end