Recasting Hoare and He’s Unifying Theory of Programs in the Context of General Correctness

We review Hoare and He’s single-predicate model of sequential programs, and uncover its inability always to provide an adequate description of the required behaviour of a sequential program which implements a partial decision procedure: a significant shortcoming in an interactive era where such programs are often found as components of reactive systems. We show how the single-predicate model can be recast to overcome this limitation, using a variation on the predicate syntactic form employed by Hoare and He for their designs, which we call a prescription . We show that our prescriptions have a remarkably simple semantic characterisation by means of a single intuitively compelling healthiness condition. Our model also admits a pleasingly simple algebraic formulation which reveals it as a natural completion of Hoare and He’s model; indeed, we can show the latter to be congruent to a restricted sub-model of the former.