A Generic Complete Dynamic Logic for Reasoning About Purity and Effects

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

• Type: Conference
• Year: 2008
• Where: FASE
• Authors: Till Mossakowski, Lutz Schröder, Sergey Goncharov
• Keywords: Dynamic Logic, FASE 2008, Hoare-style Logics, Logical Formulae, Software Engineering