Dijkstra Monads in Monadic Computation?

Abstract. The Dijkstra monad has been introduced recently for cap-turing weakest precondition computations within the context of program verification, supported by a theorem prover. Here we give a more general description of such Dijkstra 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 trans-formers. Instantiations of this triangle for different monads T show how to define the Dijkstra monad associated with T, via the logic involved. Technically, we provide a morphism of monads from the state monad transformation applied to T, to the Dijkstra monad associated with T. This monad map is precisely the weakest precondition map in the trian-gle, given in categorical terms by substitution.