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

%%% 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}
\usepackage{fancyvrb}

\newcommand{\semester}{Spring 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 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} Homework~\hwnumber~Theory
}}

 \vspace{0.2in}

 \large{Due: Tuesday, February 5, 2013, at the {\bf beginning} of lecture}
\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 written portion of this week's homework will give you some
practice working with the binary representation of integers and reasoning with
invariants.  You are strongly advised to review the C0 language reference guide (available 
at http://c0.typesafety.net/) for details on integer manipulation.  
\vspace{0.2in}

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

\vspace{0.2in}
\begin{center}
  \Large{You {\it must} use this printout, include this cover sheet,

    and staple the whole thing together before turning it in.
  
    Either type up the assignment using
    \href{http://www.cs.cmu.edu/~rjsimmon/15122-s13/hw/15122-theory1.tex}{15122-theory1.tex},

    or print this PDF and write your answers \textit{neatly} by
    hand.}
\end{center}

\newpage
\begin{questions}
\question{\textbf{Basics of \Cnought{}}}

\begin{parts}
\part[3]
Let $x$ be an \texttt{int} in the \Cnought{} language.  Express the
following operations in \Cnought{} using only constants and the bitwise operators
(\texttt{\&}, \texttt{|}, \texttt{\^}, \texttt{\~}, \texttt{<<}, \texttt{>>}).  Your answers should account 
for the fact that \Cnought{} uses 32-bit integers. 
\vspace{0.2in}
\begin{subparts}
    \subpart Set $a$ equal to $x$, where the alpha and green components have both been set 
	to 0, with the red and blue components left unchanged.  (eg \texttt{0xAB12CE34} 
	becomes \texttt{0x00120034}; see Section 1.1 of the Programming portion for more 
	info)  
\begin{solution}
\vspace{0.6in}
\end{solution}

\vspace{0.1in}
    \subpart Set $b$ equal to $x$ with its middle 16 bits flipped ($0 \Longrightarrow 1$ and $1 \Longrightarrow 0$)
	(eg \texttt{0xAB00FF12} becomes \texttt{0xABFF0012})
\begin{solution}
\vspace{0.6in}
\end{solution}

\vspace{0.1in}
    \subpart Set $c$ equal to $x$ with its highest 8 bits set to 1 and with its lowest 8 bits set to 0. (eg \texttt{0xAB12CE34} becomes \texttt{0xFF12CE00})
\begin{solution}
\vspace{0.6in}
\end{solution}

\vspace{0.1in}
    \subpart Set $d$ equal to $x$ with its highest and lowest 16 bits swapped (eg \texttt{0x1234ABCD} becomes \texttt{0xABCD1234})
	
\begin{solution}
\vspace{0.6in}
\end{solution}


\end{subparts}

\newpage

\part[1] Are the following two \texttt{bool} expressions equivalent in \Cnought{},
     assuming \texttt{x} and \texttt{y} are of type \texttt{int}?  Explain your answer.
\begin{verbatim}
      (x%y < 122) && (y != 0)          (y != 0) && (x%y < 122)
\end{verbatim}
\begin{solution}
\vspace{0.6in}
\end{solution}


\part[1]

Is the following code a valid way to check if $a+b+c$ overflows?  If not, give values for $a$, $b$ and $c$ such that the check will return an incorrect result: 

\begin{verbatim}
bool safe_add(int a, int b, int c)
{
  if (a > 0 && b > 0 && c > 0 && a + b + c < 0) return false; 
  if (a < 0 && b < 0 && c < 0 && a + b + c > 0) return false; 
  return true; 
}
\end{verbatim}

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

\part[3]
For each of the following statements, determine whether the statement is
true or false in \Cnought{}.  If it is true, explain why.  If it is false, give a counterexample to illustrate why.
\begin{subparts}
\vspace{0.1in}
    \subpart For every \texttt{int} $x$ and $y$, $x < y$ is equivalent to $x - y < 0$
\begin{solution}
\vspace{0.5in}
\end{solution}

    \subpart For every \texttt{int} $x$:
          $x \rshift 1$ is equivalent to $x / 2$.
\begin{solution}
\vspace{0.5in}
\end{solution}

    \subpart For every \texttt{int} $x$, $y$, and $z$:
          $(x + y) * z$ is equivalent to $z * y + x * z$.
\begin{solution}
\vspace{0.5in}
\end{solution}
\end{subparts}

\end{parts}

\newpage

\question{\textbf{Reasoning with Invariants}}

The Pell sequence is shown below:
\begin{verbatim}
    0, 1, 2, 5, 12, 29, 70, 169, 408, 985, ...
\end{verbatim}
Each integer $i_n$ in the sequence is the sum of $2i_{n-1}$ and $i_{n-2}$.
Consider the following implementation for \texttt{fastpell} that returns the n\textsuperscript{th} Pell number
(the body of the loop is not shown).
\begin{verbatim}
/*  1 */  int PELL(int n)
/*  2 */  //@requires n >= 1;
/*  3 */  {
/*  4 */    if (n <= 1) return 0;
/*  5 */    else if (n == 2) return 1;
/*  6 */    else return 2 * PELL(n-1) + PELL(n-2);
/*  7 */  }
/*  8 */  
/*  9 */  int fastpell(int n)
/* 10 */  //@requires n >= 1;
/* 11 */  //@ensures \result == PELL(n);
/* 12 */  {
/* 13 */    if (n <= 1) return 0;
/* 14 */    if (n == 2) return 1;
/* 15 */    int i = 1; 
/* 16 */    int j = 0;
/* 17 */    int k = 2; 
/* 18 */    int x = 3;
/* 19 */    while (x < n)
/* 20 */      //@loop_invariant 3 <= x && x <= n;
/* 21 */      //@loop_invariant i == PELL(x-1);
/* 22 */      //@loop_invariant j == PELL(x-2); 
/* 23 */      //@loop_invariant k == 2*i+j;
/* 24 */      {
/* 25 */        // LOOP BODY NOT SHOWN
/* 26 */      }
/* 27 */    return k;
/* 28 */  }
\end{verbatim}

\newpage

In this problem, we will reason about the correctness of the
\verb'fastpell' function when the argument \verb'n' is greater than or
equal to \verb'3', and we will complete the implementation based on
this reasoning. 

To completely reason about the correctness of \verb'fastpell', also
need to point out that \verb'fastpell(1) == PELL(1)' and that
\verb'fastpell(2) == PELL(2)'. This is straightforward, because no
loops are involved.

\begin{parts}

\part[2]
Show that each loop invariant is true just before the loop
condition is tested for the first time, using the precondition and
any initialization before the loop condition.

\begin{solution} 

\begin{itemize}
\item \verb'3 <= x && x <= n' -- We know \verb'x' is \verb'3' by line \framebox[.5in][l]{\vphantom{\huge$|$}}, so \verb'3 <= x' is true because \verb'3 <= 3'. 

Because \verb'x' is \verb'3', to show \verb'x <= n' we just need to
show \verb'3 <= n' before the loop condition is tested for the first
time. We know \verb'n' is greater than 1 by line
\framebox[.5in][l]{\vphantom{\huge$|$}} and we know \verb'n' is not 2
by line \framebox[.5in][l]{\vphantom{\huge$|$}}, so it follows that
\verb'n' is greater than or equal to 3.

\item \verb'i == PELL(x-1)' -- Because \verb'x' is \verb'3' before the
  loop condition is tested for the first time, \verb'PELL(x-1)' is
  \framebox[.5in][l]{\vphantom{\huge$|$}} and therefore this loop
  invariant is initially justified by line
  \framebox[.5in][l]{\vphantom{\huge$|$}}.

\item \verb'j == PELL(x-2)' -- Because \verb'x' is \verb'3'
  before the loop condition is tested for the first time,
  \verb'PELL(x-2)' is \framebox[.5in][l]{\vphantom{\huge$|$}} and
  therefore this loop invariant is initially justified by line
  \framebox[.5in][l]{\vphantom{\huge$|$}}.

\item \verb'k == 2*i+j' -- Justified by lines 
\framebox[2in][l]{\vphantom{\huge$|$}}.
\end{itemize}

\end{solution}

\newpage
\part[2]
Show that the loop invariants and the negated loop guard at termination imply the postcondition.
\begin{solution}

We know \verb'x <= n' by line \framebox[.5in][l]{\vphantom{\huge$|$}},
and we know \verb'x >= n' by line
\framebox[.5in][l]{\vphantom{\huge$|$}}, so this implies that \verb'x'
equals \verb'n'. 

The result value is the value of \verb'k' after the loop, so to show
that that the postcondition holds when \verb'n >= 3', it suffices to
show that, after the loop, \verb'k' equals \verb'PELL(x)'.

\begin{itemize}
\item \verb'k' = \verb'2*i + j' (line \framebox[.5in][l]{\vphantom{\huge$|$}})
\item \verb'2*i + j' = \verb'2*PELL(x-1) + j' (line \framebox[.5in][l]{\vphantom{\huge$|$}})
\item \verb'2*PELL(x-1) + j' = \verb'2*PELL(x-1) + PELL(x-2)' (line \framebox[.5in][l]{\vphantom{\huge$|$}})
\item \verb'2*PELL(x-1) + PELL(x-2)' = \verb'PELL(x)' (\verb'PELL' def., \verb'x >= 3' by line \framebox[.5in][l]{\vphantom{\huge$|$}})
\item \verb'k' = \verb'PELL(x)' (transitivity, the four preceding facts)
\end{itemize}
\end{solution}

\part[2] Based on the given loop invariant, write the body of the loop.
{\it DO NOT} use the specification function \verb'PELL()'.

\begin{solution}
\begin{verbatim}
{
  j =

  i = 
 
  k =

  x = 
}
\end{verbatim}
\end{solution}

\part[1]
Explain why the function must terminate with the loop you
gave in 2(c).
\begin{solution}
\vspace{.5in}
\end{solution}

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