Abstract
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 axiomatically, using
Moggi’s idea of encapsulation of effects as monads.We introduce a dynamic logic (from which, as usual, a Hoare
logic can be derived) whose logical formulae are pure programs in a strong sense. We formulate a set of proof
rules for this logic, and prove it to be complete with respect to a categorical semantics. Using dynamic logic, we
then develop a relaxed notion of purity which allows for observationally neutral effects such writing on newly
allocated memory.
Users
Please
log in to take part in the discussion (add own reviews or comments).