Posons :
\begin{center}
$P$ : \og $p=2^i$ \fg{}
\end{center}
\begin{itemize}
\item avant d'entrer dans la boucle itérative, $p=1=2^0=2^n$, donc  la propriété $P$ est vraie.
\item Notons $p_1$ et $i_1$ les valeurs de \texttt{p} et \texttt{i} lors d'une itération. Notons $p_2$ et $i_2$ les valeurs de ces mêmes variables à l'itération suivante. Alors:
\[
i_2=i_1+1\qquad\text{et}\qquad p_2=2\times p_1=2\times2^{i_1}=2^{i_1+1}=2^{i_2}.
\]
La propriété $P$ est donc vraie, ce qui montre que $P$ est un invariant de la boucle itérative.

Quand la boucle est finie, $i=n$ et $P$ est vraie, donc $p=2^n$.

L'algorithme permet donc de calculer la puissance de 2 lorsque l'exposant est égal à un entier $n$.
\end{itemize}
\newpage
