\section{Introduction}

General correctness was introduced as an alternative to 
partial correctness and total correctness by Jacobs \& Gries (1985) \cite{JG}, 
see also Nelson (1989) \cite{Nelson}.
Jacobs \& Gries use a relational model, representing a program as a relation
between initial states and final states: their space of final states includes
$\bot$, representing non-termination.
In this way they can distinguish when a program guarantees termination,
guarantees non-termination, or neither.
Neither partial correctness nor total correctness (alone) can do this.

In \cite{Dunne-CATS} and \cite{Dunne-case},
Dunne gives an account of general correctness, 
in which he gives a set of ``abstract commands'', with associated semantics.
For each abstract command, Dunne gives its semantics 
in terms of its termination condition, its weakest liberal 
precondition predicate and
its \emph{frame}, which is (loosely)
the set of program variables which might be
altered by the command.
From these one can derive total-, partial- \emph{and}
general correctness semantics.

We describe the abstract commands in terms of an operational 
interpretation similar to that of Jacobs \& Gries.
We then use the automated prover Isabelle to 
show that this interpretation implies the semantics given by Dunne.
We also use Isabelle to prove some of his more difficult results.
Use of an automated theorem prover helped ensure the correct statement of 
precise details which can easily be overlooked otherwise,
and forced us to address the distinction between 
program variables and logical variables (which are easily confused in an
informal treatment).
We refer to results proved in Isabelle 
-- the code is available via the author's home page.

In \cite{Gordon}, Gordon provided an operational interpretation of
programs (commands), and used the HOL theorem prover to verify the axioms 
(rules) of Hoare logic.
He explains in detail certain problematic aspects of such work,
which we will allude to briefly.

In \cite{Harrison}, Harrison formalized Dijkstra's program logic in the HOL
theorem prover, using a relation between states and outcomes to model commands.

In \cite{lfh}, Lermer, Fidge \& Hayes considered the semantics of 
program execution, focussing on control-flow paths.
They consider weakest liberal preconditions, and also discuss strongest
postconditions.  
Their conditions are more complex than those discussed by Dunne
and in this paper,
since they consider typed local variables and execution of a command 
within a ``context''.