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.
Author and article information
School of Computing and Mathematics, University of Teesside
Middlesbrough, TS1 3BA, UK