| Publication type: |
Article |
| Author: |
Lutz Schröder, Till Mossakowski |
| Title: |
Monad-independent dynamic logic in HasCASL |
| Volume: |
14 |
| Page(s): |
571 – 619 |
| Journal: |
Journal of Logic and Computation |
| Number: |
4 |
| Year published: |
2004 |
| Abstract: |
Monads have been recognized by Moggi as an elegant device for dealing with stateful computation in functional programming languages. In previous work, we have introduced a Hoare calculus for partial correctness of monadic programs. All this has been done in an entirely monad-independent way. Here, we extend this to a monad-independent dynamic logic (assuming a moderate amount of additional infrastructure for the monad). Dynamic logic is more expressive than the Hoare calculus; in particular, it allows reasoning about termination and total correctness. As the background formalism for these concepts, we use the logic of HasCASL, a higher-order language for functional specification and programming.
|
| Internet: |
http://www.springerlink.com/openurl.asp?genre=article&issn=0302-9743&volume=2755&spage=425 |
| PDF Version: |
http://www.informatik.uni-bremen.de/~lschrode/hascasl/monadicpdl.pdf |
| PostScript Version: |
http://www.informatik.uni-bremen.de/~lschrode/hascasl/monadicpdl.ps |
| Keywords: |
HasCASL CASL dynamic logic monad total correctness Hoare calculus |
| Note / Comment: |
Earlier version appeared in Martin Wirsing, Dirk Pattinson, and Rolf Hennicker (eds.), Recent Trends in Algebraic Development Techniques, 16th International Workshop (WADT 2002), LNCS vol. 2755, Springer, Berlin, 2003, pp. 425-441 |
| Status: |
Reviewed |
| Last updated: |
03. 01. 2005 |
