For a number of programming languages, among them Eiffel, C, Java, and Ruby, Hoare-
style logics and dynamic logics have been developed. In these logics, pre-and
postconditions are typically formulated using potentially effectful programs. In order to
ensure that these pre-and postconditions behave like logical formulae (that is, enjoy some
kind of referential transparency), a notion of purity is needed. Here, we introduce a generic
framework for reasoning about purity and effects. Effects are modelled abstractly and …

For a number of programming languages, among them Eiffel, C, Java and Ruby, Hoare-style
logics and dynamic logics have been developed. In these logics, pre-and postconditions are
typically formulated using potentially effectful programs. In order to ensure that these pre-
and postconditions behave like logical formulae (that is, enjoy some kind of referential
transparency), a notion of purity is needed. Here, we introduce a generic framework for
reasoning about purity and effects. Effects are modeled abstractly and axiomatically, using …