\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.
This paper refers to results proved in Isabelle 
-- the code is available via the author's home page (above).

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.