  I present a new method for specifying and verifying the partial correctness
of sequential programs. The key observation is that, in Hoare logic, assertions
are used as selectors of states, that is, an assertion specifies the set of
program states that satisfy the assertion. Hence, the usual meaning of the
partial correctness Hoare triple $\{f\}\{P\}\{g\}$: if execution is started in
any of the states that satisfy assertion $f$, then, upon termination, the
resulting state will be some state that satisfies assertion $g$. There are of
course other ways to specify a set of states. I propose to replace assertions
by terminating programs: a program $A$ specifies a set of states as follows: we
start $A$ in any state whatsoever, and all the states that $A$ may terminate in
constitute the specified set. I call this set the post-states of $A$. I
introduce the operational triple $[A]\, P\, [B]$ to mean: if execution of $P$
is started in any post-state of $A$, then upon termination, the resulting state
will be some post-state of $B$. Here, $A$ is the pre-program, and plays the
role of a pre-condition, and $B$ is the post-program, and plays the role of a
post-condition.
