\section{Modelling Commands and Conditions} \label{s-mcc}

\subsubsection{Commands}
Typically one models a command (or program)
as a function acting on the machine state.
A deterministic command which must terminate can be modelled as a function
returning simply a single new machine state.
A deterministic command which may or may not terminate 
could be modelled as a function which returns either a new state or nothing,
representing the idea that a non-terminating command returns no result.
However if we represent a non-deterministic program as a function
which returns a set of new states, then this leaves us without a way of
representing non-termination as one of several possible outcomes.

We also want to represent commands which are infeasible.  
(These are a useful building-block, even if you don't want to write such
programs, as Dunne discusses).
In fact this, rather than non-termination,
is naturally represented by a command returning no new state.

The solution (Plotkin \cite{Plotkin}, also used by Harrison \cite{Harrison})
is to consider command \emph{outcomes}, where an outcome
is either termination in a new state or non-termination.

\subsubsection{Conditions}
Boolean expressions, or conditions, on the machine state,
occur in work such as this in two contexts.
Firstly, many commands (such as if--then--else, or while--do)
incorporate conditions on the state.
A state is typically represented as a function from the set of variable
names to their values.
The condition in such a command will most naturally be represented as
text in the programming language, or as
an abstract syntax tree, but as it will be capable of being evaluated
in any machine state, we might well think of it as a function of type
$\textit{state} \to \textit{bool}$ (and we could treat the notion of
state as an abstract entity).

Secondly, a condition $Q$ can appear in an expression
$wlp (C, Q)$ (where $wlp$ means weakest liberal precondition),
or in $\{P\} C \{Q\}$ (Hoare logic).
It may be most natural to think of these as predicates on states
(or functions of type $\state \to \textit{bool}$).
However the rule for \wlp, and a related rule in Hoare logic, are
$$\wlp (x := E, Q) = Q[x := E] \qquad
\{Q[x := E]\}\  x := E \ \{Q\}$$
By $Q[x := E]$ we mean $Q$ with occurrences of $x$ replaced by $E$;
various other authors write this as $Q[x/E]$, $Q[E/x]$, $Q_{E\to x}$,
$Q\langle E/x\rangle $, $\{E/x\}Q$, with, confusingly, 
both the first two being popular.
The notion of substitution in these rules
is meaningless when $Q$ is an arbitrary predicate on states;
they require $Q$ to be an expression written in the command language,
or something like it,
or as, say, an abstract syntax tree, containing literal program variable names.
Note that the language for such predicates must not be able to express
a condition like ``no two different variables may have the same value''
(for, then, what would $Q[x := E]$ mean?)
\comment{It would be possible to define $Q[x := E]$ so as simply to make the
formula for \wlp\ true, ie, 
$Q[x := E] = Q \circ f$, where 
$f : \state \to \state$ is the state change $[x := E]$.} 
\comment{
Actually, Harrison answers this question.  Any function
$f : \state \to \state$ can be treated as a terminating, deterministic
command, and, trivially, satisfies 
$\wp (f, Q) s = Q (f s) = (Q o f) s$.
So, setting $f$ to be the state change $[x := E]$, 
$Q[x := E]$ can be defined to be $Q o f$.}
However, $Q$ \emph{may} also contain logical variables,
as in the following Hoare logic example 
(taken from Gordon\cite[\S5.0]{Gordon}, where
$X,Y,Z$ denote program variables and $x,y$ denote logical variables)
$$\{X = x \land Y = y\} Z := X; X := Y; Y := Z \{X = y \land Y = x\}$$

It is also worth noting at this point that where boolean expressions are used
in abstract commands (such as the guarded command $P \to A$ and the 
preconditioned command $P | A$) the boolean $P$ is not treated as 
a fragment of code but rather as an arbitrary predicate on the state.
Thus, as is clear from Dunne's treatment of these commands, the 
possibility of $P$ looping or producing other than a single answer
is not considered.

Gordon \cite{Gordon} discusses these issues.  
What this means for us now is that our analysis of many commands 
(\emph{not} including assignment) can be performed at the level of abstraction
where a boolean expression is modelled as a predicate on states,
and a command is modelled as a function from states to sets of outcomes.
The next section contains the analysis at that level.

\subsubsection{Frames}
Dunne has also defined that each abstract command has a \emph{frame}.
Loosely, this is the set of variables which ``might'' be affected.
Note, however, that $\frm (x := x) = \{x\}$.
Also, from any command a new command may be defined which has an enlarged frame
but is otherwise the same.

Stating the frame of a command does not contribute to a description
of what the command does, so we can show, for example,
that two commands behave the same way, without considering their frames.
The work in this section proceeds on this basis.
Note that the results are therefore subject to the
proviso that two abstract commands are in fact distinct if their
frames differ.
We think the relevant proofs about frames would be quite
straightforward.

Consideration of literal commands and expressions,
of the frames of commands
and of the assignment command,
is deferred to the following section.

\section{Commands as transformations of state} \label{s-transf}

\subsection{Monadic Types} \label{s-monads}

As mentioned, we model a command as a function from states to sets of 
outcomes.
Here is the formal definition of the type \outcome.
\begin{verbatim}
datatype outcome = NonTerm | Term state
\end{verbatim}
So when we model sequencing of two commands $A$ and $B$, we first
apply $A$ to a given state, obtaining a set of outcomes, and we must then
apply $B$, a function of type $\state \to \outcome\ \set$, 
to the set of outcomes obtained from $A$.
We can think of this as ``extending'' the function $B$ to a function 
\emph{ext B} of type $\outcome\ \set \to \outcome\ \set$.
When this can be done in a way that satisfies certain conditions,
we call the relationship between the types a ``monad''.
See Wadler \cite{Wadler-essence} for further information on monads.

In fact, this is an example of a \emph{compound monad}.
The type \outcome, relative to the type \state, is a monad,
where the extension function, 
of type $(\state \to \outcome) \to (\outcome \to \outcome)$ would be given by
\begin{eqnarray*}
\exto\ f\ \texttt{NonTerm} & = & \texttt{NonTerm} \\
\exto\ f\ (\texttt{Term}\ s) & = & f s 
\end{eqnarray*}

\comment{
$$
\begin{array}{rcl}
\exto\ f\ \texttt{NonTerm} & = & \texttt{NonTerm} \\[-1ex]
\exto\ f\ (\texttt{Term}\ s) & = & f s 
\end{array}
\qquad
\begin{array}{rcl}
\exts\ f\ os & = & \displaystyle\bigcup_{o \in os} f\ o 
\end{array}
$$
}
For any type $\alpha$, the type $\alpha\ \set$ (the type of sets of things of
type $\alpha$) is also a monad,
where the extension function, 
of type $(\alpha\ \to \alpha\ \set) \to (\alpha\ \set \to \alpha\ \set)$,
would be given by
\begin{eqnarray*}
\exts\ f\ os & = & \bigcup_{o \in os} f\ o 
\end{eqnarray*}

Apart from the extension function, specification of a monad includes
a \unit\ function, which converts a value of the ``base'' type,
usually in a rather natural way, to a value of the monadic type.
% For example, $\unito\ s = \Term\ s$, and $\units\ e = \{e\}$.
For the two monads mentioned, we have
$$ \begin{array}{l@{\qquad}l} 
\unito : \state \to \outcome & \units : \alpha\ \to \alpha\ \set \\[-1ex]
\unito\ s = \Term\ s & \units\ e = \{e\}
\end{array} $$
Note also that the extension function is often called \textit{bind}
and written in infix format (as in \cite{Wadler-essence}),
so $\ext\ f\ s = s\ bind\ f$.

Two monads cannot in general be composed to form another monad, but 
the first monad mentioned above can in general be composed with any other 
monad to give a compound monad (see \cite[\S 7.3]{lhj}).
The formulae for the extension function,
both generally (in terms of \units\ and \exts)
and for our specific choice of  \units\ and \exts,
are given below.
In the specific case, \textit{extos} has type
$(\state \to \outcome\ \set) \to (\outcome\ \set \to \outcome\ \set)$. 
% \begin{eqnarray*}
% \lefteqn{extos f os =} \\
% \qquad let f' (\texttt{Term} s) & = & f s \\
% \qquad \qquad f' \texttt{NonTerm} & = & \{\texttt{NonTerm}\} \\
% \lefteqn { \qquad  in exts f' os}
% \end{eqnarray*}
\\[1ex]
\mbox{} \hfill
$
\begin{array}{lllll}
\multicolumn{5}{l}{\extos\ f\ os\ =} \\[-1ex]
 \qquad & let & f'\ (\texttt{Term}\ s) & = & f\ s \\[-1ex]
 & & f'\ \texttt{NonTerm} & = & \units\ \NonTerm \\[-1ex]
  & \multicolumn{4}{l}{in\ \exts\ f'\ os}
\end{array}
$
\hfill
$
\begin{array}{lllll}
\multicolumn{5}{l}{\extos\ f\ os\ =} \\[-1ex]
 \qquad & let & f'\ (\texttt{Term}\ s) & = & f\ s \\[-1ex]
 & & f'\ \texttt{NonTerm} & = & \{\NonTerm\} \\[-1ex]
  & \multicolumn{4}{l}{in\ \bigcup_{o \in os} f'\ o}
\end{array}
$
\hfill \mbox{} 
\\[1ex]

As mentioned above, a monad consists of functions \unit\ and \ext\
(of appropriate types), which must satisfy certain conditions, as follows:
\\[1ex]
\mbox{} \hfill
$
\begin{array}{rcl@{\qquad \qquad \qquad \qquad}r}
\ext\ k \circ \unit & = & k & \mbox{(Left Unit)} \\[-1ex]
\ext\ \unit & = & id & \mbox{(Right Unit)}\\[-1ex]
\ext\ (\ext\ h \circ k) & = & \ext\ h \circ \ext\ k & \mbox{\hfill (Assoc)}
\end{array}
$
\\[1ex]

Let $\seq\ A\ B$ denote the sequencing of commands $A$ and $B$
(where $A$, $B$ and $\seq\ A\ B$ are of type $\state \to \outcome\ \set$).
As noted, we want to first
apply $A$ to the given state, obtaining a set of outcomes;
we must then
apply the extension of $B$ (of type $\outcome\ \set \to \outcome\ \set$) 
to that set of outcomes.
That is, $\seq\ A\ B = \extos\ B \circ A$.
Then we can prove the associativity of \seq:
\begin{eqnarray*}
\seq\ A (\seq\ B\ C) & = & \extos\ (\seq\ B\ C) \circ A \\
 & = & \extos\ (\extos\ C \circ B) \circ A \\
 & = & \extos\ C \circ \extos\ B \circ A 
   \mbox{\qquad by the monad rule (Assoc)} \\
 & = & \extos\ C \circ \seq\ A\ B \\
 & = & \seq\ ( \seq\ A\ B) \ C
\end{eqnarray*}
This is proved in Isabelle as \verb|seq_assoc|.
Dunne \cite[\S 7]{Dunne-CATS} uses `;' for sequential composition,
so he writes $\seq\ A\ B$ as $A;B$.

The \unit\ function, of type $\state \to \outcome\ \set$,
of the compound monad is given by
$$ \unitos\ s = \units\ (\Term\ s) = \{\Term\ s\} $$
This represents the command \skp,
which always terminates in its initial state.

\subsection{Refinement}

As we will often just give Isabelle code, we mention 
some less obvious Isabelle notation.
The ``\verb|?|'' indicates a variable for which anything 
(of a suitable type) may be substituted.
Logical equivalence of booleans is denoted by
the equality symbol \verb|=| or \verb|==|.
% By convention in this paper, definitions are given using \verb|==|,
% whereas results we have proved use \verb|=|.
By convention in this paper, results we have proved as theorems
are given in quotes (often preceded by the theorem's name),
whereas definitions are given without quotes.

Some set and function notation (mathematical and Isabelle equivalents) follows:
\begin{center}
\begin{tabular}{c@{\qquad}c}
$%\displaystyle 
a \not\in \bigcup_{b \in C} D$ &
\verb|a ~: UN b:C. D| \\
$\{a\} \cup (C \cup D) \subseteq E \cap F \backslash G$ &
\verb| insert a (C Un D) <= E Int F - G| \\
$\lambda x. E$ & \verb|(%x. E)| \\
$A \to B$ (implication) & \verb|A ==> B| or \verb|A --> B|
\end{tabular}
\end{center}

We define functions corresponding to 
\textit{wlp}, \textit{trm}, 
and \textit{wp} of \cite[\S 2]{Dunne-CATS}. 

\begin{verbatim}
wlpm ?C ?B ?state == ALL nst. Term nst : ?C ?state --> ?B nst 
trmm ?C ?state     == NonTerm ~: ?C ?state
wpm ?C ?B         == wlpm ?C ?B && trmm ?C 
\end{verbatim}

Here \verb|&&| and \verb.||. lift conjunction  and disjunction over states,
and \verb|--->| is the ``is stronger'' relation between predicates, so
\begin{verbatim}
?p ---> ?q     ==  ALL s. ?p s --> ?q s
(?p && ?q) ?s  ==  ?p ?s & ?q ?s
(?p || ?q) ?s  ==  ?p ?s | ?q ?s
\end{verbatim}

These definitions work with commands and conditions as
functions of type 
$\state \to \outcome\ \set$ and 
$\state \to \bool$ respectively.
We note that a command (as such a function) is uniquely determined
by its \wlp\ and termination conditions.
This is proved in Isabelle as \verb|unique|.
Later we will introduce corresponding (differently named) functions which
take abstract syntax trees as arguments.

In \cite[\S 5]{Dunne-CATS} 
Dunne discusses several notions of refinement, including
\mbox{general-,} total- and partial-correctness refinement.
The second equivalent definition of \texttt{gencref}
is derived from Dunne's (Gcref2) (\cite[\S 2.1]{Dunne-case}).
\begin{verbatim}
totcref ?A ?B  ==  ALL Q. wpm ?A Q ---> wpm ?B Q
partcref ?A ?B ==  ALL Q. wlpm ?A Q ---> wlpm ?B Q
gencref ?A ?B  ==  partcref ?A ?B & totcref ?A ?B 
gencref ?A ?B  ==  partcref ?A ?B & (trmm ?A ---> trmm ?B)
\end{verbatim}

From these definitions, we proved the following
more direct characterizations
of these three notions of refinement.
It is worth noting that the characterization for 
general correctness is simpler than the other two
although it is defined in terms of both of them;
this no doubt explains how general correctness semantics
often seems simpler than either partial or total correctness semantics.
Also, the general correctness relation is anti-symmetric, unlike
either total or partial correctness.

\begin{verbatim}
"totcref ?A ?B  =  (ALL st. ?B st <= ?A st | NonTerm : ?A st)"
"partcref ?A ?B =  (ALL st. ?B st <= insert NonTerm (?A st))"
"gencref ?A ?B  =  (ALL state. ?B state <= ?A state)"
gencref_antisym = "[| gencref ?A ?B; gencref ?B ?A |] ==> ?A = ?B"
\end{verbatim}

\subsection{Strongest Postconditions}

Strongest postconditions have been discussed by a number of authors, 
cited in \cite{lfh}.
In \cite{lfh}, Lermer, Fidge \& Hayes give the strongest postcondition
semantics, as well as the weakest liberal precondition semantics,
of the commands they define, and we will refer to some of these later.
Meanwhile we give its definition in Isabelle, and that of
what they call ``sp-refinement''.
\begin{verbatim}
"slpm ?C ?B ?state == EX sb. ?B sb & Term ?state : ?C sb"
"slpref ?A ?B == ALL Q. slpm ?B Q ---> slpm ?A Q"
\end{verbatim}
That is, supposing precondition \texttt{B} to be satisfied,
\texttt{slpm C} holds (only) for those states which are possible
(terminating) outcomes of \texttt{C}.
This is clearly analogous to a weakest \emph{liberal} precondition
(hence our name, \texttt{slpm}),
in that if a command is changed to allow (or disallow) the additional
possibility of non-termination, the strongest postcondition remains
unchanged.
In fact it was trivial to prove (as \verb|wlp_slp_ref|) that 
strongest post-condition refinement is equivalent to 
partial-correctness refinement (\cite[Thm~6.1(vii)]{lfh}).
This is readily explained by the Galois connection between 
the weakest liberal precondition and the strongest postcondition functions
(\verb|wlp_slp_gal|, of which Theorem~6.1(v) and (vi) of \cite{lfh} are easy
corollaries).
\begin{verbatim}
wlp_slp_ref = "partcref = slpref" 
wlp_slp_gal = "(?Q ---> wlpm ?C ?R) = (slpm ?C ?Q ---> ?R)" 
\end{verbatim}

We may well ask whether the weakest precondition function \textit{wp}
has a Galois dual \textit{sp},
but the answer is in the negative.
For that would require $sp\ C\ Q \longrightarrow \textit{true}$
(which always holds) being equivalent to 
$Q \longrightarrow wp\ C\ \textit{true}$
(which does not hold at states which satisfy $Q$ but from which $C$ may not
terminate).
However we can define functions \verb|spom| and \verb|wpom| 
(strongest post- and weakest pre-conditions based on outcomes)
which are Galois duals and are neatly related to general correctness
refinement.
\begin{eqnarray*}
  \spom & : & (\state \to \outcome\ \set) \to 
 (\state \to \bool) \to \outcome\ \to \bool\ \\
 \wpom & : & (\state \to \outcome\ \set) \to 
 (\outcome\ \to \bool) \to \state \to \bool\ \\
\end{eqnarray*}
\vspace{-7ex}
\begin{eqnarray*}
 \spom\ C\ Q\ c &=& \exists s.\ Q\ s \land c \in C\ s \\
 \wpom\ C\ R\ s &=& \forall c \in C\ s.\ R\ c
\end{eqnarray*}
\vspace{-3ex}
% spom ?C ?Q ?oc == EX sb. ?Q sb & ?oc : ?C sb
% wpom ?C ?occ ?state == ALL oc: ?C ?state. ?occ oc"
\begin{verbatim}
wpo_spo_gal = "(?Q ---> wpom ?C ?R) = (spom ?C ?Q ---> ?R)" 
gencref_wpo = "gencref ?A ?B = (ALL Q. wpom ?A Q ---> wpom ?B Q)" 
gencref_spo = "gencref ?A ?B = (ALL Q. spom ?B Q ---> spom ?A Q)" 
\end{verbatim}

\subsection{Meaning of Commands}

\subsubsection{skip, perhaps, magic, abort}
\cite[\S 7]{Dunne-CATS}
\skp\ is the command which is feasible, terminates and does nothing
to the state.  It is exactly the function \unitos.
It follows immediately from the (Left Unit) and (Right Unit) monad laws
that \skp\ is an identity (left and right) for the binary function \seq.
These are proved in Isabelle as \verb|seq_unitL| and \verb|seq_unitR|.
We also define 
\begin{verbatim}
perhaps ?st  ==  {Term ?st, NonTerm}
magic ?st    ==  {}
abort ?st    ==  {NonTerm}
\end{verbatim}

\subsubsection{preconditioned command}
\cite[\S 7]{Dunne-CATS}
The command $P | A$ is the same as $A$ except that, if $P$ does not hold,
then $P | A$ \emph{may} fail to terminate.
\begin{verbatim}
precon ?B ?C ?state ==
   if ?B ?state then ?C ?state else insert NonTerm (?C ?state)
\end{verbatim}

\subsubsection{guarded command}
\cite[\S 7]{Dunne-CATS}
The command $P \longrightarrow A$ is the same as $A$ if $P$ holds,
but is \emph{infeasible} (the outcome set is empty) if $P$ does not hold.
\begin{verbatim}
guard ?B ?C ?state == if ?B ?state then ?C ?state else {}
\end{verbatim}

A command has a ``natural'' guard and precondition.
Here \verb|fis| $A$ means $A$ is \emph{feasible}, that is, its
outcome set is non-empty.  We have proved
\begin{verbatim}
fis_guard  =  "guard (fis ?A) ?A = ?A"
pc_trm     =  "precon (trmm ?A) ?A = ?A"
\end{verbatim}

% \subsubsection{sequential composition}
% \cite[\S 7]{Dunne-CATS}
% $A ; B$ is %\seq\ A\ B$, which
% is discussed above, in \S\ref{s-monads}.

\subsubsection{choice}
In \cite[\S 7]{Dunne-CATS}
Dunne defines a binary operator, $A \Box B$, for \emph{bounded choice}:
$A \Box B$ is a command which can choose between two commands $A$ and $B$.  
This is a special case of choice among an arbitrary set of commands,
defined by
\begin{center}
$\displaystyle \choice\ C\ s = \bigcup_{c \in C} c\ s$ \hfill
\verb|choice ?Cs ?state == UN C:?Cs. C ?state|
\end{center}

From these, we prove the definitions, and other results, of Dunne
\cite[\S5,6]{Dunne-case}.
\begin{verbatim}
perhaps_alt = "perhaps = precon (%st. False) unitos"
magic_alt = "magic = guard (%st. False) ?A"
abort_alt = "abort = precon (%st. False) (guard (%st. False) ?A)"
pma = "seq perhaps magic = abort"
asp = "choice {abort, unitos} = perhaps"
\end{verbatim}

\subsubsection{concert}
\cite[\S 12]{Dunne-CATS}
The command $A \# B$ represents $A$ and $B$ executing independently, on 
seperate copies of the state: whichever of $A$ or $B$ terminates first
gives the effect of $A \# B$.
Thus the possible outcomes of $A \# B$ are:
\begin{itemize}
\item \verb|Term| $s$, if it is an outcome of $A$,
\item \verb|Term| $s$, if it is an outcome of $B$,
\item \NonTerm, if it is an outcome of \emph{both} $A$ and $B$.
\end{itemize}
\begin{verbatim}
conc ?A ?B ?state == concrs (?A ?state) (?B ?state)
concrs ?cr1 ?cr2 ==
   ?cr1 Un ?cr2 - {NonTerm} Un {NonTerm} Int ?cr1 Int ?cr2
\end{verbatim}
Interestingly, this means that if $B$ is \magic\ (everywhere infeasible),
then $A \# B$ is just $A$ with any possibility of non-termination removed
(difficult though it is to see from the first sentence above!).
This is proved in Isabelle as \verb|conc_magic|.

The \wlp\ and termination conditions for these commands, which are used
by Dunne to \emph{define} these commands, are proved in Isabelle from our
definitions, as 
\verb|precon_trm|, \verb|precon_wlp|,
\verb|guard_trm|, \verb|guard_wlp|,
\verb|seq_trm|, \verb|seq_wlp|,
\verb|choice_trm|, \verb|choice_wlp|,
\verb|conc_trm| and \verb|conc_wlp|.
Dunne's results Xpre, Xguard, Xassump and Xassert
\cite[\S4,5]{Dunne-case}
are also proved in Isabelle. %, under the same names.
\begin{verbatim}
Xpre = "seq (precon ?P ?A) ?B = precon ?P (seq ?A ?B)"
Xguard = "seq (guard ?P ?A) ?B = guard ?P (seq ?A ?B)"
Xassump = "guard ?P ?A = seq (guard ?P unitos) ?A"
Xassert = "precon ?P (guard ?P ?A) = 
    seq (precon ?P (guard ?P unitos)) ?A"
\end{verbatim}

\subsection{Repetition and Iteration}

\subsubsection{finite repetition}
\cite[\S 7]{Dunne-CATS}
Dunne defines $A^0 = \skp$ and $A^{n+1} = A ; A^n$.
A very convenient result which we proved, called \verb|rep_Suc'|, is
that $A^{n+1} = A^n ; A$.

\subsubsection{repetitive closure}
\cite[\S 12]{Dunne-CATS}
We also defined $\repall\ c\ s = \bigcup_n \rep\ n\ c\ s$, ie,
\begin{verbatim}
repall ?C ?state == UN n. rep n ?C ?state
\end{verbatim}
that is, $\texttt{repall}\ A$ is the (unbounded) choice 
of any number of repetitions of $A$.
The termination condition for $\texttt{repall}\ A$ is that for every $n$,
$A^n$ terminates (proved as \verb|repall_term|).

The \emph{repetitive closure} of $A$ is $A^{*}$, where the outcomes
of $A^{*}$ are those of \verb|repall|, augmented by 
\NonTerm\ in the case where it is feasible to execute $A$
infinitely many times sequentially (we call this an ``infinite chain'').
It is much easier to define this concept operationally 
than in terms of \wlp\ and \trm.
The definition of an infinite chain
asserts an infinite sequence of states, of which 
each is reachable from the previous one.
We omit the Isabelle definition.
% \begin{verbatim}
% infch ?A ?s == EX f. f 0 = ?s & (ALL n. Term (f (Suc n)) : ?A (f n))
% \end{verbatim}
$$
\textit{infch}\  A\  s \equiv \exists f.\  f\  0 =
  s \land (\forall n.\  \Term\  (f\  (n+1)) \in A\  (f\  n))
$$

Thus we have the definition
\begin{verbatim}
repstar ?C ?state == repall ?C ?state Un
	    (if infch ?C ?state then {NonTerm} else {})
\end{verbatim}

It may be noted that in \cite[\S 10]{Dunne-CATS},
Dunne defined a predicate \textit{cic} (``cycles and infinite chains''),
with the intended meaning that 
$\textit{cic}\ A\ s$ be true if perpetual repetition of $A$ is feasible, 
(ie, an infinite chain of executions of $A$ is possible).
However the definition made $\textit{cic}\ A\ s$ true in the situation
where $A$ could be executed any given $n$ times sequentially,
which is \emph{not} sufficient to ensure an infinite chain of executions.
(It would be sufficient under an assumption of bounded
non-determinacy, see \cite[\S 3]{Harrison}).
As is a common experience, we did not discover this discrepancy until
trying to perform Isabelle proofs based on the definition in question.
% While Dunne used a different treatment in \cite{Dunne-case}, 

We have proved some useful results, such as
\begin{description}
\item[\texttt{wlpca} :] $\wlp\ (A^*, \_) = \wlp\ (\texttt{repall}\ A, \_)$ 
(since they differ only
in that $A^*$ has an additional possibility of non-termination)
\item[\texttt{seq\_repstar} :] $A^* ; A = A ; A^*$
\end{description}

% \begin{verbatim}
% wlpca = "wlpm (repstar ?A) = wlpm (repall ?A)"
% seq_repstar = "seq (repstar ?C) ?C = seq ?C (repstar ?C)"
% \end{verbatim}

In \cite[\S 12]{Dunne-CATS}
Dunne mentions that repetitive closure could be defined
using \emph{Egli-Milner} approximation \cite[\S 6]{Dunne-CATS}.
%
\comment{
I noticed on page 7 you talk about Egli-Milner refinement.
  I think you'd be wiser to talk of Egli-Milner approximation.
    That is to say, the EM ordering isn't a refinement ordering,
      since it doesn't model any plausible kind of correctness-preserving
	transformation between programs.}
$$A \leq_{em} A' \equiv A \sqsubseteq_{tot} A' \land A' \sqsubseteq_{par} A$$
where $\sqsubseteq_{tot}$ and $\sqsubseteq_{par}$ denote respectively
total- and partial-correctness refinement.
Then $A^*$ is a least fixpoint under the ordering $\leq_{em}$:
$$A^* \equiv \mu_{em} X. (A ; X) \Box \skp$$
We show in Isabelle that our definition of $A^*$ implies this result.
Here \verb|fprep_alt2| is a paraphrase of our definition of \verb|fprep|
(\texttt{fprep} $A$ $X$ means \mbox{$X = (A ; X) \Box \skp$}),
\verb|repstar_isfp| says that $A^*$ is a fixpoint, and
\verb|repstar_is_lfp| says that $A^*$  is less than or equal to, 
in the {Egli-Milner} ordering, any given fixpoint $Y$.
We also have that the {Egli-Milner} ordering is anti-symmetric,
so a least fixpoint is unique.

% , as \verb|repstar_isfp| and \verb|repstar_is_lfp|,
\begin{verbatim}
fprep_alt2 = "fprep ?A ?X = (?X = choice {seq ?A ?X, unitos})" 
repstar_isfp = "fprep ?A (repstar ?A)" 
repstar_is_lfp = "fprep ?A ?Y ==> egMil (repstar ?A) ?Y" 
egMil_antisym = "[| egMil ?A ?B; egMil ?B ?A |] ==> ?A = ?B" 
\end{verbatim}

% It would follow that $A^*$ is both a least fixpoint under $\sqsubseteq_{tot}$ 
% and a greatest fixpoint under $\sqsubseteq_{par}$ of 
% $\lambda X.\ (A ; X) \Box \skp$ -- 
% but note that such least/greatest fixpoints are not necessarily unique.
Dunne (pers.~comm.) % (personal communication)
also defines $\trm(A^*)$ and $\wlp(A^*, Q)$ as fixpoints:
% \begin{eqnarray*}
% \trm(A^*) & = & \nu Y. \textit{wp}(A, Y) \\
% \wlp(A^*, Q) & = & \mu Y. \wlp(A, Y) \land Q
% \end{eqnarray*}
$$ \trm(A^*)  =  \nu Y. \textit{wp}(A, Y) \qquad
\wlp(A^*, Q)  =  \mu Y. \wlp(A, Y) \land Q $$
where $\mu$ and $\nu$ denote the least and greatest fixpoints,
that is the weakest and strongest (respectively) fixpoints.
We also prove these results in Isabelle, based on our definition of $A^*$.
\verb|trfp| and \verb|wrfp| say that $\trm(A^*)$ and $\wlp(A^*, Q)$
are fixpoints of the respective functions.
\verb|trsfp| says that $\trm(A^*)$ is equal or weaker than
any given fixpoint $Y$, and similarly for \verb|wrwfp|.

\begin{verbatim}
trfp = "trmm (repstar ?A) = wpm ?A (trmm (repstar ?A))" 
trsfp = "?Y = wpm ?A ?Y ==> trmm (repstar ?A) ---> ?Y" 
wrfp = "let wlpstar = wlpm (repstar ?A) ?Q
    in wlpstar = (wlpm ?A wlpstar && ?Q)" 
wrwfp = "?Y = (wlpm ?A ?Y && ?Q) ==>
    ?Y ---> wlpm (repstar ?A) ?Q" 
\end{verbatim}

We can get a similar set of results for \texttt{repall}.
Firstly, \texttt{repall} $A$ is a \emph{greatest} fixpoint under the
general correctness refinement ordering $\sqsubseteq_{gen}$,
and secondly, the termination condition for \texttt{repall} $A$ is a
\emph{least (weakest)} fixpoint.
Recall that $\wlp\ (\texttt{repall}\ A, Q) = \wlp(A^*, Q)$.
$$\texttt{repall}\ A = \nu_{gen} X. (A ; X) \Box \skp \qquad
\trm(A^*)  =  \mu Y. \textit{wp}(A, Y) $$

\begin{verbatim}
repall_isfp = "fprep ?A (repall ?A)" 
repall_is_gfp = "fprep ?A ?X ==> gencref ?X (repall ?A)" 
trallfp = "trmm (repall ?A) = wpm ?A (trmm (repall ?A))" 
trallwfp = "?Y = wpm ?A ?Y ==> ?Y ---> trmm (repall ?A)"
\end{verbatim}
It follows that \texttt{repall} $A$ and $A^*$ are both greatest fixpoints
under $\sqsubseteq_{par}$ of $\lambda X.\ (A ; X) \Box \skp$,
reflecting that such fixpoints need not be unique,
since $\sqsubseteq_{par}$ is not anti-symmetric.

\subsection{Monotonicity}
For developing a program by starting with an abstract expression 
(of requirements), and progressively refining it to a concrete program,
it is important that the abstract commands constructors are monotonic
with respect to general-correctness refinement ($\sqsubseteq_{gen}$).

Given our characterization of $A \sqsubseteq_{gen} B$ as
$(\forall \state.\ B\  \state \subseteq A\ \state)$,
and our operational definition of commands in terms of outcome sets,
it is easy to see that all the constructors mentioned are monotonic.
In any event, they are proved in Isabelle as (for example)
\verb|seq_ref_mono|,
% \verb|rep_ref_mono|,
\verb|repstar_ref_mono|, etc.


\subsection{The \while\ loop}
In \cite[\S 7, \S 12]{Dunne-CATS} Dunne defines 
\begin{eqnarray*}
\iif\ G\ \then\ A\ \eend & \ \equiv\ & (G \to A) \Box (\lnot G \to \skp) \\
\while\ G\ \ddo\ A\ \eend & \ \equiv\ & (G \to A)^* ; \lnot G \to \skp 
\end{eqnarray*}

The definition of $\while$ which is intuitive to programmers is 
$$
\while\ G\ \ddo\ A\ \eend  \ \equiv\  
  \iif\ G\ \then\ A ; \while\ G\ \ddo\ A\ \eend\ \eend$$

We cannot use this as a definition in Isabelle since it is recursive --
as it stands it is non-terminating, and when applied to a particular state,
may not terminate. 
So in Isabelle we have defined $\while$ as does Dunne, and have proved 
that it satisfies the ``intuitive'' definition.
\begin{verbatim}
while_prog = "while ?G ?A = ifthen ?G (seq ?A (while ?G ?A))"
\end{verbatim}