Weakest Preconditions in Fibrations
Alejandro Aguirre, Shin-ya Katsumata · Electronic Notes in Theoretical Computer Science · 2020
Weakest precondition transformers are useful tools in program verification. One of their key properties is compositionality, that is, the weakest precondition predicate transformer (wppt for short) associated to program f;g should be equal to the composition of the wppts associated to f and g. In this paper, we study the categorical structure behind wppts from a fibrational point of view. We characterize the wppts that satisfy compositionality as the ones constructed from the Cartesian lifting of a monad. We moreover show that Cartesian liftings of monads along lax slice categories bijectively correspond to Eilenberg-Moore monotone algebras. We then instantiate our techniques by deriving wppts for commonplace effects such as the maybe monad, the non-empty powerset monad, the counter monad or the distribution monad. We also show how to combine them to derive the wppts appearing in the literature of verification of probabilistic programs.