by Lutz Schröder and Till Mossakowski
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.
Reference:
Lutz Schröder and Till Mossakowski: Monad-independent Hoare logic in HasCASL, In Mauro Pezze, ed.: Fundamental Approaches to Software Engineering (FASE 2003), Lecture Notes in Computer Science, vol. 2621, pp. 261–277, Springer; Berlin; http://www.springer.de, 2003. [preprint]
Bibtex Entry:
@InProceedings{SchroderMossakowski03a,
author = {Lutz Schr{\"o}der and Till Mossakowski},
title = {Monad-independent Hoare logic in {HasCASL}},
year = {2003},
editor = {Mauro Pezze},
booktitle = {Fundamental Approaches to Software Engineering (FASE 2003)},
publisher = {Springer; Berlin; http://www.springer.de},
series = {Lecture Notes in Computer Science},
volume = {2621},
pages = {261--277},
keywords = {monads Hoare logic CASL HasCASL},
url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2621&spage=261},
comment = {<a href="http://www8.informatik.uni-erlangen.de/~schroeder/papers/monads.ps">[preprint]</a>},
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.
},
}