Predicate transformers as power operations
Ingrid Rewitzky, Chris Brink · Formal Aspects of Computing · 1995
Abstract In predicate transformer semantics, a program is represented as a mapping from predicates to predicates. In relational semantics, a program is represented as an (input-output) binary relation over some state space. We show how each of these approaches can be obtained from the other by using the power construction .