A generic complete dynamic logic for reasoning about purity and effects
T. Mossakowski, L. Schröder, and S. Goncharov. Fundamental Approaches to Software Engineering (FASE 2008), volume 4961 of Lecture Notes in Computer Science, page 199-214. 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.
%0 Conference Paper
%1 MossakowskiEA08b
%A Mossakowski, Till
%A Schröder, Lutz
%A Goncharov, Sergey
%B Fundamental Approaches to Software Engineering (FASE 2008)
%D 2008
%E Fiadeiro, J.
%E Inverardi, P.
%I Springer
%K completeness dynamic function logic monad observational pure purity
%P 199-214
%T A generic complete dynamic logic for reasoning about purity and effects
%U http://dx.doi.org/10.1007/978-3-540-78743-3_15
%V 4961
%X 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.
@inproceedings{MossakowskiEA08b,
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.},
added-at = {2016-08-05T15:59:03.000+0200},
author = {Mossakowski, Till and Schr{\"o}der, Lutz and Goncharov, Sergey},
biburl = {https://www.bibsonomy.org/bibtex/2a27c1257f1171c1b2833dbcadee1fb9a/tillmo},
booktitle = {Fundamental Approaches to Software Engineering (FASE 2008)},
editor = {Fiadeiro, J. and Inverardi, P.},
interhash = {2241a61078c7e0bfc014773d5cca2258},
intrahash = {a27c1257f1171c1b2833dbcadee1fb9a},
keywords = {completeness dynamic function logic monad observational pure purity},
pages = {199-214},
pdfurl = {http://www.informatik.uni-bremen.de/~till/papers/purity-effects.pdf},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
status = {Reviewed},
timestamp = {2016-08-05T15:59:03.000+0200},
title = { A generic complete dynamic logic for reasoning about purity and effects},
url = {http://dx.doi.org/10.1007/978-3-540-78743-3_15},
volume = 4961,
year = 2008
}