Publication
A generic complete dynamic logic for reasoning about purity and effects
Till Mossakowski; Lutz Schröder; Sergey Goncharov
In: J. Fiadeiro; P. Inverardi (Hrsg.). Fundamental Approaches to Software Engineering. Fundamental Approaches to Software Engineering (FASE-08), located at 11th Conference of the European Joint Conferences on Theory and Practice of Software (ETAPS 2008), March 29 - April 6, Budapest, Hungary, Pages 199-214, Lecture Notes in Computer Science (LNCS), Vol. 4961, Springer, 2008.
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 modeled 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.