Preuve par invariant et complexité

• Invariant de boucle : Proposons la propriété $\mathcal{P}(i)$ suivante : à l'entrée de la boucle while, la variable $f$ stocke le produit des entiers de 1 à $i-1$, c'est-à-dire : $$f=(i-1)!$$

• Preuve de correction :

• Initialisation : Avant la première itération, $i=1$ et $f=1$. L'invariant donne $1=(1-1)!=0!=1$, ce qui est vrai.

• Conservation : Supposons l'invariant vrai à l'entrée de la boucle pour une valeur de $i\le n$. Durant l'itération, les variables sont mises à jour : $$f_{\text{nouveau}}=f\times i=(i-1)!\times i=i!$$ $$i_{\text{nouveau}}=i+1$$ À la fin de la boucle, nous avons bien : $$f_{\text{nouveau}}=(i_{\text{nouveau}}-1)!$$ L'invariant est conservé.

• Terminaison et Correction totale : La variable $i$ est initialisée à 1 et est incrémentée de 1 à chaque tour. Comme $n$ est constant, la condition de boucle $i\le n$ finira par devenir fausse (quand $i=n+1$), ce qui assure la terminaison de la boucle. À la terminaison de la boucle, on a $i=n+1$. D'après l'invariant : $$f=(i-1)!=(n+1-1)!=n!$$ La fonction retourne $f$, soit exactement $n!$. L'algorithme est correct.

Complexités :

• Temporelle : La boucle effectue $n$ itérations. Chaque itération réalise un nombre constant d'instructions élémentaires. La complexité temporelle est : $\Theta (n)$.

• Spatiale : Seules deux variables de travail (i et f) sont utilisées en mémoire. La complexité spatiale supplémentaire est : $\Theta (1)$ (constante).