%0 Journal Article %1 SchroderMossakowski03b %A Schröder, Lutz %A Mossakowski, Till %D 2004 %J Journal of Logic and Computation %K CASL HasCASL Hoare calculus correctness dynamic logic monad total %N 4 %P 571--619 %T Monad-independent dynamic logic in HasCASL %U http://www.springerlink.com/openurl.asp?genre=article&issn=0302-9743&volume=2755&spage=425 %V 14 %X 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.

@article{SchroderMossakowski03b, 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. }, added-at = {2016-08-05T15:59:03.000+0200}, author = {Schr{\"o}der, Lutz and Mossakowski, Till}, biburl = {https://www.bibsonomy.org/bibtex/247e7f42b1fbce6587be494fac13e0b3e/tillmo}, interhash = {3d3b5e0367916d80f7e58c0feba4118c}, intrahash = {47e7f42b1fbce6587be494fac13e0b3e}, journal = {Journal of Logic and Computation}, keywords = {CASL HasCASL Hoare calculus correctness dynamic logic monad total}, note = {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}, number = 4, pages = {571--619}, pdfurl = {http://www.informatik.uni-bremen.de/~lschrode/hascasl/monadicpdl.pdf}, psurl = {http://www.informatik.uni-bremen.de/~lschrode/hascasl/monadicpdl.ps}, status = {Reviewed}, timestamp = {2016-08-05T15:59:03.000+0200}, title = {Monad-independent dynamic logic in {HasCASL}}, url = {http://www.springerlink.com/openurl.asp?genre=article&issn=0302-9743&volume=2755&spage=425}, volume = 14, year = 2004 }