\documentclass[11pt,twoside]{article}
\usepackage{macros-course-lectures}

\renewcommand{\thepage}{\arabic{page}}

%\makeslides

\renewcommand{\thefootnote}{}

\begin{document}

\onlystudents

\lecture{notes9}{%
Proof Methods for State Machines}{October 5, 2000}

\reading{These notes.  Rosen Section 3.5 (skim)}

\section{Invariants and the Invariant Theorem}

\begin{definition}
An {\em invariant\/} of a state machine $M = (Q, Q_0, \delta)$ is a
predicate $P(q)$ that is true for all reachable states $q$. \\
\end{definition}

\begin{tabbing}
XXX\=XXX\=XXX\=XXX\=XXXXXXXXXXXXXXXXXXXXX\=    \kill
Given: $M = (Q,Q_0,\delta)$ is a state machine. \\
Prove: $P$ is an invariant of $M$. \\
1. $\forall q \in Q_0  (P(q))$ \\
2. $\forall (q,q') \in \delta (P(q) \Rightarrow P(q'))$. \\
3. QED
\> \> \> \> \> Invariant theorem
\end{tabbing}

\begin{theorem}
(Invariant theorem) \\
Suppose $M = (Q,Q_0,\delta)$ is a state machine, and $P$ is a
predicate of states in $Q$ such that: 
\begin{enumerate}
\item
$\forall q \in Q_0  (P(q))$, and
\item
$\forall (q,q') \in \delta (P(q) \Rightarrow P(q'))$.
\end{enumerate}
Then $P$ is an invariant of $M$ (that is, is true in all reachable
states of $M$). 
\end{theorem}

\begin{tabbing}
XXX\=XXX\=XXX\=XXX\=XXXXXXXXXXXXXXXXXXXXX\=    \kill
Given: $M = (Q,Q_0,\delta)$ is a state machine. \\
Given: $\forall q \in Q_0  (P(q))$ \\
Given: $\forall (q,q') \in \delta (P(q) \Rightarrow P(q'))$. \\
Prove: $P$ is an invariant of $M$, that is,
$\forall q \in Q (q \mbox{ reachable } \Rightarrow P(q))$ \\
1. Let $P'(n)$ be the predicate
   $\forall q$, $q$ a final state of an $n$-step execution $(P(q))$. \\
2. $\forall n \geq 0 (P'(n))$ \\
\> 1. (Base) $P'(0)$ 
   \> \> \> \> By the assumption about start states \\
\> 2. (Inductive step) $\forall n \geq 0 (P'(n) \Rightarrow P'(n+1))$ \\
\> \> 1. Fix $n \geq 0$ \\
\> \> 2. Assume $P'(n)$ \\
\> \> 3. $P'(n+1)$, that is, $P$ is true for all final states of $n+1$-step
executions. \\
\> \> \> 1. Fix an $n+1$-step execution $q_0,q_1,\ldots,q_n,q_{n+1}$. \\
\> \> \> 2. $q_n$ is the final state of an $n$-step execution. \\
\> \> \> 3. $P(q_n)$ 
         \> \> Inductive hypothesis (2.2.2) \\
\> \> \> 4. $(q_n,q_{n+1})$ is a step of $M$. \\
\> \> \> 5. $P(q_{n+1})$ 
         \> \> By the assumption about steps preserving $P$ \\
\> \> \> 6. QED
         \> \> UG \\
\> \> 4. QED \\
\> 3. QED
   \> \> \> \> Induction \\
3. QED ($P$ is an invariant of $M$)
\> \> \> \> \> Definition of ``reachable''
\end{tabbing}

\begin{tabbing}
XXX\=XXX\=XXX\=XXX\=XXXXXXXXXXXXXXXXXXXXX\=    \kill
Prove: $P$ is an invariant of the Die Hard state machine. \\
1. $\forall q \in Q_0  (P(q))$ 
\> \> \> \> \> $P$ true for start state $(0,0)$. \\
2. $\forall (q,q') \in \delta (P(q) \Rightarrow P(q'))$. \\
\> 1. Fix $(q,q') \in \delta$ \\ 
\> 2. Assume $P(q)$. \\
\> 3. $P(q')$ \\
\> \> 1. If $(q,q')$ fills the little jar, then $P(q')$. \\
\> \> 2. If $(q,q')$ fills the big jar, then $P(q')$. \\
\> \> 3. If $(q,q')$ empties the little jar, then $P(q')$. \\
\> \> 4. If $(q,q')$ empties the big jar, then $P(q')$. \\
\> \> 5. If $(q,q')$ pours from little to big, then $P(q')$. \\
\> \> 6. If $(q,q')$ pours from big to little, then $P(q')$. \\
\> \> 7. QED
      \> \> \> Cases \\
\> 4. QED    
   \> \> \> \> Implication, UG \\
3. QED 
\> \> \> \> \> Invariant theorem
\end{tabbing}

\section{Termination and Time Bound Theorems}

\begin{definition}
Suppose $M = (Q,Q_0,\delta)$ is a state machine. \\
Then a {\em termination function\/} for $M$ is a function 
$f$ mapping reachable states of $M$ to $N$, such that for every
reachable $q$ and $q'$ with $(q,q')$ in $\delta$, $f(q') < f(q)$. 
\end{definition}

\begin{theorem}
(Time bound theorem) \\
Suppose $M = (Q,Q_0,\delta)$ is a state machine, and $f: Q \rightarrow
N$ is a termination function for $M$. \\
Then the number of steps in any execution starting from $q \in Q_0$
is at most $f(q)$.
\end{theorem}

\begin{theorem}
(Termination theorem) \\
Suppose $M = (Q,Q_0,\delta)$ is a state machine, and $f: Q \rightarrow
N$ is a termination function for $M$. \\
Then every execution of $M$ is finite. 
\end{theorem}

\begin{tabbing}
XXX\=XXX\=XXX\=XXX\=XXXXXXXXXXXXXXXXXXXXX\=    \kill
Given: $M = (Q,Q_0,\delta)$ is a state machine. \\
Given: $e$ is an execution of $M$, $k \in N$. \\
Prove: $e$ has at most $k$ steps. \\
1. $f: Q \rightarrow N$ is a termination function for $M$. \\
2. $f(q) \leq k$, where $q \in Q_0$ is the first state of $e$. \\
3. QED
\> \> \> \> \> Time bound theorem
\end{tabbing}

%[[[handout]]]
\begin{tabbing}
XXX\=XXX\=XXX\=XXX\=XXXXXXXXXXXXXXXXXXXXX\=    \kill
Given: $M = (Q,Q_0,\delta)$ is a state machine. \\
Prove: Every execution of $M$ has at most $k$ steps. \\
1. $f: Q \rightarrow N$ is a termination function for $M$. \\
2. $\forall q \in Q_0 (f(q) \leq k)$ \\
3. QED
\> \> \> \> \> Time bound theorem
\end{tabbing}

%[[[handout]]]
\begin{tabbing}
XXX\=XXX\=XXX\=XXX\=XXXXXXXXXXXXXXXXXXXXX\=    \kill
Given: $M = (Q,Q_0,\delta)$ is a state machine. \\
Prove: Every execution of $M$ is finite. \\
1. There exists a termination function for $M$. \\
2. QED
\> \> \> \> \> Termination theorem
\end{tabbing}

\end{document}

\endinput

