\documentstyle[10pt,epsf,fuzz]{article}

\input{./handout}

\newtheorem{defn}{Definition}
\newenvironment{spec}{
 \vspace*{8pt}
 \begin{center}
 \begin{minipage}{5in}
 \renewcommand{\baselinestretch}{1}
 }{
 \end{minipage}
 \end{center}
 \vspace*{8pt}
}

\begin{document}

\handout{9}{9 October 1995}{Relating State Machines: Satisfies}
\begin{symbolfootnotes}
\footnotetext[0]{\copyright 1995 Jeannette M. Wing} 
\end{symbolfootnotes}

This handout discusses the problem of whether one machine {\em
satisfies} (in some sense) another.  It should be read simultaneously
(if that's possible!) with Handouts 10 and 11, which give specific
examples.

Just as there is not one standard notion of equivalence, there
is not one standard notion of ``satisfies.''  In this handout
we give a definition that is reasonable, representative, and used in practice.

There are three key ideas that this handout presents.

\begin{itemize}
\item A definition of {\em satisfies} in terms of a subset relationship
between behavior sets of two machines.

\item The notion of a mapping, called an
{\em abstraction function}, that relates states of one machine to
states of another.

\item A proof technique that uses the abstraction function in 
a ``commuting'' diagram  (see Section
\ref{sec:technique}) to relate state transitions of one machine
to state transitions of another.
\end{itemize}

\noindent Although our notion of {\em satisfies} and the proof technique
that I present here may seem specific to the model of state machines
that I have described so far, what's the most important idea
for you to learn from these handouts is the notion of an abstraction
function.  You will also see it again, in a different guise, when we
cover refinement in Z.

\section{Why Would You Care About ``Satisfies''?}

Suppose your favorite programming language does not support the notion
of a set (i.e., {\em set} is not a built-in type) and I asked you to
implement a set type in terms of the built-in types of your language,
e.g., sequences (or arrays, more likely).  This is a standard exercise
in programming with data abstraction.  For example, you might (1)
represent sets in terms of sequences and then (2) implement each set
operation in terms of operations on sequences and other built-in
types.  After you hand in your solution, I ask you to prove that your
representation using sequences satisfies the abstract set type.  How
would you respond?

What we really care about is the relationship
between a {\em concrete} state machine, $C$, and an {\em abstract}
state machine, $A$:

\centerline{\epsfbox{pictures/acbox.ps}}

\noindent where we usually read the arrow in one of many ways:

\begin{verse}
{\em C satisfies A.}\\
{\em C implements A.}\\
{\em C is a refinement of A.}\\
The program {\em C is correct with respect to} the specification $A$.
\end{verse}

\noindent $C$ and $A$ can be interpreted in many ways:

\begin{verse}
$C$ and $A$ are both state machines.\\
$C$ is a program and $A$ is a specification.\\
$C$ is an implementation and $A$ is a specification.\\
$C$ is a state machine and $A$ is a predicate.\\
$C$ and $A$ are both programs.\\
$C$ and $A$ are both specifications.\\
$C$ is an implementation and $A$ is an interface specification.\\
$C$ is a concrete data type and $A$ is an abstract data type.\\
$C$ is an Ada package body and $A$ is a package specification.\\
$C$ is a C function definition and $A$ is a C function declaration.\\
$C$ is a C++ class definition (implementation) and $A$ is a class declaration (interface).\\
$C$ is a high-level design and $A$ is a set of customer's requirements.\\
$C$ is a low-level design and $A$ is a high-level design.\\
$C$ is an implementation and $A$ is a low-level design.
\end{verse}

\section{What Does {\em Satisfies} Mean?}

\subsection{Binary Relations}
Consider a simpler problem of determining when one binary relation
{\em satisfies} another.  Suppose we have a specification for
a {\em square\_root} procedure:

\begin{spec}
\begin{tabbing}
\indent {\em square}\={\em\_root(x: int)/ok(int)}\\
\>{\bf pre} $~\exists i: int \bullet x = i \ast i$\\
\>{\bf post} $~x = result \ast result$
\end{tabbing}
\end{spec}

\noindent that denotes the binary relation:

\begin{center}
$R_A = \{(4, 2), (4, -2), (9, 3), (9, -3), (16, 4), (16, -4) \ldots \}$
\end{center}

I could choose to implement this procedure
such that I always return the positive square root of an integer.
Its relation is:

\begin{center}
$R_C = \{(4, 2), (9, 3), (16, 4)\ldots \}$
\end{center}

\noindent Informally, my implementation {\em satisfies} the specification
because
$R_C$ just narrows the possible choice of the integer returned
allowed by $R_A$ and
the implementation defines some value for each input integer
that is defined for the specification.

More formally, we have, given an abstract relation, $R_A$,
and a concrete relation, $R_C$:

\begin{defn}
$R_C$ {\bf satisfies} $R_A$ iff:

\begin{itemize}
\item $R_C \subseteq R_A$ and 
\item $dom~ R_C = dom~ R_A$.
\end{itemize} 

\end{defn}

The first property says that any pair in the concrete relation
is also an element of the abstract relation.  The second property
says that for each input that is related by $R_A$,
we want $R_C$ to be defined.  Without the second property,
$R_C$ could be empty and the {\em satisfies} relation would
hold\footnote{A very ``unsatisfying'' relation!}.

%By the way we have been writing specifications of actions for state
%machines,
%we can define each action to denote
%a binary relation on states.  That is, associated with each action is
%a set of pairs of states.  Henceforth, we will write
%for an action $a$ of machine $M$
%its associated relation as 
%$R_{M}^{a}$.

\subsection{State Machines}

Consider the two state machines,

\begin{verse}
$A = (S_A, I_A, A_A, \delta_A)$ \\
$C = (S_C, I_C, A_C, \delta_C)$ \\
\end{verse}

\noindent each denoting a behavior set, $Beh(C)$ and $Beh(A)$, respectively.
We take an event-based view of trace: Each trace is a sequence of
(invocation, response)
pairs and each pair represents a single execution of one of the
actions provided by the machine.
%Recall that an invocation is an
%action name plus argument values and a response is the name of the
%termination
%condition (normal or exceptional) plus the result (if any).
We assume for simplicity that there is a one-to-one correspondence
between the action names in the concrete machine to those in the abstract
machine and that we use a renaming function, $\alpha$, to define the
relationship:

\begin{verse}
$\alpha: A_C \rightarrow A_A$
\end{verse}

\noindent Using $\alpha$ we can relate each state transition involving
a $C$ action to a state transition involving an $A$ action.\footnote{
In all the examples that you will see the renaming function will be
obvious.  I'm being overly pedantic here.}

We define the {\em satisfies} relation as follows between two state
machines as follows:

\begin{defn}
$C$ {\bf satisfies} $A$ iff Beh(C) $\subseteq$ Beh(A).
\end{defn}

Since $Beh(C)$ is a set of traces and $Beh(A)$ is a set of traces, the
{\em satisfies} relation is satisfied if every trace in $Beh(C)$ is
in $Beh(A)$.  This means that $A$'s set can be larger; $C$'s set
reduces the choices of possible acceptable behaviors.

Why does this definition of {\em satisfies} make sense?  Viewing $C$
as an implementation of a design specification $A$, this definition
says that an implementor makes decisions that restrict the scope of
the freedom {\em allowed by} a design.  In other words, the
specification is saying what {\em may} or {\em is permitted} to occur
at the implementation level, not what {\em must} occur.  The
implementation narrows down the choice of what is allowed to happen.
For example, an implementation might reduce the amount of
nondeterminism allowed by the specification.

Thus, certainly having the behavior sets equal ($Beh(C) = Beh(A)$) is
too strong.  Having the subset relation go the other way ($Beh(A)
\subseteq Beh(C)$) cannot be right either; otherwise there may be
executions of the concrete machine that are not permitted by the
abstract one.

According to this definition of correctness the concrete machine with
the empty behavior would be a perfectly acceptable implementation
of an abstract machine.  Since the empty behavior is not very
satisfying, we normally assume that the set of initial states and the
state transition function for the concrete machine are both non-empty;
thus its behavior is non-empty.

The empty behavior case is the extreme case where the concrete machine
does not do anything bad (a safety property)\footnote{See end of
Handout on Reasoning About State Machines.} since it does not do anything at all; however, the machine also
does not do anything good (a liveness property).  Our
definition of {\em satisfies} does not require that our machine do
anything; the definition requires only that the machine does only allowed things.

\section{Showing One Machine Satisfies Another}

How do we show the {\em satisfies} relationship holds between
two state machines?
Given our two state machines,
$A = (S_A, I_A, A_A, \delta_A)$ and
$C = (S_C, I_C, A_C, \delta_C)$,
in general it is not
so straightforward to determine if $C$ {\em satisfies} $A$ because
their state sets, $S_A$ and $S_C$, may be different.
The proof technique we present uses an {\em abstraction function}
to relate these state sets\footnote{Much like we use the renaming
function
$\alpha$ to relate different actions sets.}.

\subsection{A Proof Technique}
\label{sec:technique}

There are two major steps in the proof technique for showing
one machine satisfies another.
\begin{enumerate}

\item The Creative (Intellectually Hard) Step.
\begin{itemize}
\item Define an {\em abstraction function}
\begin{center}
$AF: S_C \rightarrow S_A$
\end{center}
to relate concrete states with abstract states.

\item Define a {\em representation} (sometimes called {\em concrete})
invariant,
\begin{center}
$RI: S_C \rightarrow bool$
\end{center}
that characterizes the domain of $AF$.  This predicate prunes down the
set of concrete states, $S_C$, to only those of interest (only those
that represent some abstract state in $S_A$).
After you define this predicate, you must prove that it indeed is an
invariant.
You may use the technique presented in the Reasoning About
State Machines handout to show this.
\end{itemize}

\item The Checklist (Tedious) Step.
\begin{itemize}
\item For each $i_C \in I_C$ (for all initial states in $I_C$) show:
\begin{center}
$AF(i_C) \in I_A$
\end{center}
This requires showing that each initial state of the concrete machine
is some initial state of the abstract machine.

\item For each state transition $(y, c, y') \in \delta_C$
of the concrete machine $C$ where $y$ satisfies $RI$,
there must exist a state transition $(AF(y), \alpha(c), AF(y')) \in \delta_A$
of the abstract machine $A$.
To show this, it suffices to show
the following
commutative relationship holds:

\centerline{\epsfbox{pictures/commutative.ps}}

\noindent where $x = AF(y), x' = AF(y')$ and $a = \alpha(c)$.
Here's how to read the diagram: Put both index fingers at the concrete
state $y$; move your right one to the right (performing the concrete
action $c$) and then up (applying $AF$ to the new concrete state $y'$);
move your left one up (applying $AF$ to $y$) and then to the right
(performing the corresponding abstract action $a = \alpha(c)$; you
should end up in the same place: the abstract state, $x'$.

\end{itemize}
\end{enumerate}

Please brand this commuting diagram on your brain.

\subsection{Rationale}

Why does this proof technique make sense?  The technique should smell
familiar.  It's inductive in nature.  There's a base case (``for each
initial state $\ldots$'') and an inductive step, defined in terms of
all possible action instances (``for each state transitions
$\ldots$'').  As before, because the action sets are finite, we can do
a big case analysis, one action per case, in the inductive step.
\begin{itemize}
\item In the base step, notice there is no requirement that all initial
states of the abstract machine be covered.  So, there may be some
abstract executions that have no corresponding concrete execution
since we could not even get started.  This is okay since we only
need to show a subset relationship between behavior sets.

\item The intuition behind the inductive step is that if a state transition
can occur in the concrete machine then it must be {\em allowed to} occur in
the abstract machine.
%This may seem counterintuitive to you.
%You might think that for each abstract state transition
%we should find a way to ``implement'' it in terms of concrete
%state transitions.  But remember, our interpretation of the abstract
%machine (the specification) is that it says what {\em may}, not {\em
%must}
%occur, in the concrete machine (the implementation).
%
If we show the inductive step for all state transitions in
the concrete machine, then we will have shown it for all of its
possible executions.
(Notice that in showing the commuting diagram for each action of the
concrete
machine, we
are really showing it for each state transition that involves that action.)
\end{itemize}

After showing the base case and inductive step,
we will have
shown that each trace in the behavior set of the concrete machine has a
corresponding (modulo the abstraction function) trace in the
behavior set of the abstract machine.  Hence, the behavior set of
the concrete machine is a subset of the behavior set of the abstract
machine (modulo the abstraction function),
which is what we needed to prove.

Aside: In our proof technique, because of our simplistic
way of associating actions in one machine to another
(through the one-to-one function $\alpha$) we are associating a single
state transition in $C$ to a single state transition in $A$.
More generally, a state transition in $C$
might map to a {\em sequence} of transitions in the abstract machine
$A$.  This generalization is especially needed for proving concurrent
state machines correct and/or dealing with state machines with
internal as well as external actions.  We won't be using this
generalization at all.

\subsection{Abstraction Functions and Representation Invariants}

An abstraction function maps a state of the concrete machine to a
state of the abstract machine.  It explains how to interpret each
state of the concrete machine as a state of the abstract machine.  It
solves the problem of the concrete and abstract machines having
different
sets of states.

Since the abstraction function is a function, we can rely on
the
substitution property:
If $AF$ is a function and we know $x = y$ then we know $AF(x) = AF(y)$.
If $AF$ were a more general kind of relation, this property would not
necessarily hold.

You might think that the abstraction function should map the other
way, explaining how to represent each state of the abstract machine.
This is usually not a good idea, in large part because there is often
more than one way of representing each state of the abstract machine.
For example, suppose I represent a set by a sequence.  Then
many {\em different} sequences, e.g.,
$\langle 3, 5, -1 \rangle$,
$\langle 5, 3, -1 \rangle$,
$\langle -1, 5, 3 \rangle$,
$\langle 3, 5, 5, -1 \rangle$, could (given the appropriate
definition of $AF$ and $RI$) all represent the {\em same} set
$\{3, 5, -1\}$.

In other words, $AF$, in general, is many-to-one.

$AF$ may be partial.  Not all states of the concrete
machine may represent a ``legal'' abstract state.
For example, in the integer-modulo7 example, integers
not within 0..6 are not ``legal'' representations of
days of the week.  The representation invariant serves to restrict
the domain of the abstraction function.  We may assume that for any concrete state
for which the representation invariant does not hold, $AF$ is undefined.

Finally, $AF$ is not necessarily onto.  There may be states of the abstract
machine that are not represented by any state of the concrete machine.
This can be true of initial states as well.  In the context of
showing that one machine adequately implements another, this may sound
strange to you; we say more on {\em adequacy} in Section \ref{sec:variations}.

Putting everything together, we have the final diagram:

\centerline{\epsfbox{pictures/ac.ps}}

\noindent where the
bottom {\em unshaded} region represents the domain of $AF$ and the
top {\em unshaded} region represents its range.

\subsection{Variations on a Theme}
\label{sec:variations}

\vspace{.15in}
\noindent {\em Adequacy}

In this handout
we explicitly stated that
$AF$ need not be surjective (onto).
Were we to require $AF$ to be surjective, then we would require
that every abstract state have some concrete representation, i.e.,
that $AF$ is {\em adequate}.  Requiring $AF$ to be adequate makes very good sense
since you might like to know that every abstract state you have
modeled is implemented by some concrete state.
Some refinement methods like VDM require that $AF$ be adequate.
And, in proving the correctnesss of an abstract data type,
we usually require $AF$ to be adequate for the concrete representation type.

As mentioned, we also do not require adequacy in the
sense
of having every state transition of $A$ be implemented in terms
of one in $C$.  Rather, we only require that every
state transition in $C$ relate to some state transition of $A$.
($C$ cannot do anything not permitted by $A$.)
This laxity is in contrast to
how we defined whether one binary relation, $R_C$,
{\em satisfies} another, $R_A$; we required that for each input
related by $R_A$, $R_C$ should be defined.  This requirement gets
at the {\em adequacy} of $R_C$ viewed as an implementation of $R_A$.

Taking this last point to an extreme, we do not even require that every action
in $A$ actually be ``implemented'' by some action (or sequence
of actions) in $C$.  In other words there can be state transitions,
all associated with a particular action of $A$, that have no correspondence
are not adequately represented) in $C$.

You will see later in the course
when we cover Z and CSP that other state machine-based
models impose different kinds of adequacy restrictions
in defining a
{\em refinement}/{\em correctness} relation between two machines.

\vspace{.15in}
\noindent {\em Abstraction Relations}

Some people prefer to use abstraction {\em relations} or
abstraction {\em mappings}
more generally than functions.  There are examples where it is easier,
more convenient, or more natural to map a concrete state to a set of
abstract states.  As mentioned, however, you would
lose the substitution property of abstraction functions.

\vspace{.12in}
\noindent {\em Auxiliary Variables}

Sometimes it is not so straightforward to prove a concrete
machine satisfies an abstract machine in terms of just the state
variables of the concrete machine.  In this case, you need
to introduce {\em auxiliary variables} (sometimes called
{\em dummy variables} or {\em history variables} in the literature).
The need for auxiliary variables in such proofs is especially common
for reasoning about concurrent programs.

\end{document}