Programming Research Group
Technical Report TR-23-95
Unifying wp and wlp
Carroll Morgan and
Annabelle McIver
August 1995, 10pp.
Abstract
By extending predicates so that as characteristic functions they may
deliver -1 as well as 0 or 1, we construct "extended-predicate
transformers" that include both wp and wlp.
We state and justify extended healthiness conditions for the new
transformers.
Keywords
Formal semantics, program correctness, weakest precondition, weakest
liberal precondition, Egli-Milner order.
This paper appears also as DCS/SVRC Technical Report 95-36 at the
University of Queensland.
It is available as a 61,613 byte
compressed PostScript file.