Invariant de boucle entrée/sortie
Bonjour,
Je dois prouver mon programme big_fermat :
Code:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
| let big_fermat n =
if n egale deux then [| un ; deux |] else
let x = ref ((deux fois (racine n)) plus un)
and r = ref (((racine n) fois (racine n)) moins n)
and y = ref un in
while not (!r egale zero) do begin
if !r superieur_a zero then
begin
r := !r moins !y;
y := !y plus deux;
end
else if !r inferieur_a zero then
begin
r := !r plus !x;
x := !x plus deux;
end
else () end done;
let aux1 = ((!x moins !y) divisé_par deux)
and aux2 = ((!x plus !y moins deux) divisé_par deux) in
[|aux1; aux2|];; |
Je dois donc trouver les invariants de boucles en entrée et en sortie, mais la je ne vois pas trop ...
Est ce que quelqu'un pourrait m'aider ?
PS : je travaille en big_int ,sur caml light, et j'ai redefini toutes les fonctions prédéfinies sur caml light pour rendre le programme plus clair.
Ex : J'ai defini racine comme sqrt_big_int.
Merci d'avance !