Abstract
We develop a theory of program specification using the notion of refinement type. This provides a notion of structured specification, useful for verification and program development. We axiomatise the satisfaction of specifications by programs as a generalised typing relation and give rules for refining specifications. A per semantics based on Henkin models is given, for which the system is proven to be sound and complete.
Chapter PDF
References
Aspinall, D. (1995) Subtyping with singleton types, in `Proceedings of Computer Science Logic `94’, Vol. 933 of LNCS.
Aspinall, D. & Compagnoni, A. (1996) Subtyping dependent types, in `Proceedings of the eleventh IEEE Symposium on Logic in Computer Science’.
Burn, G. L. (1992) A logical framework for program analysis, in J. Launchbury & P. Sansom, Eds, ‘Proceedings of the 1992 Glasgow Functional Programming Workshop’, Springer-Verlag Workshops in Computer Science series, pp. 3042.
Burstall, R. & McKinna, J. (1992) Deliverables: A categorical approach to program development in type theory, in `Mathematical Foundations of Computer Science: 18th International Symposium’, Vol. 711 of Lecture Notes in Computer Science, pp. 32–67. An earlier version appeared as LFCS Technical Report ECS-LFCS-92–242.
Denney, E. (1997) Refining Refinement Types, in `Informal Proceedings of Types Workshop on Subtyping, Inheritance and Modular Development of Proofs’, University of Durham.
Denney, E. (1998) A General Theory of Program Refinement. PhD thesis, Depart- ment of Computer Science, University of Edinburgh. Forthcoming.
Feferman, S. (1985) A theory of variable types, in `Proceedings of the Fifth Latin American Symposium on Mathematical Logic’, Vol. 19 of Revista Colombiana de Matemâticas.
Freeman, T. & Pfenning, E. (1991) Refinement types for ML, in `Proceedings of the SIGPLAN’91 Symposium on Language Design and Implementation’, ACM Press, pp. 268–277.
Hayashi, S. (1994) Logic of refinement types, in `Types for Proofs and programs’
Vol. 806 of Lecture Notes in Computer Science,Springer Verlag.
Henkin, L. (1950) Completeness in the theory of types. Journal of Symbolic Logic 15 (2), 81–91.
Luo, Z. (1991) Program specification and data refinement in type theory. LFCS Technical Report ECS-LFCS-90–131, Department of Computer Science, University of Edinburgh.
McKinna, J. (1992) Deliverables: A Categorical Approach to Program Development in Type Theory. PhD thesis, Department of Computer Science, University of Edinburgh.
Mitchell, J. (1996) Foundations for Programming Languages, Foundations of Computing Series, MIT Press.
Morgan, C. (1994) Programming from Specifications. Prentice Hall.
Nielson, H. & Nielson, F. (1988) Automatic binding time analysis for a typed a-calculus, in `Proceedings of the Fifteenth Annual ACM Symposium on Prin-ciples of Programming Languages’.
Nordström, B., Petersson, K. & Smith, J. M. (1990) Programming in Martin-Lof’s Type Theory. Vol. 7 of Monographs on Computer Science,Oxford University Press.
van Dalen, D. (1994) Logic and Structure. Springer-Verlag.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Denney, E. (1998). Refinement types for specification. In: Gries, D., de Roever, WP. (eds) Programming Concepts and Methods PROCOMET ’98. IFIP — The International Federation for Information Processing. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35358-6_13
Download citation
DOI: https://doi.org/10.1007/978-0-387-35358-6_13
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-6299-0
Online ISBN: 978-0-387-35358-6
eBook Packages: Springer Book Archive