Generic weakest precondition semantics from monads enriched with order ?
We devise a generic framework where a weakest precondition semantics, in the form of indexed posets, is derived from a monad whose Kleisli category is enriched by posets. It is inspired by Jacobs' recent identification of a categorical structure that is common in various predicate transformers, but adds generality in the following aspects: (1) different notions of modality (such as may vs. must) are captured by EilenbergMoore algebras; (2) nested alternating branchinglike in games and in probabilistic systems with nondeterministic environmentsis modularly modeled by a monad on the EilenbergMoore category of another.
monad algebra game program verification program logic precondition calculus nondeterminism effect coalgebra categorical model