Lifting General Correctness into Partial Correctness is ok

Commands interpreted in general correctness are usually characterised by their wp and wlp predicate transformer effects. We describe a way to ascribe to such commands a

single

predicate transformer semantics which embodies both their wp and wlp characteristics. The new single predicate transformer describes an everywhere-terminating “lifted” computation in an

ok

-enriched variable space, where

ok

is inspired by Hoare and He’s UTP but has the novelty here that it enjoys the same status as the other state variables, so that it can be manipulated directly in the lifted computation itself.

The relational model of this lifted computation is not, however, simply the canonical UTP relation of the original underlying computation, since this turns out to yield too cumbersome a lifted computation to permit reasoning about efficiently with the mechanised tools available. Instead we adopt a slightly less constrained model, which we are able to show is nevertheless still effective for our purpose, and yet admits a much more efficient form of mechanised reasoning with the tools available.