TY - GEN
T1 - A generic complete dynamic logic for reasoning about purity and effects
AU - Mossakowski, Till
AU - Schröder, Lutz
AU - Goncharov, Sergey
PY - 2008
Y1 - 2008
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=47249134300&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-78743-3_15
DO - 10.1007/978-3-540-78743-3_15
M3 - Conference contribution
AN - SCOPUS:47249134300
SN - 3540787429
SN - 9783540787426
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 199
EP - 214
BT - Fundamental Approaches to Software Engineering - 11th International Conference, FASE 2008 - Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Proceedings
T2 - "11th International Conferenceon Fundamental Approaches to Software Engineering, FASE 2008"
Y2 - 29 March 2008 through 6 April 2008
ER -