Monadic Computational Logic in HasCASL

Photograph of Lutz Schroeder

Lutz Schroeder

(Bremen)

Following seminal work by Moggi, monads are being used for the encapsulation of side-effects in functional programming, in particular in Haskell. We report on work aimed at supporting programming with generic side effects in this sense with monad-based generic computational logics. In particular, we describe a generic Hoare calculus and a generic dynamic logic, along with notions of determinism and state preservation in monads relevant for the definition of state-dependent formula. While the generic Hoare calculus applies in principle (although at times with strong expressive limitations) to arbitrary monads, the semantics of dynamic logic is introduced axiomatically. By means of a general mechanism for extracting a set of states from a given monad, a sufficient criterion for interpretability of dynamic logic is obtained which covers most of the relevant cases; however, it turns out that the continuation monad fails to admit dynamic logic. Monadic computational logic may be used both for the verification of generic monadic programs and for the loose specification of side effects such as mutable references or non-determinism. As a running example, partial and total correctness of Dijkstra's non-deterministic implementation of Euclid's Algorithm are proved in a loosely specified non-deterministic dynamic reference monad, using the monadic Hoare calculus and a total Hoare calculus derived from monadic dynamic logic, respectively. Finally, we extend these methods to cover correctness of programs that make use of exceptions to manipulate the control flow. To this end, we give a categorical and an equational characterization of Moggi's exception monad transformer, which in combination with the previously developed formalisms give rise to generic partial and total Hoare calculi for exceptional termination. These results apply e.g. to the so-called Java monad and subsume existing Hoare logics for Java w.r.t. aspects of exceptional termination.
Thursday 10th March 2005, 14:00
Robert Recorde Room
Department of Computer Science