\begin{questions}
\item La variable \texttt{i} vaut initialement 0. À chaque itération, elle est incrémentée. Or, \texttt{n} est constante donc  il existe une itération à partir de laquelle\linebreak\texttt{i = n}, ce qui aura pour conséquence la fin de la boucle.

\item On suppose ici que \texttt{n$\geqslant$0}.
\begin{itemize}
\item Avant d'entrer dans la boucle, \texttt{i=0} et \texttt{f=1=0!=i!} (par convention). De plus, \texttt{i} est bien inférieure ou égale à \texttt{n}, puisque les deux variables valent le même nombre.

Ainsi, la propriété $P$ est vraie avant de rentrer dans la boucle.

\item Notons \texttt{i1}, \texttt{f1} les valeurs de \texttt{i} et \texttt{f} lors d'une certaine étape, et supposons $P$ vraie à cette étape. Donc \texttt{f1 = (i1)!} et \texttt{i1 < n}.

Notons \texttt{i2} et \texttt{f2} les valeurs de ces mêmes variables après l'exécution des instructions de la boucle. On a ainsi :
\begin{center}
\texttt{i2 = i1+1 $\leqslant$ n}
\end{center}
et
\begin{center}
\texttt{f2 = f1*(i1+1) = (i1!)*(i1+1) = (i1+1)!}.
\end{center}
Ainsi, $P$ est vraie après exécution de la boucle, donc $P$ est un invariant de la boucle.

\item À la sortie de la boucle, on a \texttt{i $\geqslant$ n} (négation de la condition), et $P$ est vraie (donc \texttt{f=i!} et \texttt{i$\leqslant$n}). Donc \texttt{i = n}, d'où \texttt{f = n!}, qui est une bonne post-condition pour prouver la correction de l'algorithme.
\end{itemize}
\end{questions}
\newpage
