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.
Keywords
- High Order Logic
- Internal Logic
- Propositional Dynamic Logic
- Functional Programming Language
- Constructor Class
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Download to read the full chapter text
Chapter PDF
References
K. Claessen and J. Hughes, Testing monadic code with QuickCheck, HaskellWorkshop, ACM, 2002, pp. 65–77.
CoFI, The Common Framework Initiative for algebraic specification and development, electronic archives, http://www.brics.dk/Projects/CoFI.
CoFI Language Design Task Group, Casl-The CoFI Algebraic Specification Language-Summary, version 1.0, Documents/CASL/Summary, in [2], July 1999.
E. W. Dijkstra, A discipline of programming, Prentice Hall, 1976.
J.-C. Filliâtre, Proof of imperative programs in type theory, Types for Proofs and Programs, LNCS, vol. 1657, Springer, 1999, pp. 78–92.
R. Goldblatt, Logics of time and computation, CSLI, 1992.
S. P. Jones, J. Hughes, L. Augustsson, D. Barton, B. Boutel, W. Burton, J. Fasel, K. Hammond, R. Hinze, P. Hudak, T. Johnsson, M. Jones, J. Launchbury, E. Meijer, J. Peterson, A. Reid, C. Runciman, and P. Wadler, Haskell 98: A non-strict, purely functional language, (1999), http://www.haskell.org/onlinereport.
C. Lüth and N. Ghani, Monads and modularity, Frontiers of Combining Systems, LNAI, vol. 2309, Springer, 2002, pp. 18–32.
S. Mac Lane, Categories for the working mathematician, Springer, 1997.
E. Moggi, Notions of computation and monads, Inform. and Comput. 93 (1991), 55–92.
P. D. Mosses, Casl: A guided tour of its design,Workshop on Abstract Datatypes, LNCS, vol. 1589, Springer, 1999, pp. 216–240.
F. Regensburger, HOLCF: Higher order logic of computable functions, Theorem Proving in Higher Order Logics, LNCS, vol. 971, 1995, pp. 293–307.
L. Schröder and T. Mossakowski, HasCasl: Towards integrated specification and development of Haskell programs, Algebraic Methodology and Software Technology, LNCS, vol. 2422, Springer, 2002, pp. 99–116.
Philip Wadler, How to declare an imperative, ACM Computing Surveys 29 (1997), 240–263.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schröder, L., Mossakowski, T. (2003). Monad-Independent Hoare Logic in HASCASL . In: Pezzè, M. (eds) Fundamental Approaches to Software Engineering. FASE 2003. Lecture Notes in Computer Science, vol 2621. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36578-8_19
Download citation
DOI: https://doi.org/10.1007/3-540-36578-8_19
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00899-6
Online ISBN: 978-3-540-36578-5
eBook Packages: Springer Book Archive