Abstract
This paper discusses reasoning about IO operations in Haskell, Clean and C and compares the effect on ease of reasoning of the different approaches taken to IO in these languages. An IO system model is built using VDM and is used to prove a basic property of a program written in each of the three languages. We tentatively draw the conclusions that functional languages are easier to reason about and that Monads can make the reasoning process slightly more difficult, but note that much future work is needed.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Joe Armstrong et al. Concurrent Programming in ERLANG. Prentice Hall Europe, London, 2nd edition edition, 1996.
Peter Achten and Martin Wierich. A Tutorial to the Clean Object I/O Library—Version 1.2. Technical report, Dept. of Functional Programming, University of Nijmegen, The Netherlands, February 2000.
Richard Bird and Oege de Moor. Algebra of Programming. Series in Computer Science. Prentice Hall International, London, 1987.
Richard Bird. Introduction to Functional Programming using Haskell. Series in Computer Science. Prentice Hall, second edition edition, 1998.
J.-P. Banatre, S.B. Jones, and D. Le Métayer. Prospects for Functional Programming in Software Engineering, volume 1 of ESPRIT Research Reports, Project 302. Springer-Verlag, Berlin, 1991.
Erik Barendsen and Sjaak Smetsers. Uniqueness typing for functional languages with graph rewriting semantics. Mathematical Structures in Computer Science, 00:pp1–36, 2000.
Andrew Butterfield and Glenn Strong. Comparing I/O Proofs in Three Programming Paradigms: a Baseline. Technical Report TCD-CS-2001-31, Dublin University, Computer Science Department, Trinity College, Dublin, August 2001.
Andrew D. Gordon. Functional Programming and Input/ Output. Distinguished Dissertations in Computer Science. Cambridge University Press, 1994.
Zoltan Horvath et al. Proving the temporal properties of the unique world. In Software Technology, Fenno-Ugric Symposium FUSST’p99 Proceedings, pages pp113–125, Technical Report CS 104/99, Tallin, 1999.
M.C. Henson. Elements of Functional Languages. Computer Science Texts. Blackwell Scientific Publications, 1987.
C. A. R. Hoare and He Jifeng. Unifying Theories of Programming. Series in Computer Science. Prentice Hall International, London, 1998.
Arthur Hughes. Elements of an Operator Calculus. Ph.D. dissertation, University of Dublin, Trinity College, Department of Computer Science, 2000.
Cli. B. Jones. Systematic Software Development using VDM. Series in Computer Science. Prentice Hall International, London, 2nd edition, 1990.
Brian W. Kernighan and Dennis M. Ritchie. The C Programming Language. Software Series. Prentice Hall, 2nd edition, 1988.
Mýcheál Mac an Airchinnigh. Conceptual Models and Computing. Ph.D. dissertation, University of Dublin, Trinity College, Department of Computer Science, 1990.
Carroll Morgan. Programming from Specifications. Series in Computer Science. Prentice-Hall International, London, 2nd. edition, 1994.
Simon Peyton Jones, John Hughes, et al. Haskell 98. Technical report, http://www.haskell.org, 1999. URL: http://www.haskell.org/onlinereport/.
S.L. Peyton-Jones. The Implementation of Functional Programming Languages. Series in Computer Science. Prentice Hall International, London, 1987.
Simon Peyton-Jones. Tackling the awkward squad. Technical report, Microsoft Research, Cambridge, 2001.
Rinus Plasmeijer and Marko van Eekelen. Concurrent clean (version 1.3). Technical report, High Level Software Tools B.V. and University of Nijmegen, 1998. URL
David A. Schmidt. Denotational Semantics. William C. Brown, Dubuque, Iowa, 1988.
Philip Wadler. Monads for functional programming. Lecture Notes for Marktoberdorf Summer School on Program Design Calculi, Springer-Verlag, August 1992.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Butterfield, A., Strong, G. (2002). Proving Correctness of Programs with IO —A Paradigm Comparison. In: Arts, T., Mohnen, M. (eds) Implementation of Functional Languages. IFL 2001. Lecture Notes in Computer Science, vol 2312. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46028-4_5
Download citation
DOI: https://doi.org/10.1007/3-540-46028-4_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43537-2
Online ISBN: 978-3-540-46028-2
eBook Packages: Springer Book Archive