Abstract
This work is a case study in program verification: We have written a simple parser and a corresponding pretty-printer in a non-strict functional programming language with lifted pairs and functions (Haskell). A natural aim is to prove that the programs are, in some sense, each other’s inverses. The presence of partial and infinite values in the domains makes this exercise interesting, and having lifted types adds an extra spice to the task. We have tackled the problem in different ways, and this is a report on the merits of those approaches. More specifically, we first describe a method for testing properties of programs in the presence of partial and infinite values. By testing before proving we avoid wasting time trying to prove statements that are not valid. Then we prove that the programs we have written are in fact (more or less) inverses using first fixpoint induction and then the approximation lemma.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Chakravarty, M., et al.: The Haskell 98 Foreign Function Interface 1.0, An Addendumto the Haskell 98 Report (2003), Available online at http://www.haskell.org/definition/
Claessen, K., Hughes, J.: QuickCheck: A lightweight tool for random testing of Haskell programs. In: Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming, pp. 268–279. ACM Press, New York (2000)
Faxén, K.-F.: A static semantics for Haskell. Journal of Functional Programming 12(4&5), 295–357 (2002)
Gibbons, J., Hutton, G.: Proof methods for corecursive programs. Submitted to Fundamenta Informaticae Special Issue on Program Transformation, Available online at http://www.cs.nott.ac.uk/~gmh/bib.html (March 2004)
Hughes, J.: Why functional programming matters. Computer Journal 32(2), 98–107 (1989)
Hutton, G., Gibbons, J.: The generic approximation lemma. Information Processing Letters 79(4), 197–201 (2001)
Jansson, P., Jeuring, J.: Polytypic data conversion programs. Science of Computer Programming 43(1), 35–75 (2002)
Johann, P., Voigtländer, J.: Free theorems in the presence of seq. In: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 99–110. ACM Press, New York (2004)
Lämmel, R., Jones, S.P.: Scrap your boilerplate: A practical design pattern for generic programming. ACM SIGPLAN Notices 38(3), 26–37 (2003)
Pardo, A.: Monadic corecursion – definition, fusion laws, and applications. In: Jacobs, B., Moss, L., Reichel, H., Rutten, J. (eds.) Electronic Notes in Theoretical Computer Science, vol. 11, Elsevier, Amsterdam (2000)
Jones, S.P.: Tackling the Awkward Squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell. In: Engineering Theories of Software Construction. NATO Science Series: Computer & Systems Sciences, vol. 180, pp. 47–96. IOS Press, Amsterdam (2001). Updated version available online at http://research.microsoft.com/~simonpj/
Jones, S.P. (ed.): Haskell 98 Language and Libraries, The Revised Report. Cambridge University Press, Cambridge (2003)
Sands, D.: Total correctness by local improvement in the transformation of functional programs. ACM Transactions on Programming Languages and Systems (TOPLAS) 18(2), 175–234 (1996)
Schmidt, D.A.: Denotational Semantics: A Methodology for Language Development. W.C. Brown, Dubuque, Iowa (1988)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Danielsson, N.A., Jansson, P. (2004). Chasing Bottoms. In: Kozen, D. (eds) Mathematics of Program Construction. MPC 2004. Lecture Notes in Computer Science, vol 3125. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27764-4_6
Download citation
DOI: https://doi.org/10.1007/978-3-540-27764-4_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22380-1
Online ISBN: 978-3-540-27764-4
eBook Packages: Springer Book Archive