\section{Conclusion}
We have provided an operational model for Dunne's abstract commands
and their operators, except that our model does not provide any information
about the frame of a command.
Based upon this model, we have been able to prove,
using the automated prover Isabelle, 
Dunne's definitions of the abstract command operators, except their frames.
That is, we have shown that they follow from our operational model.

We have discussed the problems in including the frame of a command in
this work.
Briefly, while the frame of a command might be thought of as the set
of variables which ``might'' be set by the command, commands such as
$x := x$ (whose frame is $\{x\}$) prevent us from defining the command's
frame from its behaviour.
We could have attempted to show that the frame of a command
(as defined by Dunne) conforms to a rule that the frame contains
any variable which can be changed by the command, but this 
generally seems obvious.

Formalising the various definitions for use in the mechanised
prover has highlighted aspects of the specification of commands 
which need to be considered, but are easily overlooked until one
formalises them.  Examples of this appear in our discussions about 
``syntactic'' and ``semantic'' expressions and commands, and about
the language in which ``syntactic'' expressions may be expressed.

\subsubsection{Acknowledgement.} 
We wish to thank Steve Dunne for his very great assistance in 
some lengthy discussions on the topic.