Speci cation and Renement in General Correctness

Abstract. We augment B's existing total-correctness semantics of weak-est precondition (wp) with a partial-correctness semantics of weakest lib-eral precondition (wlp). By so doing we achieve a general-correctness semantics for B operations which not only accords more fully with our natural computational intuition, but also extends the essential expressive capability of B's Generalised Substitution Language (GSL) to embrace a whole new class of operations called semi-decidable, whose behaviour cannot be characterised in terms of total correctness alone. The abil-ity to specify semi-decidable operations is important because a desired conventional operation may lend itself to implementation as a concur-rent federation of semi-decidable operations co-operating under a mutual \termination pact". Indeed, computational constraints may render this the only viable implementation strategy. We call a generalised substi-tution invested with our general-correctness semantics an abstract com-mand. Our Abstract Command Language (ACL) is thus syntactically indistinguishable from the GSL, save for the introduction of one new composition operator, concert, expressing a \termination pact " between two concurrent abstract commands.