Posons :
\begin{center}
$P$ : \og $z\times x^k = b^n$ et $k\geqslant0$ \fg.
\end{center}
\begin{itemize}
\item Avant d'entrer dans la boucle, $z\times x^k=1\times b^n=b^n$ et $k=n$ donc $k\geqslant n$.

$P$ est donc vraie.

\item Posons $z_1$, $x_1$ et $k_1$ les valeurs respectives de \texttt{z}, \texttt{x} et \texttt{k} lors d'une itération où $P$ est vraie. Alors,
\[
z_1\times x_1^{k_1}=b^n\qquad\text{et}\qquad k_1>0.
\]
($k_1\neq0$ car il faut qu'il y ait une autre itération)

À l'étape suivante, notons $z_2$, $x_2$ et $k_2$ les valeurs des mêmes variables. Alors,
\begin{itemize}
\item[--] si $k_1$ est impair ($k_1=2p_1+1$):
\[
z_2=z_1\times x_1
\]
et
\[
x_2=x_1 \times x_1\qquad\text{et}\qquad k_2=E(k_1/2)=p_1.
\]
Dans ce cas,
\[
z_2 \times x_2^{k_2} = \underbrace{z_1 \times x_1}_{=z_2} \times \big(x_1^2\big)^{p_1}=z_1 \times x_1 \times x_1^{2p_1}=z_1 \times x_1\times x_1^{k_1-1}=\underbrace{z_1\times x_1^{k_1}}_{=b^n}.
\]
\item[--] Si $k_1$ est pair ($k_1=2p_1$):
\[
x_2=x_1 \times x_1\qquad\text{et}\qquad k_2=E(k_1/2)=p_1.
\]
Dans ce cas,
\[
z_2 \times x_2^{k_2} = z_1 \times \big(x_1^2\big)^{p_1} = z_1 \times x_1^{2p_1} = z_1 \times x_1^{k_1}=b^n.
\]
\end{itemize}
Dans les deux cas, $P$ est vraie.
\end{itemize}
Donc $P$ est bien un invariant de la boucle.

\Par

Quand la boucle se termine, $k=0$ et $P$ est vraie, donc $z\times x^0=b^n$, soit $z=b^n$.

L'algorithme calcule donc $b$ à l'exposant $n$.
