Reasoning about programs that use effects can be much harder than reasoning about their pure counterparts. This paper presents a predicate transformer semantics for a variety of effects, including exceptions, state, non-determinism, and general recursion. The predicate transformer semantics gives rise to a refinement relation that can be used to relate a program to its specification, or even calculate effectful programs that are correct by construction.

@article{paperbot581,
  title = {A predicate transformer semantics for effects (functional pearl)},
  author = {Wouter Swierstra and Tim Baanen},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {3},
  number = {ICFP},
  year = {2019},
  doi = {10.1145/3341707}
}