A Generic Complete Dynamic Logic for Reasoning about Purity and Effects (bibtex)

by Till Mossakowski, Lutz Schröder, Sergey Goncharov

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.

Reference:

A Generic Complete Dynamic Logic for Reasoning about Purity and Effects (Till Mossakowski, Lutz Schröder, Sergey Goncharov), In Formal Aspects of Computing, vol. 22(3-4), pp. 363–384, 2010.

Bibtex Entry:

@Article{MossakowskiEA09, author = {Till Mossakowski and Lutz Schr{\"o}der and Sergey Goncharov}, title = {A Generic Complete Dynamic Logic for Reasoning about Purity and Effects}, year = {2010}, journal = {Formal Aspects of Computing}, volume = {22}, pages = {363-384}, number = {3-4}, keywords = {monad logic purity side-effect soundness completeness}, url = {http://dx.doi.org/10.1007/s00165-010-0153-4}, pdfurl = {http://www.informatik.uni-bremen.de/~lschrode/papers/mdl-compl.pdf}, 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.}, issn = {0934-5043}, status = {Reviewed} }

Powered by bibtexbrowser