Abstract
We investigate the relation between the semantic models of Z, as proposed by the Z draft standard, and of the polymorphic version of higher-order logic that is the basis for proof systems such as HOL and Isabelle/HOL. Disregarding the names in schema types, the type models of the two systems can be identified up to isomorphism. That isomorphism determines to a large extent how terms of Z can be represented in higher-order logic. This justifies the soundness of proof support for Z based on higher-order logic, such as the encoding \(\ensuremath{\mathcal{HOL\mbox{-}Z}}\) of Z in Isabelle/HOL.
The comparison of the two semantic models also motivates a discussion of open issues in the development of a complete semantics of Z, in particular concerning the type system, generic constructs, and approaches to base the semantics of Z on a small kernel language.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Andrews, P.B.: An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Academic Press, London (1986)
Bowen, J.P., Gordon, M.J.C.: A shallow embedding of Z in HOL. Information and Software Technology 37(5–6), 269–276 (1995)
Gordon, M.J.C., Melham, T.M. (eds.): Introduction to HOL: A theorem proving environment for higher order logics. Cambridge UniversityPress, Cambridge (1993)
Henson, M.C., Reeves, S.: A logic for the schema calculus. In: Bowen, J.P., Fett, A., Hinchey, M.G. (eds.) ZUM 1998. LNCS, vol. 1493, pp. 172–192. Springer, Heidelberg (1998)
Jones, R.B.: ICL ProofPower. BCS FACS FACTS Series III 1(1), 10–13 (1992)
Kolyang, Santen, T., Wolff, B.: A structure preserving encoding of Z in Isabelle/HOL. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol. 1125, pp. 283–298. Springer, Heidelberg (1996)
Martin, A.: Approaches to proof in Z – or – whyeff ective proof tool support for Z is hard. Technical Report 97-34, Software Verification Research Centre (1997)
Nicholls, J. (ed.): Z Notation – version 1.2. Draft ISO standard (1995)
Paulson, L.C.: Isabelle. LNCS, vol. 828. Springer, Heidelberg (1994)
Saaltink, M.: Inferring generic actuals in Z/EVES. The Z/EVES mailing list (May 1997) Email: zeves@ora.on.ca
Smith, G.P.: An Object-Oriented Approach to Formal Specification. PhD thesis, Universityof Queensland, Australia (1992)
Spivey, J.M.: The fuzz manual. Computing Science Consultancy, Oxford, UK (1992)
Spivey, J.M.: The Z Notation – A Reference Manual, 2nd edn. Prentice Hall International Series in Computer Science (1992)
Toyn, I.: Z notation – draft 0.7. Proposal to the ISO Z Standards Panel (December 1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Santen, T. (1998). On the Semantic Relation of Z and HOL. In: Bowen, J.P., Fett, A., Hinchey, M.G. (eds) ZUM ’98: The Z Formal Specification Notation. ZUM 1998. Lecture Notes in Computer Science, vol 1493. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-49676-2_8
Download citation
DOI: https://doi.org/10.1007/978-3-540-49676-2_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65070-6
Online ISBN: 978-3-540-49676-2
eBook Packages: Springer Book Archive