\documentstyle[12pt,psfig,amssymb]{article}
\input{macros-course}
\begin{document}

\handout{algos}{Proving Algorithm Correctness}{March 10, 1997}
\renewcommand{\gcd}[2]{\mbox{GCD}(#1,#2)}
\newcommand{\Euclid}[2]{\mbox{Euclid}(#1,#2)}

\newcommand{\ef}[2]{
\begin{tabbing}       
XX\= XX\=XX\=XX\=XX\=XX\=   \kill
\protect #1\\
\>Effect: \+ \+ \\ 
   #2  \- \-
\end{tabbing}}

\newcommand{\iocode}[2]{\begin{center}\footnotesize
\begin{minipage}[t]{.45\linewidth}
\hbox to\linewidth{}
#1
\end{minipage}
\hspace{.05\linewidth} 
\begin{minipage}[t]{.45\linewidth}
\hbox to\linewidth{}
#2
\end{minipage}
\end{center}}

 \newcommand{\prcef}[3]{\begin{tabbing}       
XX\=  XX\=XX\=XX\=XX\=  \kill
\protect #1\\
\>Precondition: \+ \+ \\ 
  #2  \-  \- \\ 
\>Effect: \+  \+ \\
  #3 \- \- 
\end{tabbing}} 


The following handout discusses the three ``styles'' of algorithm
correctness proofs we have studied in this class.  In order to
highlight the frameworks rather than the content, I have chosen to
present a single algorithm (our favorite, Euclid's algorithm) and its
correctness proof under all three frameworks.  

The three frameworks we have seen are as follows:
\begin{description}
\item{\bf Functional (Recursive) Programs.} In this model, the algorithm
  is given as a (typically recursive) functional program
  without assignments.  Such programs are close to the static notion
  of mathematical functions, and are typically proved correct by
  induction on the depth of recursive calls made, but can sometimes be
  proved correct by induction on the values of the inputs.
\item{\bf Procedural (Iterative) Programs.} In this model, the
  algorithm is given as a (typically iterative) procedure that
  modifies variables.  Proof of correctness is typically via an {\em
    invariant,} a proposition that is true at all times while the
  program is executing.  We prove that the variant is true at all
  times by induction on the number of program steps, number of
  iterations of the main program loop, or some variant thereof.
\item{\bf State Machines.} In this model, the system is modeled as a
  collection of {\em states.} Each state is often given by a set of
  {\em state variables} whose values change from state to state.
  Computation takes place via a sequence of {\em transitions} from one
  state to another.  As with procedural programs, we prove correctness
  by studying {\em invariants} that are true at every reachable state.
  We prove the invariant is true at every reachable state by induction
  on the number of transitions taken to reach a given state.
\end{description}

In the next sections, I will describe Euclid's algorithm in each of
the 3 formats.  In order to do so, I will need to make use of two
lemmas: one which always forms the core of the inductive step in the
proof of termination, the other which forms the core of the inductive
step in the correct-if-terminates proof.  Both these lemmas are
from the class notes.

\begin{lemma}
\label{lem:mod}
$x \bmod y < y$.
\end{lemma}

\begin{lemma}
\label{lem:gcd}
If $y > 0$, then $\gcd{x}{y}=\gcd{y}{x \bmod y}$.
\end{lemma}
\begin{proof}
Notes from lecture 6.
\end{proof}

\section{Functional Programs}

In this model, the algorithm is given as a (typically
recursive) functional program without assignments.  Such programs are
close to the static notion of mathematical functions, and are
typically proved correct by induction on the depth of recursive calls
made to solve the problem.  Let's momentarily ignore the issue of
termination.  The basic inductive hypothesis has the form ``the
program returns the right answer when the program terminates at
recursion depth $n$,'' and the inductive step relies on the fact that
the recursive call returns the right answer (note that the recursive
call will involve a recursion depth one less than that of the original
call).

Let's consider the concrete case of Euclid's Algorithm.  The
function-program formulation of this algorithm is as follows.

\boxtext{

\begin{tabbing}
else \= else \= else \= \kill
{\bf Procedure} $\Euclid{x}{y}$, ($x,y \in \naturals$, $x \ne 0$)\\
\\
\> {\bf if} $y=0$, then return $x$.\\
\> {\bf else} return $\Euclid{y}{x \bmod y}$.
\end{tabbing}
}

To prove correctness, we need to show two things:
\begin{itemize}
\item If it ever terminates, it gives the right answer (partial
correctness).
\item It eventually terminates.
\end{itemize}

Both of these are normally part of correctness proofs (for standard
sequential algorithms).

\paragraph{Partial correctness}

As stated above, partial correctness is usually proved by induction on
the depth of recursive calls made by the functional program.  If the
program, when called with a certain pair of arguments, terminates at a
depth of $n$ recursive calls, then by definition recursive subproblem
it generates must terminate at a depth of $n-1$ recursive calls.
Here's the proof for Euclid's Algorithm.

\begin{theorem}
If $\Euclid{x}{y}$ terminates, then its output is $\gcd{x}{y}$.
\end{theorem}

\begin{proof}
  The proof is by induction on the number of recursive calls.  The
  inductive hypothesis is ``for any $x$ and $y$ such that
  $\Euclid{x}{y}$ terminates after $n$ recursive calls, the output is
  $\gcd{x}{y}$.''  

  First consider the base case.  This is the case $n=0$, ie, no
  recursive calls.  This case only happens when $y=0$.  But we know
  that $\gcd{x}{0}=x$, and this is what we return in this case.  So
  base case is proven.

  Now we prove the inductive step.  Suppose the inductive hypothesis
  is true for any pair of arguments that makes the algorithm terminate
  at a depth of $n-1$ recursive calls.  Consider an instance
  $\Euclid{x}{y}$ that terminates in $n$ calls.  Then this instance
  generates a recursive call to $\Euclid{y}{x \bmod y}$ that
  terminates at a depth of $n-1$ calls.  It follows from the inductive
  hypothesis that $\Euclid{y}{x \bmod y}$ returns $\gcd{y}{x \bmod
    y}$.  This, then, is also the value that we return. But now
  observe that by Lemma~\ref{lem:gcd}, $\gcd{y}{x \bmod y} =
  \gcd{x}{y}$.  It follows that $\Euclid{x}{y}$ returns $\gcd{x}{y}$.
  This completes the proof of the inductive step.
\end{proof}

We have proven partial correctness, now we prove termination.  This
time we use induction on the input argument values (we can't use
induction on the depth of recursion---this would be circular
reasoning, since until we prove the algorithm terminates, we don't
know that the depth of recursion is finite).

\begin{theorem}
  $\Euclid{x}{y}$ terminates at a depth of at most $y$ recursive
  calls.
\end{theorem}

\begin{proof}
Strong induction on $y$.  The inductive hypothesis is:
$\Euclid{x}{y}$ terminates at a depth of at most $y$ recursive
  calls.  Note this looks the same as the theorem.  But the theorem
  actually has an implicit universal quantification: ``$(\forall y)$,
  the statement holds.''  We will prove this using the inductive hypothesis.

  We start with the base case.  If $y=0$, then we don't make any
  recursive call.  So clearly we terminate at a depth of $0 \le y$
  recursive calls.

  Now consider the inductive step.  Consider a call to $\Euclid{x}{y}$
  where $y > 0$.  This generates a call to $\Euclid{y}{x \bmod y}$.
  By Lemma~\ref{lem:mod}, $x \bmod y < y$.  It follows from the
  inductive hypothesis that $\Euclid{y}{x \bmod y}$ terminates at a
  depth of at most $x \bmod y \le y-1$ recursive calls.  Therefore,
  $\Euclid{x}{y}$ terminates at a recursion depth which is one
  greater, and thus at most $y$.
\end{proof}

\section{Iterative Algorithms}

In this model, the algorithm is given in terms of a (typically
iterative) procedure that modifies variables.  Proof of correctness is
typically via an {\em invariant,} a proposition that is true at all
times while the program is executing.  In particular, the invariant is
true when the program finishes---if we choose the right invariant,
this will prove that the program is correct at the end.\footnote{In
  some cases, the key statement will not actually be an invariant;
  instead, it might be something like ``after $n$ iterations of the
  while loop, the variable $a$ has value $n^2$.''  But the proof
  framework is the same as the one we will see here.} To prove that
the invariant is always true, we use induction on the number of
program steps, number of iterations of the main program loop, or some
variant thereof.  As before, we need to show both partial correctness
and termination.

We now reformulate Euclid's Algorithm as an iterative algorithm.   In
the following code, I am using simultaneous assignments to avoid
temporary variables: $(x,y) \leftarrow (a,b)$ means $x$ gets set to
$a$ and $y$ to $b$ simultaneously.

\boxtext{
\begin{tabbing}
else \= else \= else \= else \= \kill
Procedure $\Euclid{x_0}{y_0}$\\
\\
$(x,y) \leftarrow (x_0,y_0)$\\
{\bf while} $y \ne 0$\\
   \> $(x,y) \leftarrow (y,x \bmod y)$\\
{\bf return} $x$
\end{tabbing}
}

I've introduced two extra variables, $x_0$ and $y_0$.  These are
convenient handles to let me talk about the ``original input values.''

To prove partial correctness of this program, we will introduce an
{\em invariant:} a proposition that is true at all times in the
program.  For this proof, our invariant will be
``$\gcd{x}{y}=\gcd{x_0}{y_0}$.''  Let's see how this works:

\begin{theorem}
$\Euclid{x_0}{y_0}$ returns $\gcd{x_0}{y_0}.$
\end{theorem}
\begin{proof}
  We prove that once $x$ and $y$ have been assigned their initial
  values, the invariant ``$\gcd{x}{y}=\gcd{x_0}{y_0}$'' is true at all
  times during execution of the program.  Why does this suffice?
  Well, consider the situation when the program terminates.  In order
  for the while loop to exit, it must be the case that $y=0$.  At this
  point, we return $x$.  However, by our invariant, when we return
  $x$, it holds that $\gcd{x}{y}=\gcd{x_0}{y_0}$.  But $y=0$, meaning
  that we return $x=\gcd{x}{0}=\gcd{x}{y}=\gcd{x_0}{y_0}$.

  To prove the invariant, we use induction on the number of iterations
  of the while loop.  For the base case, when $0$ iterations have been
  performed, we know that $x=x_0$ and $y=y_0$, so the invariant is
  obviously true.  For the inductive step, suppose the invariant is
  true after $n-1$ iterations of the while loop.  Consider the $n^{th}$
  iteration.  In this iteration, we set $(x,y) \leftarrow (y,x \bmod
  y)$.  Let $x'$ and $y'$ denote these new values for $x$ and $y$.  By
  Lemma~\ref{lem:gcd}, we know that $\gcd{x'}{y'} = \gcd{x}{y}$.  By
  the inductive hypothesis, we know that
  $\gcd{x}{y}=\gcd{x_0}{y_0}$. It follows that $\gcd{x'}{y'} =
  \gcd{x_0}{y_0}$, proving our inductive step.
\end{proof}

Note that this proof used exactly the same content (namely,
Lemma~\ref{lem:gcd}) as did the proof in the functional-program case.
Here, we just packaged that content a little differently.

We also need to prove termination.  We do so as follows (again, the
content will be the same as in the functional program, namely
Lemma~\ref{lem:mod}, but the packaging will be slightly different).

\begin{theorem}
$\Euclid{x}{y}$ always terminates in a finite number of steps.
\end{theorem}
\begin{proof}
  We prove by induction that after $n$ iterations of the while loop,
  $y \le y_0-n$.  It follows that after $y_0$ iterations of the while
  loop, $y \le 0$, meaning the while loop must terminate at or before
  this point.

To prove the induction, start with the base case.  After no
iterations, $y=y_0$, so the inductive hypothesis holds.  Now suppose
the hypothesis holds after $n-1$ iterations.  In the $n^{th}$
iteration, we replace $y$ with $x \bmod y$.  But by
Lemma~\ref{lem:mod}, $x \bmod y < y$, or in other words, $x \bmod y
\le y-1$.  Thus, the $n^{th}$ iteration decreases $y$ by at least 1.
Since by the inductive hypothesis, we had $y \le y_0-(n-1)$ in the
$(n-1)^{st}$ iteration, it must be that after the $n^{th}$ iteration,
$y \le y_0-(n-1)-1 = y_0-n$.
\end{proof}

\section{State Machines}

In this model, the system is modeled as a collection of {\em states.}
Each state is often given by a set of {\em state variables} whose
values change from state to state.  Computation takes place via a
sequence of {\em transitions} from one state to another.  As with
procedural programs, we prove correctness by studying {\em invariants}
that are true at every reachable state.  We prove the invariant is
true at every reachable state by induction on the number of
transitions taken to reach a given state.  If a state is reachable, it
is reachable by a finite number of transitions.  This means we arrive
at it from some immediately preceding state that was reached by one
fewer transitions.

Unlike the previous two models, state machine analyses don't really
talk about the algorithm running to termination.  State machines are
often used to model systems that run forever and have transitions at
unpredictable rates, so what we really care about is the entire set of
reachable states and their properties.


Euclid is therefore a somewhat weird algorithm to study in the state
machine model, since all we really care about is what happens at
termination.  But with appropriate shoehorning, we can use the state
machine model to say something pretty close to the previous two
models.

Here's a state machine model of Euclid's Algorithm.
We can model the algorithm by a state machine as follows.
The state set $Q$ consists of values for 5 ``state variables'': 
\begin{tabbing}
XXX\=XXX\= \kill
\> $x_0 \in \naturals$ \\
\> $y_0 \in \naturals$ \\
\> $x \in \naturals$ \\
\> $y \in \naturals$ \\
\> $\ms{answer} \in \naturals \cup \{ \ms{null} \}$
\end{tabbing}

The variables $x_0$ and $y_0$ represent the ``inputs'' to the program,
whose GCD we want to compute.  The two state variables $x$ and $y$ are
auxiliary state variables which keep track of the current values on
which we are working.  The final state variable, $\ms{answer}$ is
intended to hold the final answer.  It can hold either an answer or
$\ms{null}$, which represents that the answer has not yet been found.

One thing we need to define for a state machine is its start
state(s).  We specify that the start state is the state in which
$x=x_0$, $y=y_0$, and $\ms{answer}=\ms{null}$.

The transition relation is defined by the following two code
fragments.  In this algorithm, only two kinds of things can happen:
reductions, and final decisions.

\boxtext{
\iocode{

\prcef{$\ms{reduction}$}
{% Precondition: \\
   $\ms{answer} = \ms{null}$ \\
   $y_1 \neq 0$}
{% Effect: \\
   $(x_1,y_1) \leftarrow (y_1,x_1 \bmod y_1)$}

}{

\prcef{$\ms{decision}$}
{% Precondition: \\
   $\ms{answer} = \ms{null}$ \\
   $y_1 = 0$}
{% Effect: \\
   $\ms{answer} \leftarrow x_1$}

}
}

In a typical execution, a sequence of $\ms{reduction}$ transitions
occur, followed by a single $\ms{decision}$ transition.

We will prove the following property of all reachable states of this
machine:

\begin{theorem}
If $\ms{answer} \neq \ms{null}$ then $\ms{answer} = \gcd{x}{y}$.
\end{theorem}

This is the statement of {\em partial correctness\/} for the Euclidean
GCD algorithm.  (Since the transitions happen at arbitrary times, it
is a little odd to talk about termination, so we won't.  The above
property says that the state machine, if it decides on an answer,
decides the correct answer).

\begin{proof}
  To prove the property, we make use of a different invariant---one
  quite similar to that used in the iterative program.  We will use
  the following convenient notation.  For a state $q$, $q.x$ denotes
  the value of variable $x$ in state $q$.  The invariant says the
  following: ``in any reachable state $q$,
  $\gcd{q.x}{q.y}=\gcd{q.x_0}{q.y_0}$.''  We prove this invariant by
  induction on the number of transitions to the reachable state.

  First consider the base case.  If we are looking at a state reached
  in $0$ transition steps, we must be looking at a start state.  In a
  start state $q$, $q.x=q.x_0$ and $q.y=q.y_0$, so the invariant is
  trivially true.  
  
  Now the inductive step.  Suppose the invariant is true for any state
  reached in $n-1$ transitions.  Consider a state $q'$ reached via $n$
  transitions.  It must be preceded by a state $q$ that was reached
  via $n-1$ transitions.  The inductive hypothesis therefore applies
  to $q$, meaning that $\gcd{q.x}{q.y} = \gcd{q.x_0}{q.y_0}$.  Now
  consider the transition that takes $q$ to $q'$.  There are two kinds
  of transitions, so we must consider cases.

  If the transition is of type $\ms{decision}$, then the proof is
  obvious.  Since decision changes only the value of $\ms{answer}$, we
  know that $q.x=q'.x$, $q.y=q'.y$, and so on.  So
  $\gcd{q'.x}{q'.y}=\gcd{q.x}{q.y}=\gcd{q.x_0}{q.y_0}=\gcd{q'x_0}{q'.y_0}$.  

  If the transition is of type $\ms{reduce}$, we again use
  Lemma~\ref{lem:gcd}.  From the transition, we see that $q'.x=q.y$
  and $q'.y = x \bmod y$. while $q.x_0=q'.x_0$ and $q.y_0=q'.y_0$.  It
  follows from Lemma~\ref{lem:gcd} that
  $\gcd{q'.x}{q'.y}=\gcd{x}{y}$.  So we deduce that
  $\gcd{q'.x}{q'.y}=\gcd{q.x}{q.y} =
  \gcd{q.x_0}{q.y_0}=\gcd{q'.x_0}{q'.y_0}$.

  So we have proven the invariant claimed at the start of the proof.
  We need go only a little farther in order to prove the invariant of
  the theorem.  Suppose that in reachable state $q'$, we have
  $q'.\ms{answer} \ne \ms{null}$.  Consider the previous state $q$.
  What transition could deliver us to $q'$?  Only a $\ms{decision}$
  transition.  It follows that $q.y=0$ (since this is a precondition
  for the $\ms{decision}$ transition to occur).  By the invariant that
  we proved before, we know that $\gcd{q.x}{q.y}=\gcd{q.x_0}{q.y_0}$.
  Therefore, since $q.y_0=0$, we know that
  $q.x=\gcd{q.x}{q.y}=\gcd{q.x_0}{q.y_0}$.  Thus in the $\ms{decision}$
  transition, we set $q'.\ms{answer}=q.x=\gcd{q.x_0}{q.y_0}$ as
  desired.  This proves the claim.
\end{proof}

Note the similarity to our iterative algorithm proof.  In fact, this
state machine can be seen as a model for the state of the iterative
algorithm.  

\end{document}

% Local Variables: 
% mode: latex
% TeX-master: t
% End: 
% LocalWords:  GCD
