
\documentstyle[twoside,amsfonts,amstex,macros]{article}
% Cross-references for handout numbers.
\input{handout-numbers}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%        SPRING 96:
\newcommand{\coursenumber}{6.042J/18.062J}
\newcommand{\coursetitle}{Mathematics for Computer Science}
\newcommand{\courseprofessors}{Professors Nancy Lynch and Tom Leighton}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newlength{\toppush}
\setlength{\toppush}{2\headheight}
\addtolength{\toppush}{\headsep}

%       Usage: \htitle{handoutnumber}{title}{dateout}
\newcommand{\htitle}[3]{\noindent\vspace*{-\toppush}\newline\parbox{6.5in}
{Massachusetts Institute of Technology \hfill Handout #1 \newline
\coursenumber : \coursetitle \hfill #3 \newline
\courseprofessors\hfill\vspace*{-.5ex} \newline
\mbox{}\hrulefill\mbox{}}\vspace*{1ex}\mbox{}\newline
\bigskip
\begin{center}{\Large\bf #2}\end{center}
\bigskip}

%       Usage: \handout{refname}{title}{dateout}
\newcommand{\handout}[3]{\thispagestyle{empty}
 \markboth{Handout \protect\ref{#1}: #2}{Handout \protect\ref{#1}: #2}
 \pagestyle{myheadings}\htitle{\protect\ref{#1}}{#2}{#3}}





%\parskip1.5ex
\parindent0pt

\begin{document}

\handout{exer}{Exercises on State Machines}{September 30, 1996}


\section{Building Up a Tree}

\noindent We define the $TreeBuilder$ state machine as given below.

\vspace{.12in}
\noindent
\footnotesize

\footnotesize
\noindent
{\bf States:} \nobreak
\vspace{.12in}

\begin{quote} \nobreak
$\ms{V}$, a set of vertices, with initial set $V_0 = \{v_0\}$\\
$\ms{E}$, a subset of $V \times V$, initially empty\\
$\ms{n}$, an element of $\cal N$, initially $n = 1$\\

\end{quote}
\normalsize
\noindent


\footnotesize
\noindent
{\bf Transitions:} \nobreak
\normalsize 
\iocode{
\prcef{$\ms{expand(v,w,x)}$}
{%Precondition:
  $v \in V$\\
  There is at most one edge incident on $v$ in $E$}
{%Effect:
  $V := V \cup \{w,x\}$\\
  $E := E \cup \{(v,w), (v,x)\}$\\
  $n := n +2$}}
 
\vspace{.12in}

\noindent Now prove the following $3$ invariants (in order):
\begin{itemize}
\item $|V| = n$
\item $(V,E)$ is a tree
\item If $|V| \geq 2$, then $(V,E)$ has $(n-1)/2$ internal nodes
\end {itemize}
\newpage
\section{Binary Search}

\noindent In the following, let $k$ be a fixed positive integer. We
then define the $BinarySearch$ state machine as given below.\\ 


\vspace{.12in}
\noindent
\footnotesize


\footnotesize
\noindent
{\bf States:} \nobreak
\vspace{.12in}

\begin{quote} \nobreak
$\ms{A}$, an array indexed by $\{1, .., 2^k-1\}$ of elements of $\cal
N$, subject to $A(i) < A(j)$ if $i <j$\\
$\ms{v}$, an element of $\cal N$, initially arbitrary\\
$\ms{i}$, an element of $\cal N$, initially $i = 2^{k-1}$\\
$\ms{jump}$, an element of $\cal N$, initially $jump = k-1$\\
$\ms{ans}$, an element of $\{1, .., 2^k -1\} \cup \{\ms{unknown}, \ms{no}\}$,
initially $\ms{ans} = \ms{unknown}$\\

\end{quote}
\normalsize
\noindent

\footnotesize
\noindent
{\bf Transitions:} \nobreak
\normalsize 
\iocode{

\prcef{$\ms{less}$}
{%Precondition:
  $\ms{ans} = \ms{unknown}$\\
  $v < A(i)$}
{%Effect:
  If $\ms{jump} > 0$ then\\
  $\;\;\;\ms{jump} := \ms{jump} -1$\\
  $\;\;\; i := i - 2^{\ms{jump}}$\\
  else\\
  $\;\;\; \ms{ans} := \ms{no}$}

\prcef{$\ms{greater}$}
{%Precondition:
  $\ms{ans} = \ms{unknown}$\\
  $v > A(i)$}
{%Effect:
  If $\ms{jump} > 0$ then\\
  $\;\;\;\ms{jump} := \ms{jump} -1$\\
  $\;\;\; i := i + 2^{\ms{jump}}$\\
  else\\
  $\;\;\; \ms{ans} := \ms{no}$}
}{

\prcef{$\ms{equal}$}
{%Precondition:
  $\ms{ans} = \ms{unknown}$\\
  $v = A(i)$}
{%Effect:
   $\ms{ans} := i$}

}
 
\vspace{.12in}


\noindent Now prove the following $3$ invariants:\\
\begin{itemize}

\item At the beginning of each operation, if $v \in A$ then $v \in
  \{A(i-2^{jump}+1), .., A(i+2^{jump}-1) \}$.
\item If $\ms{ans} = \ms{no}$ then $\forall i: A(i) \neq v$.
\item If $\ms{ans} = i \in \cal N$, then $A(i) = v$.
\end {itemize}

\end {document}


























