\problemdata                                                             
        {Multiplication algorithm} % latex-friendly label for the prob.
        {Algorithms, State Machine} % The topic(s) of the problem content.  
        {?} % Source (if known)                                          
        {S01 Tutorial 5, 3} % Usage (list ones you are aware of). 
        {Tina Wang, S02} % Last revision info (author, date).   
                                                                         
                                                                         
\begin{problem}           
Suppose that the following procedure is used to multiply two
non-negative integers $a$ and $b$.

\centerline{
\begin{minipage}{0 in}
\medskip
\begin{tabbing}
xxx \= xxx \= xxx \= xxx \= xxx \= xxx \= \kill
Let $x = a$, $y = b$, $p = 0$. \\
Repeat the following steps. \\
\> If $x = 0$, then output $p$ and terminate. \\
\> Otherwise, if $x$ is even, then let $x = x/2$ and $y = 2y$. \\
\> Otherwise, if $x$ is odd, then let $x = x - 1$ and $p = p + y$.
\end{tabbing}
\medskip
\end{minipage}}

\begin{problemparts}

\problempart Model the procedure with a state machine.

\solution{The set of states $Q$ consists of quintuples $(a, b, x, y,
p)$ where all variables are non-negative integers.  The set of start
states $Q_0$ consists of the single state $(a, b, a, b, 0)$.  The set
of transitions $\delta$ consists of transitions of the form $(a, b, x,
y, p) \rightarrow (a, b, x', y', p')$ where one of the following two
sets of conditions holds:

\begin{enumerate}
\item $x$ is even and positive, $x' = x/2$, $y' = 2y$, and $p' = p$.
\item $x$ is odd, $x' = x - 1$, $y' = y$, and $p' = p + y$.
\end{enumerate}
}

\problempart Formulate an invariant relating $a$, $b$, $x$, $y$, and
$p$ that holds at the top of the loop.  Your invariant should imply
that when $x = 0$, $p = ab$.

\solution{
\[
xy + p = ab
\]
}

\problempart Prove that the invariant holds.

\solution{ The invariant holds initially, because $x = a$, $y = b$,
and $p = 0$.  Suppose that the invariant holds in state $(a, b, x, y,
p)$.  The invariant holds under a transition of the first type because:

\begin{eqnarray*}
x' y' + p'      & = &   (x / 2) \cdot 2y + p \\
                & = &   x y + p \\
                & = &   a b
\end{eqnarray*}

The first equation follows from the definition of the first type of
transition.  The second line is obtained by simplification, and the
third line uses the hypothesis that the invariant holds prior to the
transition.  By similar reasoning, the invariant holds under a
transition of the second type:

\begin{eqnarray*}
x' y' + p'      & = &   (x - 1) \cdot y + (p + y)\\
                & = &   x y + p \\
                & = &   a b
\end{eqnarray*}
}

\problempart Prove that the procedure terminates.

\solution{The variable $x$ is a non-negative integer that decreases
under every transition.  Therefore, the procedure must terminate after
at most $x$ transitions.}

\end{problemparts}
\end{problem}
                                 