Monad-independent Hoare logic in HASCASL

Abstract

Monads have been recognized by Moggi as an elegant device for dealing with stateful computation in functional programming languages. It is thus natural to develop a Hoare calculus for reasoning about computational monads. While this has previously been done only for the state monad, we here provide a generic, monad-independent approach, which applies also to further computational monads such as exceptions, input/output, and non-determinism. All this is formalized within the logic of HASCASL, a higher-order language for functional specification and programming. Combination of monadic features can be obtained by combining their loose specifications. As an application, we prove partial correctness of Dijkstra's nondeterministic version of Euclid's algorithm in a monad with nondeterministic dynamic references. © Springer-Verlag Berlin Heidelberg 2003.