\begin{questions}
\item \texttt{r} représente le reste de la division euclidienne de $a$ par $b$, donc\linebreak$0\leqslant r <b$ par définition mathématique. Or, \texttt{b}  devient \texttt{r} à chaque itération, donc \texttt{r} diminue à chaque itération. Comme \texttt{r} est un entier naturel, il existe une itération pour laquelle \texttt{r=0}, donc pour laquelle \texttt{b=0}, ce qui assure une sortie de la boucle.

\item Pré-condition : $y\geqslant0$. Considérons l'algorithme complété suivant:

\begin{algorithme}{}
a $>$ b deux entiers
x $\leftarrow$ a
y $\leftarrow$ b
r entier
Tant que b $>$ 0:
\quad r $\leftarrow$ a\%b
\quad a $\leftarrow$ b
\quad b $\leftarrow$ r
Fin du Tant que
\end{algorithme}

\Par

Posons alors:
\begin{center}
$P$ : \og $\text{pgcd}(a,b)=\text{pgcd}(x,y)$ et $b\geqslant0$. \fg{}
\end{center}
\begin{itemize}
\item Avant l'entrée dans la boucle, $P$ est vraie.
\item Notons \texttt{a1}, \texttt{b1} et \texttt{r1} les valeurs de \texttt{a}, \texttt{b} et \texttt{r} à une certaine étape.

Supposons que $P$ est vraie à cette étape; donc $\text{pgcd}(\texttt{a1},\texttt{b1})=\text{pgcd}(\texttt{x},\texttt{y})$ et $\texttt{b1}\geqslant0$.

Notons \texttt{a2}, \texttt{b2} et \texttt{r2} les valeurs de \texttt{a}, \texttt{b} et \texttt{r} lors de l'itération suivante.

Alors, \texttt{r2 = a1\%b1}, \texttt{a2=b1} et \texttt{b2=r2}.

D'après la propriété mathématique rappelée en énoncé,
\begin{center}
pgcd(\texttt{a2},\texttt{b2}) = pgcd(\texttt{b1},\texttt{r2}) = pgcd(\texttt{a1},\texttt{a2}) = pgcd(\texttt{x},\texttt{y}).
\end{center}
De plus, \texttt{b2 $\geqslant$ 0} car \texttt{r2 $\geqslant$ 0}.

Ainsi, la propriété $P$ est vraie à cette étape; c'est donc un invariant de la boucle \og Tant que \fg.
\end{itemize}

La post-condition qui découle de ceci est que $\PGCD(\texttt{x},0)=\PGCD(\texttt{a},\texttt{b})$, et donc $x=\PGCD(a,b)$.
\end{questions}
\newpage
