A Relatively Complete Generic Hoare Logic for Order-Enriched Effects

Monads are the basis of a well-established method of encapsulating side-effects in semantics and programming. There have been a number of proposals for monadic program logics in the setting of plain monads, while much of the recent work on monadic semantics is concerned with monads on enriched categories, in particular in domain-theoretic settings, which allow for recursive monadic programs. Here, we lay out a definition of order-enriched monad which imposes cpo structure on the monad itself rather than on base category. Starting from the observation that order-enrichment of a monad induces a weak truth-value object, we develop a generic Hoare calculus for monadic side-effecting programs. For this calculus, we prove relative completeness via a calculus of weakest preconditions, which we also relate to strongest postconditions.