| Publication type: |
Article in Proceedings |
| Author: |
Lutz Schröder, Till Mossakowski |
| Editor: |
Mauro Pezze |
| Title: |
Monad-independent Hoare logic in HasCASL |
| Book / Collection title: |
Fundamental Approaches to Software Engineering (FASE 2003) |
| Volume: |
2621 |
| Page(s): |
261 – 277 |
| Series: |
Lecture Notes in Computer Science |
| Year published: |
2003 |
| Publisher: |
Springer, Berlin |
| 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.
|
| Internet: |
http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2621&spage=261 |
| PostScript Version: |
http://www.informatik.uni-bremen.de/~lschrode/hascasl/monads.ps |
| Keywords: |
monads Hoare logic CASL HasCASL |
| Status: |
Reviewed |
| Last updated: |
22. 06. 2005 |
