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 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.

Reference:

A generic complete dynamic logic for reasoning about purity and effects (Till Mossakowski, Lutz Schröder, Sergey Goncharov), In Fundamental Approaches to Software Engineering (FASE 2008) (J. Fiadeiro, P. Inverardi, eds.), Lecture Notes in Computer Science, vol. 4961, pp. 199–214, Springer, 2008.

Bibtex Entry:

@InProceedings{MossakowskiEA08b, author = {Till Mossakowski and Lutz Schr{\"o}der and Sergey Goncharov}, title = { A generic complete dynamic logic for reasoning about purity and effects}, year = {2008}, editor = {J. Fiadeiro and P. Inverardi}, booktitle = {Fundamental Approaches to Software Engineering (FASE 2008)}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {4961}, pages = {199-214}, keywords = {dynamic logic pure function monad observational purity completeness}, url = {http://dx.doi.org/10.1007/978-3-540-78743-3_15}, pdfurl = {http://www.informatik.uni-bremen.de/~till/papers/purity-effects.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 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.}, status = {Reviewed} }

Powered by bibtexbrowser