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

%%%
\setmonofont[Scale=MatchLowercase]{Consolas Bold}

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

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

\newif\ifanswers
\answersfalse

\begin{document}
\maketitle



\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 loop 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\ \lnot(m>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\ \lnot(j\not=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 a variant for each loop. (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\ge[]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 \lnot(r\ge[]g) }]      \tsc[while]
     \ensuremath[{ I\sb1 }]                \tsc[implied]

  \ensuremath[{\ I\sb1 \land \lnot(r\ge[]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%%%
way of writing the ``modulo'' or ``remainder'' operator in code.)

\begin{Verbatim}[commandchars=\\\[\]]
  \ensuremath[{ a>0 \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 a variant for each loop. (Again, no proof is required.)

\end{enumerate}




\end{document}
