\section{Frames and Variable Names}
In \S\ref{s-transf}, we viewed a command
as a function from a state to a set of outcomes,
and a condition as a predicate on states.
In this treatment, the view of a state was abstract.
As discussed in \S\ref{s-mcc},
there are various ways in which a full treatment needs
to be more concrete, namely
\begin{itemize}
\item referring to program variables
\item having conditions in a form
allowing substitution for a program variable
\item specifying a frame for a command
\end{itemize}
In this section we discuss those abstract command constructors which
require us to address these issues.
In our Isabelle model, the program variable names are of type \verb|'n|
(eg, strings) and they take values of type \verb|'v|,
where \verb|'n| and \verb|'v| are Isabelle type variables.
As a state is an assignment of variables to values,
we have the type definition $\state = \name \to \val$, or,
in Isabelle, \verb|state = "'n => 'v"|.
\subsubsection{indeterminate assignment}
\cite[\S 12]{Dunne-CATS}
Where $x$ is a (list of) variables, and $P$ is a predicate,
the command $x : P$ assigns values to the variable(s) in $x$
in any way such that the change of state satisfies $P$.
More precisely, if $\alpha$ is the ``current alphabet''
(the set of variables whose names are currently ``in scope''),
and $x_0$ is the set of variable names in $x$, but with subscript 0 added,
then $P$ is a predicate on $\alpha \cup x_0$.
(The paper \cite{Dunne-CATS} says $\alpha \cup \alpha_0$ --
we comment on this below).
The subscripted variable names represent the values of those variables
before the command is executed.
%
We model such a $P$ as a relation on states, so we define this command as
\begin{verbatim}
"indetass ?vars ?P ?state ==
Term ` ((?P Int chst ?vars) `` {?state})"
\end{verbatim}
where \verb|chst ?vars| means the set of pairs of states
which differ only in the variables \verb|?vars|,
\texttt{f ` X} means the image of the set \verb|X| under the function \verb|f|,
and \texttt{r `` X} means the ``image'' of \verb|X| under the
relation \verb|r|, ie,
$\{y \;|\; (x, y) \in r \mbox{ for some } x \in X\}$.
% and \texttt{Collect (?P ?s)} means
% $\{s' \;|\; P\ s\ s'\}$.
%$\{s' | P\ s\ s' \land s' \in \texttt{chst ?vars}\ s\}$.
Although Dunne does not give the \wlp\ for indeterminate assignment,
Lermer, Fidge \& Hayes \cite{lfh} (who use the notation $x:[P]$
for Dunne's $x:P$) give \wlp\ and \sp\ for it.
When we omit reference to contexts, their formulae are as follows,
where $x'$ refers to the value(s) of variable(s) $x$ after the
execution of a command.
$$
\wlp (x:Q, R) = \forall x'. Q \to R[x := x'] \qquad
\sp (x:Q, R) = (\exists x. R \land Q)[x' := x]
$$
These are difficult to express in Isabelle.
This is because $\exists x. \ldots$ means ``for some values $x$,
which, when taken to be the values of variables $x$, \ldots''.
This is, in a sense, an overloading of the symbol $x$, which
complicates the formalisation.
However, we derived the following results for the
\wlp\ and \sp\ of indeterminate assignment,
which are in a form fairly close to the expressions above.
We use a function \texttt{setvars},
of type $\name\ \set \to \state \to \state \to \state $,
which resets the values of variables in the given set,
and we refer to a second state \texttt{primed} to refer to the
values in $x'$.
\begin{verbatim}
setvars ?vars ?primed ?state ?str ==
if ?str : ?vars then ?primed ?str else ?state ?str
indetass_wlp' = "wlpm (indetass ?x ?Q) ?R ?state =
(ALL primed. (?state, setvars ?x primed ?state) : ?Q -->
?R (setvars ?x primed ?state))"
indetass_slp' = "slpm (indetass ?x ?Q) ?R ?primed =
(EX state. (setvars ?x state ?primed, ?primed) : ?Q &
?R (setvars ?x state ?primed))"
\end{verbatim}
% indetass_wlp = "wlpm (indetass ?x ?Q) ?R ?state =
% (ALL primed. (?state, primed) : ?Q Int chst ?x --> ?R primed)"
% indetass_slp = "slpm (indetass ?x ?Q) ?R ?final =
% (EX init. (init, ?final) : ?Q Int chst ?x & ?R init)"
\subsubsection{prd}
\cite[\S 10]{Dunne-CATS}
The ``before-after'' predicate \prd\ specifies conditions under which
the command \emph{may} terminate in a state where
variables have certain given values.
Dunne defines this as
$$\prd\ (A) \equiv \lnot \wlp\ (A, x \not = x')$$
where $x'$ are new (logical) variables corresponding to the program variables
$x$.
We define \verb|prds| and \verb|prdm|, as
\begin{verbatim}
prds ?vars ?primed ?A ==
Not o wlpm ?A (%st. EX str:?vars. st str ~= ?primed str)
prdm ?primed ?A == Not o wlpm ?A (%st. st ~= ?primed)
\end{verbatim}
where \verb|?primed|, of type \textit{state}, represents the values $x'$,
and \verb|prdm| is a simpler version of \verb|prds| for use when $x$ can
be taken to be all variable names.
% As a sort of inverse to this definition, Dunne gives
Dunne also gives \wlp\ in terms of \prd\ as
$\wlp\ (A, Q) = \forall x'. \prd\ (A) \Rightarrow Q [x := x']$
which we prove as
\begin{verbatim}
wlp_prd = "wlpm ?A ?Q ?state =
(ALL primed. prdm primed ?A ?state --> ?Q primed)"
\end{verbatim}
In \cite[\S 9]{Dunne-case} Dunne states the result
$\prd\ (x : P) = P [ x_0,x := x,x' ]$.
We proved a corresponding result for the special case where $x$ represents all
variable names
\begin{verbatim}
indetass_prd = "prdm ?primed (indetass UNIV ?P) ?state =
((?state, ?primed) : ?P)"
\end{verbatim}
but found that we could not prove the stated result generally.
% if \verb|UNIV| (which means the universal set for its type)
% is replaced by an arbitrary set of variable names.
It turned out that Dunne's result requires that $P$
be a predicate on $\alpha \cup x_0$, not on
$\alpha \cup \alpha_0$ (as stated in the paper).
This is another example of the common situation that
attempting to prove such results formally
detects points such as this which can easily be overlooked
in an informal treatment.
\subsubsection{unbounded choice}
\cite[\S 7]{Dunne-CATS}
The command $(@z. A)$ means that variable $z$ is to be set to any value
and then $A$ is to be executed. But $z$ is to be a ``local'' variable in $A$;
if, for example, $Q$ contains $z$, then it is a \emph{different} $z$ from
that in $A$. In other words, the notation correctly reflects that
$z$ behaves as normal for a bound variable (it can be $\alpha$-converted
with no change in meaning).
So we model this command as follows:
\begin{itemize}
\item set variables $z$ to arbitrary values, using \texttt{setvars}
\item execute $A$
\item reset variables $z$ to their initial values, using \texttt{revert}
\end{itemize}
\begin{verbatim}
revert ?vars ?A ?initst ==
mapos (setvars ?vars ?initst) (?A ?initst)
at ?vars ?A ?initst ==
let initptf = %primed. setvars ?vars primed ?initst;
initptc = %x. UNION UNIV (?A o initptf)
in revert ?vars initptc ?initst
\end{verbatim}
Here, $\texttt{UNION UNIV}\ F = \bigcup_x F \;x$,
and \texttt{mapos} is the monadic ``map'' function:
% $\texttt{mapos} \;f\; \textit{ocset} =
% \{\textit{mapo} \;f\; s \;|\; s \in \textit{ocset} \}$, where
\begin{eqnarray*}
\textit{mapos} \;f\; \textit{ocset} & = &
\{\textit{mapo} \;f\; s \;|\; s \in \textit{ocset} \} \\
\textit{mapo} \;f\; (\texttt{Term} \;s) & = & \texttt{Term} \;(f \;s) \\
\textit{mapo} \;f\; \texttt{NonTerm} & = & \texttt{NonTerm}
\end{eqnarray*}
We then proved
\begin{verbatim}
at_trm = "trmm (at ?vars ?A) = allvars ?vars (trmm ?A)"
\end{verbatim}
where \texttt{allvars vars} $B\ s$
means that for any other state $s'$ obtained by taking $s$
and setting the variables \texttt{vars} to any values,
$B\ s'$ holds.
Since Dunne gives $\wlp\ (@z. A, Q) = \forall z.\ \wlp\ (A, Q)$,
we tried to prove
\begin{verbatim}
wlpm (at ?vars ?A) ?Q = allvars ?vars (wlpm ?A ?Q)
\end{verbatim}
but could not.
This reflected the fact that the formula for $\wlp\ (@z. A, Q)$
given by Dunne assumes that $Q$ does not involve $z$.
(As noted above, the $\alpha$-convertibility of $z$ in $@z. A$
means that we can sensibly assume this).
In fact we proved the more complex results
\begin{verbatim}
at_wlp = "wlpm (at ?vars ?A) ?Q ?st = (ALL nst.
wlpm ?A (?Q o setvars ?vars ?st) (setvars ?vars nst ?st))"
at_slp = "slpm (at ?vars ?A) ?Q ?st = (EX nst.
slpm ?A (?Q o setvars ?vars ?st) (setvars ?vars nst ?st))"
\end{verbatim}
% (ALL nst: chst ?vars `` {?st}.
% wlpm A (Q o setvars ?vars ?st) nst)"
% (EX st: chst ?vars `` {?nst}.
% slpm ?A (?Q o setvars ?vars ?nst) st)"
% at_wlp = "wlpm (at ?vars ?A) ?Q ?st =
% allvars ?vars (wlpm ?A (?Q o setvars ?vars ?st)) ?st"
% at_wlp = "indep ?vars ?Q ==>
% wlpm (at ?vars ?A) ?Q = allvars ?vars (wlpm ?A ?Q)
% where \texttt{indep} $z \ Q$ means that $Q$ is ``independent'' of $z$.
% As $Q$ is a semantic expression, not a syntactic one (see \S\ref{s-ass}),
% ``independent'' was defined to mean that changing $z$ does not change $Q$.
Lermer, Fidge \& Hayes \cite{lfh} give a similar command
(using `\textbf{var}' rather than `@').
Their framework involves typed variables and execution of a command in a
``context'', but if these aspects are removed, their expressions amount to
\begin{eqnarray*}
\wlp (@z. A, Q) & = & (\forall z. \wlp\ (A, Q[z := y]))[y := z] \\
\sp (@z. A, Q) & = & (\exists z. \sp\ (A, Q[z := y]))[y := z]
\end{eqnarray*}
where $y$ denotes new variables which do not appear (free) in $A$ or $Q$.
We now compare these results with ours.
\begin{enumerate}
\item \label{exp1}
Firstly, while $Q[z := y]$ refers to the textual substitution of
variable(s) $y$ for variable(s) $z$, we can interpret it as follows:
$Q[z := y]\ s$ means take state $s$, assign the \emph{values} $y$
(ie, treating $y$ as \emph{logical} variables)
to the \emph{program} variables $z$, and then apply
the predicate $Q$ to the resulting state.
Thus we can say $Q[z := y] = Q \circ \setvars\ z\ y$,
noting that the $y$ on the right-hand side is an assignment of values
to \emph{all} variables -- the $y$-values outside $z$ are simply not used.
\item \label{exp2}
Next we interpret $(\forall z. P)\ s$, where $P$ is a predicate on states.
This means that $P\ s'$ holds for every state $s'$ which is obtained
from $s$ by setting the program variables $z$ to other values $x$.
That is, $(\forall z. P)\ s = \forall x.\ (P\circ \setvars\ z\ x)\ s$.
\item \label{exp3}
Finally, we need to interpret $R[y := z] s$, for $R$ a predicate
containing the logical variable(s) $y$.
This requires replacing occurrences of $y$ in $R$ with the values,
in the state $s$, of the program variables $z$.
Fortunately, we find that $y$ only appears in the sub-expression
$\setvars\ z\ y$ (the function which resets $z$ to $y$ in a state);
in this particular expression, replacing $y$ by the values of $z$ in $s$
gives simply $\setvars\ z\ s$.
We could also say we get $\setvars\ z\ (\setvars\ z\ s\ y)$,
which we have proved (as \verb|setvars_set|) equal to $\setvars\ z\ s$.
\end{enumerate}
Thus the following shows the equivalence of our results to those in \cite{lfh}.
$$
\begin{array}{rcl@{\qquad \qquad}r}
\lefteqn{(\forall z. \wlp\ (A, Q[z := y]))[y := z] s} \\[-1ex]
&=& (\forall z.\ \wlp\ (A, Q\circ \setvars\ z\ y))[y := z] s
& \mbox{(by (\ref{exp1}))} \\[-1ex]
&=& \forall x.\ (\wlp\ (A, Q\circ \setvars\ z\ y) \circ
\setvars\ z\ x)[y := z] s & \mbox{(by (\ref{exp2}))} \\[-1ex]
&=& \forall x.\ \wlp\ (A, Q\circ \setvars\ z\ s) (\setvars\ z\ x\ s)
& \mbox{(by (\ref{exp3}))}
\end{array}
$$
\subsection{Assignment; the Syntactic View} \label{s-ass}
As noted in \S\ref{s-mcc},
$\wlp (x := E, Q) = Q[x := E]$, which is only meaningful when
$Q$ is some structure in which we can define substitutions
(although we have imitated $Q[x := E]s$ by $Q s'$ where $s'$ is the state
which is the same as $s$ except that the variable $s$ is assigned the
value of $E$).
So we have defined types for the abstract-syntax-tree version of
expressions (\verb|exp|) and boolean expressions (\verb|bexp|), thus:
\comment{
datatype exp = Num nat datatype bexp = Eq exp exp
| Var string | Lt exp exp
| Pluss exp exp | Le exp exp
| Minus exp exp | Gt exp exp
| Timess exp exp | Ge exp exp
| Nott bexp
| T
| F
| And bexp bexp
| Or bexp bexp
| Imp bexp bexp
}
\begin{verbatim}
datatype ('n,'v) exp = Val 'v
| Op "'v list => 'v" "('n,'v) exp list"
| Var 'n
datatype ('n,'v) bexp = Rel "'v list => bool" "('n,'v) exp list"
| BRel "bool list => bool" "('n,'v) bexp list"
\end{verbatim}
Thus an expression is a simple value, or an operation on values
together with an argument list, or a program variable.
A boolean expression is a relation on values together with an argument list
of value expressions,
or a boolean function together with an argument list of boolean expressions.
We defined substitution functions, of the following types
\begin{verbatim}
expSub :: "'n => ('n,'v) exp => ('n,'v) exp => ('n,'v) exp"
bexpSub :: "'n => ('n,'v) exp => ('n,'v) bexp => ('n,'v) bexp"
\end{verbatim}
where (for example) $\texttt{expSub} \ x \ E \ M$ means $M[x := E]$.
We also defined functions \texttt{expMng} and \texttt{bexpMng}
to translate an expression (type \aexp\ or
\bexp\ -- which we will call a \textbf{syntactic} expression)
to the corresponding function of type $\state \to \val$ or
$\state \to \bool$ (which we will call a \textbf{semantic} expression,
calling it the ``meaning'' of the syntactic expression).
Obviously, distinct syntactic expressions may have the same meaning, and
therefore the ``='' symbol in a proposition of the form
``$\wlp\ (A, Q) = \ldots$'' can only be
sensibly interpreted as equality of semantic expressions,
notwithstanding that in ``$\wlp (x := E, Q) = Q[x := E]$'',
the right-hand side is only meaningful as a syntactic expression.
We can also refer to syntactic and semantic \emph{commands}.
\begin{verbatim}
expMng :: "('n,'v) exp => ('n,'v) state => 'v"
bexpMng :: "('n,'v) bexp => ('n,'v) state => bool"
\end{verbatim}
We can then prove the following results,
and corresponding ones for boolean expressions.
% (in effect) the result for $\wlp (x := E, Q)$, in the form
\begin{verbatim}
subLemma = "expMng (expSub ?x ?E ?Q) ?state =
expMng ?Q (?state(?x := expMng ?E ?state))"
sub_equiv = "expMng ?Q = expMng ?R -->
expMng (expSub ?x ?E ?Q) = expMng (expSub ?x ?E ?R)"
\end{verbatim}
Here $f(x \verb|:=| E)$ is Isabelle notation for
the function that is like $f$ except that its value at
argument $x$ is $E$.
The first of these results relates substitution for a variable in an
expression to assignment to that variable in the state.
The second expresses that if two syntactic expressions
have the same meaning, then the results of making the same substitution in
the two of them also have the same meaning.
(Thanks to Dunne for pointing out the need for this result).
We are now in a position to define assignment and prove its properties.
We define \verb|assignv| and \verb|assigne| for the assignment, to a variable,
of a value and a (semantic) expression respectively.
We also define \verb|assignvs| for the assignment of values
to a set of variables.
\begin{verbatim}
assignv ?var ?n ?state == {Term (?state(?var := ?n))}
assigne ?var ?E ?state == assignv ?var (?E ?state) ?state
assignvs ?vars ?primed ?state ==
{Term (setvars ?vars ?primed ?state)}
\end{verbatim}
We can then prove \verb|ass_trm|
(which is trivial -- an assignment terminates), and
\verb|ass_wlpl|, which says $\wlp (x := E, Q) = Q[x := E]$.
Although we can prove \verb|ass_wlp|,
which is at the level of semantic expressions and conditions, this is trivial,
as it follows directly from the definitions.
\begin{verbatim}
ass_wlp = "wlpm (assigne ?x ?E) ?Q ?st = ?Q (?st(?x := ?E ?st))"
ass_wlpl = "wlpm (assigne ?x (expMng ?E)) (bexpMng ?Q) =
bexpMng (bexpSub ?x ?E ?Q)"
\end{verbatim}
\subsection{Normal Form}
In \cite[\S 7.1]{Dunne-case}
Dunne gives the following result, giving a ``normal form'' for
an abstract command $A$.
$$A = \trm\ (A) \;|\; @x'. \prd\ (A) \to x := x'$$
Here $x$ is the frame of $A$ (which we first take to be the entire
current alphabet of variable names), and
$x'$ is a corresponding set of logical variables, with names primed.
For this purpose we want somewhat different definitions of $@$ and of $A$,
involving a set of logical variables $x'$, one for each program variable.
So again we use a second state function \texttt{primed},
which gives the values of these logical variables,
and $A$ will depend on both state functions.
\begin{verbatim}
atd ?Ad ?state == UN primed. ?Ad primed ?state
\end{verbatim}
Here \verb|?Ad| is not a semantic command, but a function which, given
a ``primed'' state as argument, returns a semantic command.
Then also the assignment $x := x'$
(where $x$ represents \emph{all} variables)
becomes the replacing of state $x$ by ``state'' $x'$.
Thus we prove the following corresponding result.
\begin{verbatim}
ACNF = "?A = precon (trmm ?A)
(atd (%primed. guard (prdm primed ?A) (%st. {Term primed})))"
\end{verbatim}
We also proved a corresponding result for the case where $x$ is a proper subset
of all variables.
Here Dunne's result requires that $A$ does not change variables
outside the set $x$.
Rather than specify this requirement as such, we proved a result whose
left-hand-side means ``A restricted to $x$'', that is, as though
you executed $A$ and then
reset the variables outside $x$ to their original values.
\begin{verbatim}
ACNFs = "revert (- ?x) ?A = precon (trmm ?A)
(atd (%primed. guard (prds ?x primed ?A) (assignvs ?x primed)))"
\end{verbatim}
\subsection{Frames}
In Dunne's formulation \cite[\S 7]{Dunne-CATS},
each abstract command comes decorated with a frame,
and the frame of the new command is defined individually
for each abstract command constructor: for example
$$\frm\ (A \Box B) = \frm\ (A \# B) = \frm(A) \cup \frm(B)$$
However we are unable to give an exact semantic
meaning to the frame in a similar sense
to the meaning we have given to commands so far.
The frame may be thought of as a set of variables ``potentially''
set by a command, but it can
be larger than the set of variables actually set by the command.
The frame may be smaller than the set of variables read by the command,
and two commands which have the same semantic meaning can have different
frames.
Accordingly we could not attempt to prove the statements about frames
given by Dunne in his definitions of abstract commands from our
operational model, in the way we have done for their \wlp\ and \trm\
conditions.
The best one could do is to attempt to prove that for any abstract command
the frame of the result \emph{contains} the set of variables which are
changed by the command.
However this does not look at all difficult in any case, and so we have
not included frames in our model.
\subsubsection{parallel composition}
\cite[\S 12]{Dunne-CATS}
This is the only abstract command operator
whose meaning depends on the frames of its operands.
The command $A || B$ executes $A$ and $B$, independently,
each on its own copy of the variables in its frame,
and waits until both have terminated.
(Thus, non-termination is a possible outcome of $A || B$ if it is
possible for either $A$ or $B$).
We say a new state resulting from $A$ is \emph{compatible}
with a new state resulting from $B$ if these new states agree on
the values they give to the variables in $\fram (A) \cap \fram (B)$.
Then, for each $(s_A, s_B)$, where $s_A$ and $s_B$ are compatible new states
resulting from $A$ and $B$ respectively, there is an
outcome $\texttt{Term}\ s_{AB}$ of $A || B$, where $s_{AB}$ is given by:
\begin{itemize}
\item the new values of variables in $\fram (A) \cap \fram (B)$ are as in $s_A$
(or $s_B$),
\item the new values of variables in $\fram (A) \backslash \fram (B)$ are as in
$s_A$, and
\item the new values of variables in $\fram (B) \backslash \fram (A)$ are as in
$s_B$.
\end{itemize}
Dunne defines $A || B$ by
\begin{eqnarray*}
\trm (A || B) & = & \trm (A) \land \trm (B) \\
\prd (A || B) & = & \prd (A) \land \prd (B)
\end{eqnarray*}
but the latter formula
contains an implicit reference to the frames of the commands.
It is interesting to note that if $A$ is infeasible, and $B$
is feasible but does not terminate, then $A || B$
is feasible but does not terminate.
We consider first a version of this command for which the frame is the
entire set of variables, defined by \verb|pcomp_def| and \verb|pcomprs_def| ;
for these, we prove the formulae just mentioned,
as \verb|pcomp_prd| and \verb|pcomp_trm|.
We also prove as, \verb|pcomp_wlp|, a result (communicated by Dunne)
$$\wlp\;(A || B)\;Q\;s =
\exists Q_1 \;Q_2. (\forall t. Q_1\;t \land Q_2\;t \Rightarrow Q\;t)
\land \wlp(A,Q_1)\;s \land \wlp(B,Q_2)\;s$$
Unusually, we have explicitly referred to states $s$ and $t$
in this statement of the result to emphasize that
the choice of $Q_1$ and $Q_2$ depends on the state $s$.
%
% \begin{verbatim}
% pcomp_def = "pcomp ?A ?B ?state ==
% pcomprs (?A ?state) (?B ?state)"
%
% pcomprs_def = "pcomprs ?cr1 ?cr2 ==
% ?cr1 Int ?cr2 Un {NonTerm} Int (?cr1 Un ?cr2)"
% \end{verbatim}
The following definition of $A || B$ takes into account the
frames of $A$ and $B$.
Firstly, \verb|pccomb| combines two states (resulting from $A$ and $B$)
if they are compatible.
\begin{verbatim}
"pccomb ?frA ?frB ?initst (?stA, ?stB) =
(let compat = ALL str:?frA Int ?frB. ?stA str = ?stB str;
combst = %str.
if str : ?frA then ?stA str
else if str : ?frB then ?stB str else ?initst str
in if compat then {Term combst} else {})"
"pcompfr ?frA ?A ?frB ?B ?state ==
let tsA = {st. Term st : ?A ?state};
tsB = {st. Term st : ?B ?state};
nont = {NonTerm} Int (?A ?state Un ?B ?state)
in nont Un UNION (tsA <*> tsB) (pccomb ?frA ?frB ?state)"
\end{verbatim}
Here \verb|(tsA <*> tsB)| means the set product of \verb|tsA| and \verb|tsB|.
We have a result \verb|pcomp_chk| which is a sanity check that,
where the frames of
$A$ and $B$ are the set of all variable names,
this definition is equivalent to the
one mentioned in the previous paragraph (a useful check,
since our first attempt at the definition above was erroneous).
Noting that Dunne's formula $\prd (A || B) = \prd (A) \land \prd (B)$
implicitly refers to the frames of the commands, we
prove it as \verb|pcompfr_prd|, as follows:
\begin{verbatim}
pcompfr_prd = "prds (?fA Un ?fB) ?primed (pcompfr ?fA ?A ?fB ?B) =
(prds ?fA ?primed ?A && prds ?fB ?primed ?B)"
\end{verbatim}