Bonjour, je suis étudiant en première année de licence informatique, et j'ai un problème afin de résoudre un exercice. Voici mon problème ..
 
Le but est d'établir la preuve d'un programme pascal, un algorithme de calcul de la factorielle d'un naturel.
 
l'assertion P est :
 
k <= n
n et la valeur de k sont de meme parité
q = (k-1)k
f = k!
 
la condition C est :
 
k < n
 
Et I l'instruction :
 
begin
q := q + 4*k +2
f := f*q
k := k+2
end
 
La question est : "Quelles valeurs donner aux variables k,q et f avant l'execution de la boucle pour qu'à la terminaison de celle-ci la valeur de la variable f soit n!"
 
J'ai essayé de partir de l'état final ( f = n!, d'ou k =n .. ), mais je n'arrive pas à avancer ..
 
Merci d'avance de votre aide.

Si tu prend k = n mod 2, f = 1, et q = 0, ca marche.
Fait le "à la main" pour des petites valeurs de n pour comprendre.

Je comprends pour k = n mod 2, mais pas pour f = 1 et q =0 .. quant aux tests pour des petites valeurs de n, je ne vois même pas ou je dois remplacer sa valeur ..

exemple pour n = 0:0! = 1
 
k = n mod 2 = 0;
f = 1;
q = 0;
la condition k < n est fausse, donc la boucle n'est pas executée.
résultat: f = 1 = 1!
 
exemple pour n = 3:3! = 6
 
k = n mod 2 = 1;
f = 1;
q = 0;
la condition k < n est vraie, donc boucle est executée:
q := q + 4*k +2 = 6;
f := f * q = 6;
k := k+2 = 3;
 
la condition k < n est fausse, donc boucle s'arrête.
résultat: f = 6 = 3!
 
Et ainsi de suite...
Pour la preuve, une preuve par récurrence semble bien adaptée.

Merci beaucoup ryujakk pour ces réponses. Je comprend à présent. Au plaisir