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

\input{./handout}

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

\begin{document}

\handout{11}{9 October 1995}{Seq Satisfies Set}
\begin{symbolfootnotes}
\footnotetext[0]{\copyright 1995 Jeannette M. Wing} 
\end{symbolfootnotes}

The motivation for this example is show you that when
you do ``object-oriented'' programming, you are really identifying
certain abstract objects (better known an {\em data abstractions} or
{\em abstract data types}) like sets, stacks, queues, symbol tables, etc..
You eventually have to realize (i.e., implement) these objects in a
real programming language in terms of either other abstract objects or
the language's built-in data objects like sequences, arrays, records, linked
lists, etc.  After you write your (concrete) implementation you are then faced
with
proving it correct with respect to the (abstract) specification.

Not surprisingly, these data objects (abstract or built-in) can
themselves be viewed as little state machines.  So, to show the correctness
of an implementation of an abstract object is very much like showing
that one state machine (the concrete one) satisfies another (the abstract one).

There are other proof techniques used to prove the correctness of the
implementations of abstract data types.  You may see them in the
Methods Course (when you learn about object-oriented programming)
and/or the Analysis course (when you learn about program verification).

\section{Abstract Machine: Set}

My Set abstract machine has the following interface:

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

\begin{verse}
Set = $($ \\
$\{ s: \{t\} \rightarrow set[int] \}$,\\
$\{ s: \{t\} \rightarrow set[int] | s(t) = \emptyset \}$,\\
$\{insert(i:int)/ok(), \ldots$ see above $\ldots , pick()/ok(int)\},$ \\
$\delta_A = \ldots$ see next page $\ldots$\\
$)$.
\end{verse}

Here are specifications of the actions, {\em insert, delete, card, member, and pick}.
\begin{spec}
\begin{tabbing}
\indent {\em insert}\={\em (i: int)/ok()}\\
            \>{\bf pre} $true$\\
            \>{\bf post} $t' = t \cup \{i\} $\\

\\
\indent {\em delete(i: int)/ok()}\\
            \>{\bf pre} $true$\\
            \>{\bf post} $t' = t \setminus \{i\} $\\
\\
\indent {\em card()/ok(int)}\\
            \>{\bf pre} $true$\\
            \>{\bf post} $t' = t \wedge result = \#t $\\
\\
\indent {\em member}{\em(i: int)/ok(bool)}\\
            \>{\bf pre} $true$\\
            \>{\bf post} $t' = t \wedge result = (i \in t)$\\
\\
\indent {\em pick()/ok(int)}\\
           \>{\bf pre} $t \neq \emptyset$\\
           \>{\bf post} $t' = t \wedge result \in t$
\end{tabbing}
\end{spec}

\section{Concrete Machine: Seq}

I've decided that I want to implement the Set machine in terms of a Seq
machine with the following interface:

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

\noindent I'm going to define the actions such that
the state where $q = \langle 3, 5, 5\rangle$ is unreachable.
You'll see why soon.

\begin{verse}
Seq = $($ \\
$\{ s: \{q\} \rightarrow seq[int] \},$\\
$\{ s: \{q\} \rightarrow seq[int] | s(q) = \langle\rangle\},$\\
$\{addh(i:int)/ok(), \ldots$ see above $\ldots , fetch(i: int)/ok(int)\},$ \\
$\delta_C = \ldots$ see next page $\ldots$\\
$)$.
\end{verse}

\noindent Seq's actions have the following specification:

\begin{spec}
\begin{tabbing}
\indent {\em addh}\={\em (i: int)/ok()}\\
            \>{\bf pre} $i \notin ran~ q$\\
            \>{\bf post} $q' = q \cat \langle i \rangle $\\
\\
\indent {\em remh()/ok(int)}\\
            \>{\bf pre} $q \neq \langle\rangle $\\
            \>{\bf post} $q = q' \cat \langle result \rangle$\\
\\
\indent {\em size()/ok(int)}\\
            \>{\bf pre} $true$\\
            \>{\bf post} $q' = q \wedge result = \#q $\\
\\
\indent {\em isin(i: int)/ok(bool)}\\
            \>{\bf pre} $true$\\
            \>{\bf post} $q' = q \wedge result = (i \in ran~ q)$\\
\\
\indent {\em fetch(i: int)/ok(int)}\\
           \>{\bf pre} $q \neq \langle\rangle \wedge i \in dom~q$\\
            \>{\bf post} $q' = q \wedge result = q~ i$
\end{tabbing}
\end{spec}

\section{Proof of Correctness}

Formally,
$RI$ and $AF$ are defined
over Seq's set of states, but it's going to be notationally convenient
(and I hope more understandable) if I denote each of these states
by the sequence value to which Seq's state variable, $q$, maps.
In other words, I should write something like:

\begin{center}
$RI( s(q) = \langle 3, 5, -1 \rangle ) = \ldots$
\end{center}

\noindent but instead I'm going to write:

\begin{center}
$RI(\langle 3, 5, -1 \rangle) = \ldots$
\end{center}

\subsection{Step 1}

I first need to define an abstraction function and a representation invariant.

\vspace{.15in}
\noindent {\em 1. Abstraction Function.}

Informally $AF$ takes an (ordered) sequence of elements and turns
it into an (unordered) set of the sequence's elements.
Formally,

\begin{verse}
$AF: seq[int] \pfun set[int]$\\
$AF(\langle\rangle) = \emptyset$\\
$AF(q \cat \langle e\rangle) = AF(q) \cup \{e\}$
\end{verse}

\noindent It is common for abstraction functions to be defined recursively like this.

Notice that this $AF$ is many-to-one.  There are many sequence values
that map to the same set value because we don't care what the order of
elements is in a set.  In fact, the orderedness property of sequences
is exactly the ``irrelevant'' property from which we abstract.  For
example,

\begin{verse}
$AF(\langle 3, 5, -1 \rangle) = \{3, 5, -1\}$\\
$AF(\langle 5, 3, -1 \rangle) = \{3, 5, -1\}$\\
$AF(\langle -1, 5, 3 \rangle) = \{3, 5, -1\}$
\end{verse}

\noindent These three different sequence values map to the same set value.

\vspace{.15in}
\noindent {\em 2. Representation Invariant.}

Notice that the {\em addh} action has a pre-condition that
checks whether the element to be inserted is already in the sequence.
Thus,
only sequence values that have no duplicate
elements serve to represent set values.  We have the following
representation invariant, which characterizes the domain of $AF$:

\begin{verse}
$RI: seq[int] \rightarrow bool$\\
$RI(q) = \forall 1 \leq i, j \leq \#q \bullet i \neq j \Rightarrow q~ i \neq q~ j$
\end{verse}

\noindent Informally I'll call this representation invariant, NoDups.
Thus we have,

\begin{verse}
\begin{tabbing}
$RI(\langle 3, 5, 5, -1\rangle) ~~~~~~$\=$= false~~~~~~~~~$\= 5 appears twice.\\
$RI(\langle 3,  5, -1\rangle)$\> $= true$\> NoDups\\
$RI(\langle\rangle)$\> $= true$\> The empty sequence is ok.
\end{tabbing}
\end{verse}

\noindent All those sequence values that $RI$ maps to {\em true} are legal
representations of set values.

IMPORTANT: Remember that there's a side proof that we need to do here.
We need to show that
the representation invariant is indeed an invariant.  That is, along
the lines of the proof technique described in the handout
on Reasoning About State Machines, we need
to show that the invariant is established in the initial states and preserved by each action.
I'll leave this part of the proof as an exercise to the reader.

Here's a picture illustrating that $AF$ is partial and many-to-one:

\centerline{\epsfbox{pictures/set-seq-af.ps}}

\subsection{Step 2}

Armed with $RI$ and $AF$,
I can now show the concrete machine satisfies the abstract one.

\vspace{.15in}
\noindent{\em 1. Initial condition.}

We need to show that each initial state of Seq maps to some initial
state of Set.
More formally,
we need to show that $AF(\langle\rangle) = \emptyset$.  This is obviously true
by the definition of $AF$.

\newpage
\noindent {\em 2. Commuting diagram for each Seq action.}

I need to show this diagram:

\centerline{\epsfbox{pictures/set-seq.ps}}

\noindent There are five cases, one for each Seq action.
I'll just do three actions, {\em addh}, {\em remh}, and {\em size}.

\vspace{.15in}
\noindent Case: {\em addh} satisfies {\em insert}.

We'll first consider the case where $i$ is not in the sequence
and then the case for when it is.

\indent Case 1: $i \notin ran~ q$

According to the post-condition for
Set's {\em insert} action we need to show that the set value for
$t'$
obtained
after doing an {\em insert} with argument $i$ is
$t \cup \{i\}$.  Seq's {\em addh} action 
has the effect of adding to the high end of the sequence
only if its argument $i$ is not already stored in the sequence.
Thus if $q$ is the value of the sequence before, then $q \cat \langle i\rangle$ is the value after.
In other words, we have:

\begin{verse}
\begin{tabbing}
\hspace{2em}\=$AF(\delta_C(q, addh(i)/ok()))$\hspace{2em}\= \\.
\>$= AF(q) \cat \langle i\rangle)$\>post-condition of {\em addh}\\
\>$= AF(q) \cup \{i\}$\>def'n of AF\\
\>$= t \cup \{i\}$\>since $t = AF(q)$\\
\>$= t'$\>post-condition of {\em insert}
\end{tabbing}
\end{verse}

\indent Case 2: $i \in ran~ q$

If $i$ is already in the sequence then no state transition
occurs and $q$ stays
the same.

%\begin{verse}
%\begin{tabbing}
%\hspace{2em}\=$AF(\delta_C(q, addh(i)/ok()))$\hspace{2em}\= \\
%\>$= AF(q')$\>def'n of $\delta_C$\\
%\>$= AF(q)$\>pre-condition of {\em addh} implies q' = q\\
%\>$= AF(q) \cup \{i\}$\>assumption that $i \in ran~ q$ and property about set union\\
%\>$= t \cup \{i\}$\>def'n of $AF$\\
%\>$= t'$\>def'n of $AF$
%\end{tabbing}
%\end{verse}
%
%\noindent The third step (going from $AF(q)$ to $AF(q) \cup \{i\}$)
%actually requires that we prove a lemma that
%says
%if $i$ is in a sequence then it is in the set that the sequence
%represents:
%
%\begin{lemma}
%$\forall q: seq[int] \bullet \forall i: int \bullet (i \in ran~q \Rightarrow i \in A(q))$
%\end{lemma}

\vspace{.15in}
\noindent Case: {\em remh} satisfies {\em delete}.

According to the post-condition of Set's {\em delete} action
the set value for $t'$ obtained after doing the {\em delete}
is the set with $i$ removed.  Seq's {\em remh} action has the effect
of removing and returning the high end of the original sequence $q$.
Informally speaking, it's this element
$result$, which we would ``pass to'' {\em delete}
as an argument.
In other words, given a particular
state transition involving {\em remh}, I am choosing a particular
state transition involving {\em delete}---the one for which {\em
result} is passed
as an argument.
We have:

\begin{verse}
\begin{tabbing}
\hspace{2em}\=$\delta_A(AF(q), delete(result)/ok())$\hspace{1in}\= \\
\>$= \delta_A(AF(q' \cat \langle result \rangle), delete(result)/ok())$\>post-condition of {\em remh}\\
\>$= \delta_A(AF(q') \cup \{result\}, delete(result)/ok())$\>def'n of $AF$\\
\>$= (AF(q') \cup \{result\}) \setminus \{result\}$\>post-condition of {\em delete} (and def'n of $\delta_A$)\\
\>$= AF(q')$\>properties about set union and set difference\\
\>$= t'$\>$t' = AF(q')$
\end{tabbing}
\end{verse}

\vspace{.15in}
\noindent Case: {\em size} satisfies {\em card}

Looking at the post-condition for Set's {\em card} action,
there are two things to show.

First,
we need to show that the value returned by the Seq's {\em size} action
is the size of the corresponding set (under $AF$).
Because of NoDups (the $RI$), we know that
the size of the sequence representing a set
is the size of the set it represents.
More formally, you would need to prove a lemma like:

\begin{lemma}
$\forall q: seq[int] \bullet (\#q = \#AF(q))$
\end{lemma}

%\noindent and you would definitely appeal to the NoDups representation
%invariant to prove the lemma.  For example,
%$\#\langle~3,~5,~5\rangle~\neq~\#\{3,~5\}$ but we know the
%sequence value $\langle 3, 5, 5\rangle$ is not a legal representation for sets.
%(Notice the lefthand side use of $\#$ is on sequences and the righthand
%side
%use is on sets.)

Second, we need to show
that {\em size} does not change the abstract value of the set
that $q$ represents.  More formally,

\begin{verse}
\begin{tabbing}
$q'$\= = $q$\\
$\Rightarrow$\>~~~~~~~~~~~~~~~~~~~~~~~~~~~~\=post-condition of {\em size}\\
$AF(q')$ $= AF(q)$\\
$\Rightarrow$\>\>$AF$ is a function.\\
$t'$\> $= t$
\end{tabbing}
\end{verse}

\noindent {\bf IMPORTANT}: Notice that we rely on the abstraction function
$AF$ on being a function here.  In the second step above, we apply
$AF$ to two equal things; since $AF$ is a function (and not a
relation), we know the result of applying $AF$ to two equal things
will result in two equal things.

\vspace{.2in}
For your homework, it's okay to give informal proofs like the ones I
give here.

\end{document}