38 lines
776 B
Plaintext
Executable file
38 lines
776 B
Plaintext
Executable file
(* 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
|