Monads classify program specifications with nondeterminism and state effects
A Taxonomy of Predicate Transformer Monads for Specifying Monadic Programs
Programming Languages
Summary
Specifying what computer programs do can be tricky when programs have uncertain choices or do not always finish. This paper offers a way to describe programs using mathematical structures called monads, which capture outcomes before and after running programs, even with uncertain or incomplete behavior. The authors also explain how to handle changes in program memory and side effects more smoothly. Their work unifies different ways to describe program correctness and shows how these descriptions relate to each other.
What this means in practice
- •For software verification engineers: Construct formal specifications that handle complex program behaviors like nondeterminism and state changes more comprehensively.
- •For programming language designers: Design verification frameworks supporting richer program effects and reasoning styles by applying the taxonomy of specification monads and transformers.
A theory result. No direct application yet.
Authors
Abigail Pribisova, Yao Li, Catalin Hritcu, Cezar-Constantin Andrici, Kenji Maillard, Exequiel Rivas
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.