Abstract
This paper presents a method that facilitates formal reasoning about the correctness of programs. In this method, properties of programs (e.g. pre- and postconditions of functions) are described in terms of type invariants. Subtype marks are annotations attached to types and denote type invariants. A large amount of program properties expressed with subtype marks are verifiable fully automatically by an appropriate type system; the rest can be proven with a proof system. In this paper an eager pure functional language with a type system supporting subtype marks is briefly described. By assigning an interpretation to subtype marks, a concept of program correctness is introduced. The soundness of the presented type system is investigated.
Supported by GVOP-3.2.2-2004-07-0005/3.0 ELTE IKKK.
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.
References
de Mol, M., van Eekelen, M., Plasmeijer, R.: Theorem Proving for Functional Programmers, Sparkle: A Functional Theorem Prover. In: Arts, T., Mohnen, M. (eds.) IFL 2002. LNCS, vol. 2312, pp. 55–71. Springer, Heidelberg (2002)
Plasmeijer, R., van Eekelen, M.: Concurrent Clean Version 2.0 Language Report (2001), http://www.cs.ru.nl/~clean/Manuals/manuals.html
Koopman, P.: Language support to enforce constraints on data types. Technical Report 96-37, Computer Science, Leiden University, The Netherlands (1996)
van Arkel, D.F.R.: Annotated Types. M.Sc. thesis, Rijksuniversiteit te Leiden, Vakgroep Informatica (1998)
Kozsik, T., van Arkel, D., Plasmeijer, R.: Subtyping with strengthening type invariants. In: Mohnen, M., Koopman, P. (eds.) Proceedings of the 12th International Workshop on Implementation of Functional Languages. Aachener Informatik-Berichte, Aachen, Germany pp. 315–330 (2000)
Kozsik, T.: Subtyping with subtype marks. Technical Report 2003-P05, Eötvös Loránd University, Faculty of Informatics, Budapest, Hungary (2003)
Kozsik, T.: Tutorial on Subtype Marks. In: Horváth, Z. (ed.) CEFP 2005. LNCS, vol. 4164, pp. 191–222. Springer, Heidelberg (2006)
Barendsen, E., Smetsers, S.: Uniqueness typing for functional languages with graph rewriting semantics. Mathematical Structures in Comp. Sci. 6, 579–612 (1996)
Kozsik, T.: Soundness of the type system of Senyv. Technical Report, Eötvös Loránd University, Faculty of Informatics, Budapest, Hungary (to appear, 2007)
Peyton Jones, S., Washburn, G., Weirich, S.: Wobbly types: type inference for generalised algebraic data types. Technical Report MS-CIS-05-26, Computer and Information Science Department, University of Pennsylvania (2004)
McBride, C.: Epigram: Practical Programming with Dependent Types. In: Vene, V., Uustalu, T. (eds.) AFP 2004. LNCS, vol. 3622, pp. 130–170. Springer, Heidelberg (2005)
Chen, C., Xi, H.: Combining Programming with Theorem Proving. In: ACM SIGPLAN Int’l Conf. on Functional Programming. pp. 66–77 (2005)
Nanevski, A., Morrisett, G., Birkedal, L.: Polymorphism and Separation in Hoare Type Theory. In: ACM SIGPLAN Int’l Conf. on Functional Programming. pp. 62–73 (2006)
Mandelbaum, Y., Walker, D., Harper, R.: An Effective Theory of Type Refinements. In: ACM SIGPLAN Int’l Conf. on Functional Programming. pp. 213–225 (2003)
Clark, D., Potter, J., Noble, J.: Ownership types for flexible alias protection. In: Proceedings of Conference on Object-Oriented Programming, Languages, and Applications, ACM Press, New York (1998)
Igarashi, A., Kobayashi, N.: Resource usage analysis. In: Symposium on Principles of Programming Languages. pp. 331–342 (2002)
Brady, E., Hammond, K.: A dependently typed framework for static analysis of program execution costs. In: Butterfield, A., Grelck, C., Huch, F. (eds.) IFL 2005. LNCS, vol. 4015, pp. 74–90. Springer, Heidelberg (2006)
Horváth, Z., Hernyák, Z., Zsók, V.: Control Language for Distributed Clean. Acta Cybernetica 17, 247–271 (2005)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kozsik, T. (2007). Proving Program Properties Specified with Subtype Marks. In: Horváth, Z., Zsók, V., Butterfield, A. (eds) Implementation and Application of Functional Languages. IFL 2006. Lecture Notes in Computer Science, vol 4449. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74130-5_10
Download citation
DOI: https://doi.org/10.1007/978-3-540-74130-5_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74129-9
Online ISBN: 978-3-540-74130-5
eBook Packages: Computer ScienceComputer Science (R0)