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) befindet sich 11th Conference of the European Joint Conferences on Theory and Practice of Software (ETAPS 2008) March 29-April 6 Budapest Hungary Seiten 199-214 Lecture Notes in Computer Science (LNCS) 4961 Springer 2008.


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.


Weitere Links

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence