\documentstyle[11pt]{article}
% frob with the margins
\addtolength{\topmargin}{-1in}
\addtolength{\footskip}{-1in}
\addtolength{\textheight}{2in}
\addtolength{\oddsidemargin}{-.5in}
\addtolength{\evensidemargin}{-.5in}
\addtolength{\textwidth}{1in}
% no page numbers
\pagestyle{empty}
% counter for page numbers
\newcounter{pg}
\setcounter{pg}{2}

% DEFINE THE PROBLEM SET NUMBER
\def\psnum{2 (Non-Programming)}

% DEFINE THE DUE DATE
\def\due{April 23, 1991}

% title command
\newcommand{\mytitle}{{\large\noindent 6.170 \hfill{} Juliet Bourne \\
Problem Set \psnum \hfill{} \due \\}
\vspace{-.6in}
\begin{center} \rule{6in}{.25mm} \end{center}}
\newcommand{\mypage}{\newpage{\large\noindent 6.170 \hfill{} Juliet Bourne \\
Problem Set \psnum \hfill{} \due \\}
\vspace{-.6in}
\begin{center} \rule{6in}{.25mm} \end{center}}
% problem command
\newcommand{\prob}[1]{\noindent{\fbox{\large\bf Problem #1}}\vspace{.25in}}
% subproblem command
\newcommand{\subprob}[1]{\vspace{.15in} \noindent{\large\bf #1.}}
% equations commands
\newcommand{\beq}{\vspace*{-.3in}\begin{eqnarray*}}
\newcommand{\eeq}{\end{eqnarray*}}

\begin{document}

\mytitle

\begin{center}
{\Large\bf Reasoning about Programs}
\end{center}

\subprob{a} Total correctness formula:

\noindent$s_o = s$
\vspace*{-.15in}
\begin{verbatim}
{
j:int := rep$high(s)
ans:bool := false
while j >= rep$low(s) do
   if s[j] = i
        then ans := true;
             j := rep$low(s) - 1
        else j := j - 1
        end
   end
}
\end{verbatim}
\vspace*{-.15in}
$(ans = i \in s) \& (s = s_0)$

\subprob{b} Loop invariant and decrementing function:

{\em loop invariant:} 

\verb+(ans = exists x:int [j < x <= rep$high(s) & s[x] = i]) &+ $(s = s_0)$

{\em decrementing function:}

\verb@j - rep$low(s) + 1@

\subprob{c} Proof of total correctness formula:

\begin{enumerate}
\item Show invariant holds before entry to loop:

assert $s_0 = s$
\vspace*{-.15in}
\begin{verbatim}
j:int := rep$high(s)
ans:bool := false
\end{verbatim}
\vspace*{-.15in}
assert \verb+(ans = exists x:int [j < x <= rep$high(s) & s[x] = i]) &+ $(s = s_0)$

Apply rule of assignment:

assert $s_0 = s$
\vspace*{-.15in}
\begin{verbatim}
j:int := rep$high(s)
\end{verbatim}
\vspace*{-.15in}
assert \verb+(false = exists x:int [j < x <= rep$high(s) & s[x] = i]) &+ $(s = s_0)$

Apply rule of assignment again:

assert $s_0 = s$
assert \verb+(false = exists x:int [rep$high(s) < x <= rep$high(s) & s[x] = i]) &+ $(s = s_0)$

$s_0 = s \Rightarrow$ \verb+(false = exists x:int [rep$high(s) < x <= rep$high(s) & s[x]=i]) &+ $(s = s_0)$

The first assertion just introduces the variable $s_0$ and gives it the
value of $s$. Thus, it is obviously \verb+true+. The first part of the
second assertion reduces to the identity \verb+false = false+ since there
cannot exist an $x: a < x <= a$. The second part of the second assertion is
\verb+true+ since $s_0 = s$ from the first assertion and from the
specification of \verb+rep$high+, $s$ is not modified, so it still
equals $s_0$.

\mypage

\item Show invariant is preserved by the loop body:

Looking at the specs, \verb+rep$low+ doesn't modify $s$; so, the test
doesn't modify anything.

assert \verb+(ans = exists x:int [j < x <= rep$high(s) & s[x] = i]) &+
$(s = s_0)$ \verb+& j >= rep$low(s)+
\vspace*{-.15in}
\begin{verbatim}
if s[j] = i
     then ans := true;
          j := rep$low(s) - 1
     else j := j - 1
     end
end
\end{verbatim}
\vspace*{-.15in}
assert \verb+(ans = exists x:int [j < x <= rep$high(s) & s[x] = i]) &+ $(s = s_0)$

Case analysis:
\begin{itemize}
\item Subgoal 1:

assert \verb+(ans = exists x:int [j < x <= rep$high(s) & s[x]=i]) &+
$(s=s_0)$ \verb+& j >= rep$low(s) &+ $s[j]=i$
\vspace*{-.15in}
\begin{verbatim}
     ans := true
     j := rep$low(s) - 1
\end{verbatim}
\vspace*{-.15in}
assert \verb+(ans = exists x:int [j < x <= rep$high(s) & s[x]=i]) &+ $(s=s_0)$

Apply rule of assignment:

assert \verb+(ans = exists x:int [j < x <= rep$high(s) & s[x]=i]) &+
$(s=s_0)$ \verb+& j >= rep$low(s) &+ $s[j]=i$
\vspace*{-.15in}
\begin{verbatim}
     ans := true
\end{verbatim}
\vspace*{-.15in}
assert \verb+(ans = exists x:int [rep$low(s)-1 < x <= rep$high(s) & s[x]=i]) &+ $(s=s_0)$

Apply rule of assignment again:

assert \verb+(ans = exists x:int [j < x <= rep$high(s) & s[x]=i]) &+
$(s = s_0)$ \verb+& j >= rep$low(s) &+ $s[j]=i$

assert \verb+(true = exists x:int [rep$low(s)-1 < x <= rep$high(s) & s[x]=i]) &+ $(s=s_0)$

The first assertion implies the second since $s[j]=i$,
\verb+j>=rep$low(s)+, and \verb+rep$low+ doesn't modify $s$.

\item Subgoal 2:

assert \verb+(ans = exists x:int [j < x <= rep$high(s) & s[x]=i]) &+
$(s=s_0)$ \verb+& j >= rep$low(s) &+ $s[j] \neq i$
\vspace*{-.15in}
\begin{verbatim}
j := j - 1
\end{verbatim}
\vspace*{-.15in}
assert \verb+(ans = exists x:int [j < x <= rep$high(s) & s[x]=i]) &+
$(s=s_0)$ 

Apply rule of assignment:

assert \verb+(ans = exists x:int [j < x <= rep$high(s) & s[x]=i]) &+
$(s=s_0)$ \verb+& j >= rep$low(s) &+ $s[j] \neq i$

assert \verb+(ans = exists x:int [j-1 < x <= rep$high(s) & s[x]=i]) &+
$(s=s_0)$ 

If \verb+ans = true+ then the first assertion implies the second
assertion since \verb+j-1 < x <= rep$high(s)+ includes \verb+j < x <= rep$high(s)+. 

If \verb+ans = false+ then the first assertion implies the second since,
with $x=j$, $s[x] = s[j] \neq i$ and for \verb+j < x <= rep$high(s)+,
$s[x] \neq i$.
\end{itemize}

\mypage

\item Show invariant and negation of loop test $\Rightarrow$
post-condition:

\verb+(ans = exists x:int [j<x<=rep$high(s) & s[x]=i]) &+ $(s=s_0)$ \&
\verb+~(j>=rep$low(s))+  

implies 

\verb+(ans = exists x:int [j < x <= rep$high(s) & s[x] = i]) &+ $(s = s_0)$ 

since \verb+~(j >= rep$low(s))+ implies that \verb+j < rep$low(s) - 1+
and that implies that 

\verb+ans = exists x:int [rep$low(s) - 1 < x <= rep$high(s) & s[x]=i] &+
$s = s_0$

which means that the whole set was looked at.

\item Show that the loop terminates:

assert \verb@(d0 = j - rep$low(s) + 1) & j >= rep$low(s)@
\vspace*{-.15in}
\begin{verbatim}
     if s[j] = i
          then ans := true;
               j := rep$low(s) - 1
          else j := j + 1
\end{verbatim}
\vspace*{-.15in}
assert \verb@j - rep$low(s) + 1 < d0@

Case analysis:

\begin{itemize}
\item Subgoal 1:

assert \verb@(d0 = j - rep$low(s) + 1) & j >= rep$low(s) &@ $s[j]=i$
\vspace*{-.15in} 
\begin{verbatim}
     ans := true;
     j := rep$low(s) - 1
\end{verbatim}
\vspace*{-.15in}
assert \verb@j - rep$low(s) + 1 < d0@

Apply rule of assignment twice (second one doesn't change anything):

assert \verb@(d0 = j - rep$low(s) + 1) & j >= rep$low(s) &@ $s[j]=i$

assert \verb@rep$low(s) - 1 - rep$low(s) + 1 < d0@

The second assertion states that $d0 > 0$, which is \verb+true+ since 
\verb+j >= rep$low(s)+ implies \verb+d0 >= 1+.

\item Subgoal 2:

assert \verb@(d0 = j - rep$low(s) + 1) & j >= rep$low(s) &@ $s[j] \neq i$
\vspace*{-.15in} 
\begin{verbatim}
     j := j - 1
\end{verbatim}
\vspace*{-.15in}
assert \verb@j - rep$low(s) + 1 < d0@

Apply rule of assignment:

assert \verb@(d0 = j - rep$low(s) + 1) & j >= rep$low(s) &@ $s[j] \neq i$

assert \verb@j - 1 - rep$low(s) + 1 < d0@

The second assertion states that \verb+d0 - j + rep$low(s) > 0$, which
is \verb+true+ since in the first assertion \verb+j >= rep$low(s)+
implies \verb+d0 >= 1+. 

\end{itemize}

\item Decrementing function \verb+ <= + 0 implies negation of loop test:

\verb@j - rep$low(s) + 1 <= 0@ $\Rightarrow$ \verb+j < rep$low(s)+

which reduces to \verb+true+.

\end{enumerate}

QED.

\end{document}
