\documentclass[12pt]{cas-handout}
\usepackage{paralist}
\usepackage{fancyvrb} % for the Verbatim environment.

% Requires xelatex (and the appropriate font installation)
\setmonofont[Scale=MatchLowercase]{Consolas Bold}

\newcommand{\tsc}[1]{{\rm\textsc{#1}}}

\anumber{6}
\title{Proving Programs}
\duedate{11:00am, Wednesday, October 5}

\begin{document}
\maketitle 

\begin{itemize}
  \item Emails about this assignment should be directed to
    \helpalias.
 \item The usual collaboration rules apply. You may \emph{discuss} an
    exercise with any other student(s) currently taking CS 81 as long as:
    \begin{compactitem}
      \item You contribute equally;
      \item You come away from this discussion only with
        \emph{understanding in your head} --- no written materials or
        computer notes may be retained;
      \item Your submission is authored solely by you, on a separate
        occasion.
   \end{compactitem}
  \item You should refer only to materials from this semester of CS 81 (lecture
   notes, handouts, textbooks, grutors, profs, etc.).
 \item Bring a writeup/printout to class on the due date. Illegible answers
    will get no credit.
\item Make sure your submission includes your name!
\end{itemize}

\hrule

\bigskip\bigskip
\noindent

\section{Maximum of a Function [30 points]}
\enlargethispage{\baselineskip} 
Consider the following code for finding the maximum of a function $f$ on the first $N \ge 1$ natural numbers).

% In this environment (Verbatim + commandchars incantation)
%    Curly braces stand for themselves
%    Square brackets behave like latex curly braces
%    LaTeX macros that start with \ can be invoked
%       which is why I use \ensuremath[...]
%       instead of just writing $...$

\begin{Verbatim}[commandchars=\\\[\]]
 \ensuremath[{\ N \ge 1\ }]

 j = 1
 m = f(0)
 while (j != N):
    if m > f(j):
        j = j + 1
    else:
        m = f(j)
        j = j + 1

 \ensuremath[{\ \displaystyle m=\max\sb[k\in0..N-1]f(k)\ }]
\end{Verbatim}


\begin{enumerate}
\item {[10 points]} Specify a suitable invariant $I$. (It should be true
  before the loop starts, remain true after every iteration, and imply
  the desired postcondition when the loop has terminated.)
\item {[10 points]} Use the proof rules of Hoare Logic to prove the
  code partially correct.  In your ``implied'' steps, you can
 make any mathematically correct deduction and do not need to 
 show the proof of that deduction.
\item {[10 points]} Specify a loop variant that could be used to prove
  termination (and hence total correctness). You do not need to supply such a proof.
\end{enumerate}
\enlargethispage{\baselineskip}

\noindent Hint: my partial correctness proof had the following form, where $I$
is my loop invariant.
\begin{Verbatim}[commandchars=\\\[\],baselinestretch=1.15]
  \ensuremath[{\ N \ge 1\ }]                               \tsc[precondition]
  \ensuremath[{\ \ldots\ }]                                    \tsc[implied]
  j = 1
  \ensuremath[{\ \ldots\ }]                                    \tsc[assignment]
  m = f(0)
  \ensuremath[{\ I }]                                      \tsc[assignment]
  while (j != N):
      \ensuremath[{\ I\ \land\ j\not=N }]                          \tsc[assumption]
      if m > f(j):
          \ensuremath[{\ I\ \land\ j\not=N\ \land\ m>f(j) }]           \tsc[assumption]
          \ensuremath[{\ \ldots }]                                \tsc[implied]
          j = j + 1
          \ensuremath[{\ I }]                                  \tsc[assignment]
      else:
          \ensuremath[{\ I\ \land\ j\not=N\ \land\ m\le[]f(j)\ }]            \tsc[assumption]
          \ensuremath[{\ \ldots }]                                \tsc[implied]
          m = f(j)
          \ensuremath[{\ \ldots }]                                \tsc[assignment]
          j = j + 1
          \ensuremath[{\ I }]                                  \tsc[assignment]
      \ensuremath[{\ I }]                                   \tsc[if]
 \ensuremath[{\ I\ \land\ j=N\ }]                           \tsc[while]
 \ensuremath[{\ \displaystyle m=\max\sb[k\in0..N-1]f(k)\ }]                   \tsc[implied]
\end{Verbatim}

\goodbreak

\section{Remainder via repeated subtraction [35 points]}

The following code computes $a\bmod{}d$ (where $a \ge 0$ and $d > 0$)
via repeated subtraction, and puts the final result in $r$. It tries to speed things up (e.g.,
when $a$ is much larger than $d$) by subtracting larger and larger multiples of $d$
where possible.

\begin{Verbatim}[commandchars=\\\[\]]
  \ensuremath[{\ a\ge0 \land d>0 }] 

  r = a
  while (r >= d):
     g = d
     while (r >= g):
        r = r - g
        g = g + g

  \ensuremath[{\ r = a\bmod[]d }] 
\end{Verbatim}

\begin{enumerate}
\item {[10 points]} Specify a suitable invariant $I_1$ for the outer
  \texttt{while}. (It should be true before the loop starts, remain
  true after every iteration, and imply the desired postcondition when
  the loop has terminated.)
\item {[10 points]} Specify a suitable invariant $I_2$ for the inner
  \texttt{while}. (It should be true before the inner loop starts,
   remain true after every iteration of the inner loop, and imply 
   $I_1$ when the inner loop has terminated. It probably should 
   mention \texttt{g}.)
\item {[10 points]} Use the proof rules of Hoare Logic to prove the
  code partially correct. In your ``implied'' steps, you can
 make any mathematically correct deduction and do not need to 
 show the proof of that deduction.
\item {[5 points]} Specify variants for both loops. (Again, no proof is required.)
\end{enumerate}

\clearpage

Hint: again, my proof skeleton.

\begin{Verbatim}[commandchars=\\\[\],baselinestretch=1.15]
  \ensuremath[{\ a\ge0 \land d>0 }]  \tsc[precondition]
  \ensuremath[{\ \ldots }]              \tsc[implied]
  r = a
  \ensuremath[{\ I\sb1 }]                \tsc[assignment]
  while (r >= d):
     \ensuremath[{\ I\sb1 \land r\ge[]d\ }]       \tsc[assumption]
     \ensuremath[{\ \ldots }]               \tsc[implied]
     g = d
     \ensuremath[{\ I\sb2 }]                \tsc[assignment]
     while (r > g):
        \ensuremath[{\ I\sb2 \land r>g\ }]    \tsc[assumption]
        \ensuremath[{\ \ldots }]            \tsc[implied]
        r = r - g
        \ensuremath[{\ \ldots }]            \tsc[assignment]
        g = g + g
        \ensuremath[{\ I\sb2\ }]             \tsc[assignment]
     \ensuremath[{ I\sb2 \land r\le[]g }]      \tsc[while]
     \ensuremath[{ I\sb1 }]                \tsc[implied]
      
  \ensuremath[{\ I\sb1 \land r<d }]         \tsc[while]
  \ensuremath[{\ r = a\bmod[]d }]      \tsc[implied]
\end{Verbatim}

\clearpage
\section*{Exponentiation [35 points]}

Finally, here is some code that sets $z$ to be $a^b$, where $a$ and $b$ are nonnegative integers.
For efficiency, it uses repeated squaring.  (Recall that \Verb|%| is the standard
way of writing the ``modulo'' operator in code.)

\begin{Verbatim}[commandchars=\\\[\]]
  \ensuremath[{ a\ge0 \land b\ge0 }]

  x = a
  y = b
  z = 1
  while (y != 0):
      while (y % 2 == 0):
          x = x * x
          y = y / 2
      y = y - 1
      z = z * x

  \ensuremath[{\ z = a\sp[b] }]      
\end{Verbatim}

\begin{enumerate}
\item {[10 points]} Specify a suitable invariant $I_1$ for the outer
  \texttt{while}. (It should be true before the loop starts, remain
  true after every iteration, and imply the desired postcondition when
  the loop has terminated.)
\item {[10 points]} Specify a suitable invariant $I_2$ for the inner
  \texttt{while}. (It should be true before the inner loop starts,
   remain true after every iteration of the inner loop, and imply
   whatever is necessary when the inner loop has terminated.)
\item {[10 points]} Use the proof rules of Hoare Logic to prove the
  code partially correct. In your ``implied'' steps, you can
 make any mathematically correct deduction and do not need to 
 show the proof of that deduction.
\item {[5 points]} Specify variants for both loops. (Again, no proof is required.)
\end{enumerate}




\end{document}
