\documentclass[12pt]{exam}
\newcommand{\hwnumber}{1}

%%% begin hw-packages-and-macros.tex
\usepackage{amsmath}
\usepackage[left=1in, right=1in, top=1in, bottom=1in]{geometry}
\usepackage{graphicx}
\usepackage{hyperref}
\usepackage{color}
\usepackage[all]{xy}
\usepackage{wrapfig}

\newcommand{\semester}{Fall 2013}

\newcommand{\Cnought}{C$_0$}
\newcommand{\modulo}{\ \texttt{\%}\ }
\newcommand{\lshift}{\ \texttt{<<}\ }
\newcommand{\rshift}{\ \texttt{>>}\ }
\newcommand{\cgeq}{\ \texttt{>=}\ }
\newtheorem{task}{Task}
\newtheorem{ectask}{Extra Credit Task}
\newtheorem{exercise}{Exercise}

\newcommand{\answerbox}[1]{
\begin{framed}
\hspace{5.65in}
\vspace{#1}
\end{framed}}

\pagestyle{head}

\headrule \header{\textbf{15-122 Written Homework \hwnumber}}{}{\textbf{Page
\thepage\ of \numpages}}

\pointsinmargin \printanswers

\setlength\answerlinelength{2in} \setlength\answerskip{0.3in}
%%% end hw-packages-and-macros.tex

\begin{document}

\addpoints
\begin{center}
\textbf{\large{15-122 : Principles of Imperative Computation, \semester
\\  \vspace{0.2in} Written Homework~\hwnumber
}}

 \vspace{0.2in}

 \large{Due: Thursday, September 5, 2013 at 10pm}
\end{center}

\vspace{0.5in}

\hbox to \textwidth{Name:\enspace\hrulefill}


\vspace{0.2in}

\hbox to \textwidth{Andrew ID:\enspace\hrulefill}

\vspace{0.2in}

\hbox to \textwidth{Recitation:\enspace\hrulefill}


\vspace{0.5in}

\noindent The theory portion of this week's homework will introduce
you to the way we reason about C0 code in 15-122.
\vspace{0.2in}

\begin{center}
\gradetable[v][questions]
\end{center}

\vspace{0.2in}
\begin{center}
  \Large{You {\it must} print this PDF and write your answers
    \textit{neatly} by hand.

    You can hand the assignment in during lecture or, after lecture,
    outside of Tom Cortina's office (GHC 4117).}
\end{center}

\newpage
\begin{questions}

\question{\textbf{Running C0 programs}}

\begin{parts}

The file \verb'foo.c0' contains a function \verb'foo' that takes an
integer and returns an integer. From the command line, give two
different ways of testing the value of \verb'foo(12)'; one is given.

\begin{solution}
\begin{verbatim}
% echo "int main() { return foo(12); }" > foo-test.c0
% cc0 -d -x foo.c0 foo-test.c0 
33
\end{verbatim}
\end{solution}

\part[1] Use the \verb'cc0' compiler without 
\verb'-x' and with the \verb'-o' option.

\begin{solution}
\vspace{1.8in}
\end{solution}

\part[1] Use the Coin interpreter.

\begin{solution}
\vspace{1.8in}
\end{solution}
\end{parts}

You are encouraged (on this and other ``written'' homeworks) to
actually type out and test your solutions. Keep in mind, though: one
reason we ask you to write code by hand in homework is because, on the
midterms and final, you will be required to read and write code by
hand without the benefit of a computer. One strategy is to try to do
homeworks without a compiler at first, but then test your answers just
like you'd test your programming assignments. But do what works for
you!

Finally, note that the problems above are problem 1(a) and 1(b). The
(1) that is in parentheses next to the left of the (a) and the (b)
refers to how many points the sub-problems are worth.

\question{\textbf{The preservation of loop invariants}}

The core of proving the correctness of a function with a loop is
proving that the loop invariant is {\it preserved} -- that if the loop
invariant holds at the beginning of a loop, it still holds at the end.

For each of the following loops, state whether the loop invariant is
always preserved or not. If you say that the loop invariant is always
preserved, prove this. If you say that the loop invariant is not
always preserved, give initial values of the assignable variables such
that the loop guard and loop invariant will hold before the loop body
executes, but where the loop invariant will not hold after the loop
body executes.

In this problem and in the next one, we will give solutions to some of
the questions to give you some idea of what we are looking for. We
will give two answers: a ``long form'' answer where we write out all
the reasoning, and a ``short form'' answer where we just give the
facts that we know to be true and the line or lines that justify those
facts. You can answer questions either way; we prefer the shorter
version.

\begin{parts}

\part[0]

\begin{verbatim}
/* 1 */  while(j < 10000)
/* 2 */    //@loop_invariant 2 * i == j;
/* 3 */    {
/* 4 */      i = i+2;
/* 5 */      j = j+4;
/* 6 */    }
\end{verbatim}

\begin{solution} The loop invariant is always preserved.

{\it Long version}: From line \verb'1', we know that \verb'j < 10000'
at the beginning of the loop and from line \verb'2' we know \verb'2 * i' =
\verb'j' at the beginning of the loop. 

We use primed variables to refer to the values stored in \verb'i' and
\verb'j' at the end of the loop. Therefore, to show that the loop
invariant is preserved, we need to show that \verb"2 * i'" = \verb"j'"
where \verb"i'" = \verb"i+2" (line \verb'4') and \verb"j'" =
\verb"j+4" (line \verb'5').

Therefore we have that \verb"2 * i'" = \verb"2 * (i+2)" =
\verb"2 * (i+2)" = \verb"2*i + 4" = \verb"2*i + 4" = \verb"j + 4" =
\verb"j'", which by transitivity is what we needed to show.

{\it Short version}:
\begin{tabbing}
--~~\= \verb"2 * i'" = \verb"2 * (i+2)"\qquad\= (line \verb'4')\\
--\> \verb"2 * (i+2)" = \verb"2*i + 4"\> (distributivity)\\
--\> \verb"2*i + 4" = \verb"j + 4"\> (line \verb'2')\\
--\> \verb"j + 4" = \verb"j'"\> (line \verb'5')\\
--\> \verb"2 * i'" = \verb"j'"\> (transitivity, the four preceding facts)
\end{tabbing}
\end{solution}

\newpage

\part[2]
\begin{verbatim}
/* 1 */  while (k <= n)
/* 2 */    //@loop_invariant i*i == k;
/* 3 */    {
/* 4 */      k = k + 2*i + 1;
/* 5 */      i = i + 1;
/* 6 */    }
\end{verbatim}

\begin{solution}
\vspace{2.5in}
\end{solution}

\part[2]

\begin{verbatim}
/* 1 */  while(i < x)
/* 2 */    //@loop_invariant x <= y;
/* 3 */    //@loop_invariant i < y;
/* 4 */    {
/* 5 */      i++;
/* 6 */    }
\end{verbatim}

\begin{solution}
\vspace{2.5in}
\end{solution}

\newpage
\part[2]

\begin{verbatim}
/* 1 */  while (a != b)
/* 2 */    //@loop_invariant a > 0 && b > 0;
/* 3 */    {
/* 4 */      if (a > b) {
/* 5 */        a = a - b;
/* 6 */      } else { 
/* 7 */        b = b - a;
/* 8 */      }
/* 9 */    }
\end{verbatim}

\begin{solution} The loop invariant is always preserved.

We reason by case analysis on the relationship between the integers
\verb'a' and \verb'b'.

Case 1: \verb'(a > b)'
\vspace{2.5in}

Case 2: \verb'(a < b)'
\vspace{2.5in}

Case 3: \verb'(a == b)'

Because we know \verb'a != b' (line \verb'1'), this case is impossible.
\end{solution}

\newpage
\part[1]

\begin{verbatim}
/* 1 */  while (e > 0)
/* 2 */    //@loop_invariant e > 0 || accum == POW(x,y);
/* 3 */    {
/* 4 */      accum = accum * x;
/* 5 */      e = e - 1;
/* 6 */    }
\end{verbatim}

\begin{solution} The loop invariant is not always preserved.
\vspace{2.5in}
\end{solution}

\part[2]

\begin{verbatim}
/* 1 */  while(x == 2*y)
/* 2 */    //@loop_invariant i == 4*j;
/* 3 */    {
/* 4 */      i = i+2*x;
/* 5 */      j = j+y;
/* 6 */      x = f(i);
/* 7 */    }
\end{verbatim}

\begin{solution}
\vspace{2.5in}
\end{solution}

\end{parts}

\newpage

\question{\textbf{Assertions in loops}}

This question involves a series of functions \verb'f' with one loop;
each contains additional \verb'//@assert' statements. None of the
assertions will ever fail -- they will never evaluate to \verb'false'
when the function \verb'f' is called with arguments that satisfy the
precondition. However, if our loop invariants aren't up to the task,
we may not be able to {\it prove} these assertions hold.

When assignable variables are {\it untouched} by a loop, statements we
know to be true about those untouched assignables {\it before} the
loop remain valid {\it inside} the loop and {\it after} the loop. For
assignables that are modified by the loop, the loop guard and the loop
invariants are the only statements we can use.  Inside of a loop, we
know that the loop invariant held just before the loop guard was
checked and that the loop guard returned \verb'true'.  After a loop,
we know that the loop invariant held just before the loop guard was
checked for the last time and that the loop guard returned
\verb'false'.

For each of the problems below, you can assume that the loop invariant
is true initially (before the loop guard is checked the first time)
and that it is always preserved.

\begin{parts}

\part[0]
\begin{verbatim}
/*  1 */  int f(int a, int b) 
/*  2 */  //@requires 0 <= a && a < b;
/*  3 */  {
/*  4 */    int i = 0;
/*  5 */    while (i < a) {
/*  6 */      //@assert i < b; /*** Assertion 1 ***/
/*  7 */      i += 1;
/*  8 */    }
/*  9 */    //@assert i == a; /*** Assertion 2 ***/
/* 10 */    return i;
/* 11 */  }
\end{verbatim}

\begin{solution} \verb'Assertion 1' is supported.

{\it Long version}: Because the assignables \verb'a' and \verb'b' are
not modified by the loop, the assertion \verb'a < b' from line
\verb'2' can be used at line \verb'6'. Because we are inside the loop,
we know the loop guard held at the beginning of the loop, so line
\verb'5' gives us that \verb'i < a'. The facts \verb'i < a' and
\verb'a < b' together imply \verb'i < b'.

{\it Short version}:
\begin{tabbing}
--~~\= \verb'i < a'\qquad\= (line \verb'5')\\
--\> \verb'a < b'\> (line \verb'2')\\
--\> \verb'i < b'\> (\verb'i < a') $\wedge$ (\verb'a < b') $\Rightarrow$ (\verb'i < b')
\end{tabbing}
\end{solution}

\begin{solution} \verb'Assertion 2' is unsupported.

At line \verb'9', we know that the loop guard \verb'i < a' is false --
that is, we know that \verb'!(i < a)', which is the same thing as
saying \verb'i >= a'. We can't conclude, from this, that \verb'i' is
equal to \verb'a'.
\end{solution}

\newpage

\part[3]
\begin{verbatim}
/*  1 */  int f(int a, int b) 
/*  2 */  //@requires 0 <= a && a <= b;
/*  3 */  {
/*  4 */    int i = 0;
/*  5 */    while (i < a) 
/*  6 */      //@loop_invariant 0 <= i;
/*  7 */      {
/*  8 */        //@assert 0 <= i && i < b; /*** Assertion 3 ***/
/*  9 */        i += 1;
/* 10 */      }
/* 11 */    //@assert i <= b; /*** Assertion 4 ***/
/* 12 */    return i;
/* 13 */  }
\end{verbatim}

\begin{solution} \verb'Assertion 3' is 
\vspace{2.5in}
\end{solution}

\begin{solution} \verb'Assertion 4' is 
\vspace{2.5in}
\end{solution}

\newpage

\part[3]
\begin{verbatim}
/*  1 */  int f(int a, int b) 
/*  2 */  //@requires 0 <= a && a <= b;
/*  3 */  {
/*  4 */    int i = 0;
/*  5 */    while (i < a) 
/*  6 */      //@loop_invariant i <= a; 
/*  7 */      {
/*  8 */        //@assert i < b; /*** Assertion 5 ***/
/*  9 */        i += 1;
/* 10 */      }
/* 11 */    //@assert i == a; /*** Assertion 6 ***/
/* 12 */    return i;
/* 13 */  }
\end{verbatim}

\begin{solution} \verb'Assertion 5' is
\vspace{2.5in}
\end{solution}

\begin{solution} \verb'Assertion 6' is
\vspace{2.5in}
\end{solution}

\newpage

\part[3]
\begin{verbatim}
/*  1 */  int f(int a, int b) 
/*  2 */  //@requires 0 <= a && 2*a < b;
/*  3 */  {
/*  4 */    int i = 0;
/*  5 */    while (i < a) {
/*  6 */      //@assert i < b; /*** Assertion 7 ***/
/*  7 */      i += 2;
/*  8 */      a += 1;
/*  9 */    }
/* 10 */    //@assert a <= i; /*** Assertion 8 ***/
/* 11 */    return i;
/* 12 */  }
\end{verbatim}

\begin{solution}  \verb'Assertion 7' is
\vspace{2.5in}
\end{solution}

\begin{solution}  \verb'Assertion 8' is
\vspace{2.5in}
\end{solution}

\end{parts}

\end{questions}
\end{document}

\newpage
\question{\textbf{Thinking about how proofs can break}}

In this problem, we will work with loop invariants for the power
function.

\begin{verbatim}
int pow_impl(int x, int y)
//@requires y >= 0;
//@ensures \result == POW(x,y);
{
  int accum = 1;
  int e = y;
  while (e > 0) {
    accum = accum * x;
    e = e - 1;
  }
  return accum;
}
\end{verbatim}

\begin{parts}
\part[2]
Give a loop invariant that is true initially, is preserved by any
iteration of the loop, but that does not imply the postcondition.

\begin{solution}
\vspace{.4in}
\end{solution}

\part
Give a ``loop invariant'' that is not true initially, but that is
preserved by any iteration of the loop. (It can imply the
postcondition or not, either way is fine.)
\begin{solution}
\vspace{.4in}
\end{solution}


\part[2]
Recall from question 2(e) that the ``loop invariant''
\verb'e > 0 || accum == POW(x,y)' is not preserved by every iteration
of the loop. However, it is true initially and it does imply the
postcondition. (You should convince yourself of this.)

Come up with a {\it different} loop body where
\verb'e > 0 || accum == POW(x,y)' {\it is} a provably valid loop
invariant. You're generally not allowed to use specification functions
in your code, but in this case you may use the \verb'POW()' function
in your revised loop body. Your solution must terminate, otherwise
just leaving the loop body empty would be a valid solution!
(You should convince yourself of this, too.)

\begin{solution}
\begin{verbatim}
while (e > 0) {



}
\end{verbatim}
\end{solution}



\end{parts} 
\end{questions}
\end{document}

