\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
  in which we can substitute 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 strings
and they take natural number values.
As a state is an assignment of variables to values,
we have the type definition
\verb|state = "string => nat"|

\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 function on two states, so our definition of 
this command is
\begin{verbatim}
indetass ?vars ?P ?s == Term ` (Collect (?P ?s) Int chst ?vars ?s)
\end{verbatim}
where \verb|chst ?vars ?s| means the set of states
which differ from \verb|?s| only in the variables \verb|?vars|,
\texttt{f ` X} means $\{f\ x \;|\; x \in X\}$, 
and \texttt{Collect (?P ?s)} means 
$\{s' \;|\; P\ s\ s'\}$.
%$\{s' | P\ s\ s' \land s' \in \texttt{chst ?vars}\ s\}$.

\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.
We define \verb|prds| and \verb|prdm|, as
\begin{verbatim}
prds ?strs ?dashed ?Am ==
   Not o wlpm ?Am (%st. EX str:?strs. st str ~= ?dashed str)
prdm ?dashed ?Am == Not o wlpm ?Am (%st. st ~= ?dashed)
\end{verbatim}
where \verb|?dashed|, 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
$\wlp\ (A, Q) = \forall x'. \prd\ (A) \Rightarrow Q [x := x']$
which we prove as
\begin{verbatim}
wlp_prd = "wlpm ?Am ?Qm ?state =
  (ALL dashed. prdm dashed ?Am ?state --> ?Qm dashed)"
\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 ?dashed (indetass UNIV ?P) ?state = ?P ?state ?dashed" 
\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
\item execute $A$
\item reset variables $z$ to their initial values
\end{itemize}

\begin{verbatim}
setstrs ?strs ?strfun ?state ?str ==
   if ?str : ?strs then ?strfun ?str else ?state ?str
revert ?strs ?Am ?initst ==
   mapos (setstrs ?strs ?initst) (?Am ?initst)
at ?strs ?Am ?initst ==
   let initptf = %strfun. setstrs ?strs strfun ?initst;
      initptc = %x. UNION UNIV (?Am o initptf)
   in revert ?strs 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 ?strs ?Am) = allstrs ?strs (trmm ?Am)"
\end{verbatim}
where \texttt{allstrs strs} $B$ \textit{s}
means that for any other state \textit{s'} obtained by taking \textit{s} 
and setting the variables \texttt{strs} to any values, 
$B$ \textit{s'} holds.
We tried to prove
\begin{verbatim}
wlpm (at ?strs ?Am) ?Qm = allstrs ?strs (wlpm ?Am ?Qm)
\end{verbatim}
but could not.  
This reflected the fact that the formula for $\wlp\ (@z. A)$
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
\begin{verbatim}
at_wlp = "indep ?strs ?Qm ==>
   wlpm (at ?strs ?Am) ?Qm = allstrs ?strs (wlpm ?Am ?Qm)
\end{verbatim}
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$.

\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.
So we have defined types for the abstract-syntax-tree version of
integer and boolean expressions, thus (abbreviated):
\begin{verbatim}
datatype exp = Num nat
             | Var string
             | Pluss exp exp
             | Minus exp exp
             | Timess exp exp

datatype bexp = Eq exp exp
              | Lt exp exp
              | Le exp exp
              | Gt exp exp
              | Ge exp exp
              | Nott bexp
              | T
              | F
              | And bexp bexp
              | Or bexp bexp
              | Imp bexp bexp
\end{verbatim}
We defined substitution functions, of the following types
\begin{verbatim}
  expSub   :: "string => exp => exp => exp"
  bexpSub  :: "string => exp => bexp => bexp"
\end{verbatim}
where (for example) $\texttt{expSub} \ x \ E \ M$ means $M[x := E]$.
We also defined functions to translate an expression (type \aexp\ or 
\bexp\ -- which we will call a \textbf{syntactic} expression) 
to the corresponding function of type $\state \to \nat$ or
$\state \to \bool$ (which we will call a \textbf{semantic} expression).
We may also say the semantic expression is 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 talk about syntactic and semantic \emph{commands} also.

\begin{verbatim}
types
  expMeaning = "state => nat"
  bexpMeaning = "state => bool"

consts
  expMng   :: "exp => expMeaning"
  bexpMng  :: "bexp => bexpMeaning"
\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 := 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 ?strs ?strfun ?state ==
   {Term (setstrs ?strs ?strfun ?state)}
\end{verbatim}
We can then prove \verb|ass_trm| 
(which is trivial -- an assignment terminates), and
\verb|ass_wlp|, which says $\wlp (x := E, Q) = Q[x := E]$.
\begin{verbatim}
ass_wlp = "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 dashed.
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 we use a function \texttt{dashed}, of type \textit{state},
which gives the values of these logical variables.
\begin{verbatim}
atd ?Ad ?state == UN dashed. ?Ad dashed ?state
\end{verbatim}
Here \verb|?Ad| is not a semantic command, but a function which, given
a ``dashed'' 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 (%dashed. guard (prdm dashed ?A) (%st. {Term dashed})))"
\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 (%dashed. guard (prds ?x dashed ?A) (assignvs ?x dashed)))"
\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 the commands, 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 the 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 make it clear that 
the choice of $Q_1$ and $Q_2$ depends on the state $s$.
% 
% \begin{verbatim}
% pcomp_def = "pcomp ?Am ?Bm ?state ==
%   pcomprs (?Am ?state) (?Bm ?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 strings, 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) ?dashed (pcompfr ?fA ?Am ?fB ?Bm) =
   (prds ?fA ?dashed ?Am && prds ?fB ?dashed ?Bm)" 
\end{verbatim}