Dijkstra and Hoare Monads in Monadic Computation

The Dijkstra and Hoare monads have been introduced recently for capturing weak-est precondition computations and computations with pre- and post-conditions, within the context of program verification, supported by a theorem prover. Here we give a more general description of such monads in a categorical setting. We first elaborate the recently developed view on program semantics in terms of a triangle of computations, state transformers, and predicate transformers. Instantiating this triangle for different computational monads T shows how to define the Dijkstra monad associated with T, via the logic involved. Subsequently we give abstract definitions of the Dijkstra and Hoare monad, parametrised by a computational monad. These definitions presuppose a suitable (categorical) predicate logic, defined on the Kleisli category of the underlying monad. When all this structure exists, we show that there are maps of monads (Hoare) ⇒ (State) ⇒ (Dijkstra), all parametrised by a monad T.