A Taxonomy of Predicate Transformer Monads for Specifying Monadic Programs

Abstract

Monads of weakest precondition predicate transformers are the foundation of several verification frameworks for monadic programs. For specifying monadic computations with nondeterminism and nontermination, in addition to weakest preconditions, we introduce the first strongest postcondition monads covering all combinations of angelic or demonic nondeterminism and partial or total interpretations of nontermination. For extending these base strongest postcondition monads with side effects such as mutable state, monad transformers do not yield the expected monads, so we instead generalize the base monads to arrows and use arrow transformers. We give a taxonomy of weakest precondition and strongest postcondition monads, for the base monads and for their versions with state, and show that the known relationships between under- and over-approximate triples based on predicate transformers already hold at the level of the predicate transformers themselves. We use the predicate transformer monads to define under- and over-approximate triples and, where possible, Dijkstra monads. Finally, we relate these two specification styles.