%0 Conference Paper %1 SchroderMossakowski03a %A Schröder, Lutz %A Mossakowski, Till %B Fundamental Approaches to Software Engineering (FASE 2003) %D 2003 %E Pezze, Mauro %I Springer; Berlin; http://www.springer.de %K CASL HasCASL Hoare logic monads %P 261--277 %T Monad-independent Hoare logic in HasCASL %U https://link.springer.com/chapter/10.1007/978-3-540-40020-2_25 %V 2621 %X 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.

@inproceedings{SchroderMossakowski03a, 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. }, added-at = {2016-08-05T15:59:03.000+0200}, author = {Schr{\"o}der, Lutz and Mossakowski, Till}, biburl = {https://www.bibsonomy.org/bibtex/2e252291f4075c90bed6825687aa7d108/tillmo}, booktitle = {Fundamental Approaches to Software Engineering (FASE 2003)}, editor = {Pezze, Mauro}, interhash = {d0a6761892bec1745f535c4c15a0ae7a}, intrahash = {e252291f4075c90bed6825687aa7d108}, keywords = {CASL HasCASL Hoare logic monads}, pages = {261--277}, psurl = {http://www.informatik.uni-bremen.de/~lschrode/hascasl/monads.ps}, publisher = {Springer; Berlin; http://www.springer.de}, series = {Lecture Notes in Computer Science}, status = {Reviewed}, timestamp = {2022-12-08T11:58:28.000+0100}, title = {Monad-independent Hoare logic in {HasCASL}}, url = {https://link.springer.com/chapter/10.1007/978-3-540-40020-2_25}, volume = 2621, year = 2003 }