\documentclass{article}
\usepackage{graphics}
\usepackage{fancyhdr}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage[topbottom,singlearrows]{../logicsym}
\usepackage{multicol}
\usepackage{alltt}


\newcommand{\coursenumber}{081}
\newcommand{\coursetitle}{Computability and Logic}

\topmargin  18pt  	% 27pt
\headheight 12pt  	% 12pt
\headsep    35pt 	% 45pt
\textheight 8.0in
\textwidth  6.2in

\oddsidemargin   22pt      % Left margin on odd-numbered pages.
\evensidemargin  22pt      % Left margin on even-numbered pages.
\marginparwidth  72pt       % Width of marginal notes.
\marginparsep    11pt      % Horizontal space between outer margin and 
                           % marginal note

\pagestyle{fancy}
\lhead{CSCI \coursenumber}
\chead{}
\rhead{\semester}
\lfoot{}
\cfoot{\thepage}
\rfoot{}
\renewcommand{\headrulewidth}{0pt}
\renewcommand{\footrulewidth}{0pt}
\newcommand{\semester}[0]{
     \ifnum\month>7{Fall}\fi
     \ifnum\month<8{Spring}\fi\  \number\year
}

\begin{document}

\begin{center}{\Large Homework 8}\\ \vspace{1 ex} Due midnight,
Thursday, 4/2/2015 \end{center}

\vspace{2 ex}
\noindent

Please submit your homework solutions online at  
\texttt{http://www.dci.pomona.edu/tools-bin/cs081upload.php}.  If you 
have more than one file to be turned in, please put it in a folder 
and zip it up before turning it in.

\vspace{2 ex}

\begin{enumerate}

    \item (10 points) \textbf{Program Proofs}
    
    Problem 4.3.13 from H \& R page 301.  Please show the proof 
    carefully in the same style as the proof in Example 4.17 on page 
    286.  \emph{Hint:  Consider a loop invariant of x == y+a.}
    
    \emph{Be careful to use the Imply rule in the correct direction.  
    In the past many students have lost points by proving 
    implications in the wrong direction!}
 
    
    \item (15 points) \textbf{More program proofs}
    
    This exercise is about integer division.  Suppose that $a$ and $b$
    are positive integers.  If we divide $a$ by $b$ we get a quotient
    $q$ and a remainder $r$ satisfying
    \begin{itemize}
	\item[]
	$a=bq+r$ and $0\le r<b$.
    \end{itemize}
    We use Python/Java/C notation for the remainder, $a\mathrel{\%}b$.
    We say that $b$ \emph{divides} $a$, written $b|a$, if the
    remainder is zero.  Notice that $b|a$ implies $b \leq a$.

    Further, a number $d$ divides both $a$ and $b$ if and only if $d$
    divides both $b$ and~$r$.

    The \emph{greatest common divisor} of $a$ and $b$, written
    $\gcd(a,b)$, is the largest element of the set \\
    $\{d\mid \mbox{$0<d$, $d|a$, and $d|b$}\}$.

    \begin{enumerate}
	\item
	Annotate the block of code in Figure~\ref{Figure:Euclid} to
	verify that it is a correct Hoare triple.  A full box-and-line
	proof is not necessary; just annotate each step and give a
	brief reason why the annotation is correct.

	\begin{figure}[h]
	    \begin{itemize}
		\item[]
		$\{ 0<B<A \}$
		\begin{alltt}
		    a := A;
		    b := B;
		    while (0 < b) \{
		       t := a;
		       a := b;
		       b := t % b;
		    \}
		\end{alltt}
		$\{ \texttt{b}=0\And\Forall d
		\big(0<d\Implies \big(d|\texttt{a}\And
		d|\texttt{b}\Iff d|A\And d|B\big)\big)\}$
	    \end{itemize}
	    \caption[]{An instance of Euclid's algorithm to compute greatest common divisors.}
	    \label{Figure:Euclid}
	\end{figure}

	Until now, we have avoided using the symbol for logical
	equivalence.  The notation $\phi\Iff\psi$ is an abbreviation
	for $(\phi\Implies\psi)\And(\psi\Implies\phi)$.

	\item 
	Argue informally that the postcondition implies $\texttt{a}=\gcd(A,B)$.

    \end{enumerate}

    
    \item (10 points) \textbf{Program Proofs}
    
    Problem 4.4.1a from H \& R page 303. 
    
   \end{enumerate}  
    
\end{document}
