problemdata       % Takes 5 *mandatory* arguments
        {computational-processes-3}             % latex-friendly label for the prob.
        {computational-processes}  % The topic(s) of the problem content.
        {}               % Source (if known)
        {S02 PS5} % Usage (list ones you are aware of).
        {Jack Kwok, S02}        % Last revision info (author, date).

\begin{problem}
\textbf{Extended GCD} We have already proved in two different ways that
the gcd of two natural numbers can be expressed as an integer linear
combination of them.  The following procedure extends the Euclidean GCD to
explicitly calculate the desired integer coefficients.

In particular, given natural numbers $m,n$, with $n>0$, we claim the
following procedure halts with integers $K,L$ in registers \texttt{K} and
\texttt{L} such that
\[
Km+Ln=\mbox{gcd}(m,n).
\]
(This procedure and its invariants are taken from Aho, Hopcroft, and
Ullman's text on algorithms.)

Inputs: $m,n \in \naturals, n>0$.

Registers: \texttt{X,Y,K,L,U,V,Q}.

\begin{verbatim}
X := m; Y := n; K := 0; L := 1; U := 1; V := 0; 
loop:
if Y|X, then halt
else
 Q := floor(X/Y);      ;; same as Q:= quotient of X divided by Y
 {X := Y,              ;; assignments within the braces are SIMULTANEOUS
  Y := X - Q * Y,      ;; same as Y:= remainder of X divided by Y
  U := K,
  V := L,
  K := U - Q * K,
  L := V - Q * L}     ;; assignments within the braces are SIMULTANEOUS
goto loop
\end{verbatim}

Note that \texttt{X,Y} behave exactly as in the Euclidean GCD algorithm
from lecture, except that this procedure stops one step sooner, ensuring
that $\mbox{gcd}(m,n)$ is in \texttt{Y} at the end.

\bparts

\ppart Prove that this procedure terminates for all inputs $m,n$.

\solution{It terminates for the same reason as the Euclidean algorithm:
the contents, $Y$, of register \texttt{Y} is a natural number-valued
variable that strictly decreases each time around the loop.}

\ppart We claim that invariant properties that can be used to prove partial
correctness are:
\begin{itemize}
\item %\label{gcd}
(a)  $\mbox{gcd}(X,Y) = \mbox{gcd}(m,n)$,
\item % \label{kl}
(b) $Km+ Ln = Y$, and
\item % \label{uv}
(c) $Um+Vn = X$.
\end{itemize}

Prove that (a), (b) and (c) are ``loop'' invariants, that is, if they are
true at the start of the loop, they are true at the start of the next
loop.

\solution{Invariant (a) is the same one as for the Euclidean algorithm, which
we proved in lecture.  To check the other two invariants, note that at the
start $X=m, Y=n, K=0, L=1$ so $Km+Ln=0m+1n=n=Y$ as required; also $U=1, V=0$
and $Um+Vn= 1m+0n=m =X$ as required.

So let $x,y,k,l,u,v$ be the contents of registers \texttt{X,Y,K,L,U,V} at
the start of the loop and assume that all the invariants hold for these
values.  We must prove that (b) and (c) hold (we already know (a) does)
for the new contents $x',y',k',l',u',v'$ of these registers at the next
time the loop is started.

Now according to the procedure, $u'=k,v'=l,x'=y$, so invariant (c) holds
for $u',v',x'$ because of invariant (b) for $k,l,y$.  Also, $k'= u - qk,
l'= v - ql, y' = x - qy$ where $q = \floor{x/y}$, so
\[k'm+l'n = (u-qk)m + (v-ql)n =um+vn - q(km+ln) = x - qy = y',\]
and therefore invariant (b) holds for $k',l',y'$.
}

\ppart Prove that at termination, \texttt{Y} contains $\mbox{gcd}(m,n)$
and \texttt{K} and \texttt{L} contains integers $K$ and $L$ such that
\[
\mbox{gcd}(m,n) = Km+Ln.
\]

\solution{It's easy to check that all three invariant are true at the
start of the first time around the loop.  So they are true at termination.
At termination the contents, $Y$, of register \texttt{Y} divides the
contents, $X$, of register \texttt{X}, so invariants (a) and (b) imply
\[
\mbox{gcd}(m,n) = \mbox{gcd}(X,Y) = Y = Km + Ln.
\]
So we have the gcd in register \texttt{Y} and the desired coefficients in
\texttt{K}, \texttt{L}.}

\eparts
\end{problem}
