Abstract
We present work in progress on a deep semantic embedding of the specification language Z and its deductive system (as defined by the draft Z standard) in the theorem prover Isabelle. Z is based on Zermelo-Fraenkel set theory and firstorder predicate logic, extended by a notion of schemas. Isabelle supports a fragment of higher-order predicate logic, in which object logics such as Z can be encoded as theories. This paper gives an overview of Z-in-Isabelle, including some example proofs, and discusses some of the major issues involved in formalizing Z in Isabelle.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
J.P. Bowen and M.J.C. Gordon. Z and HOL. In J.P. Bowen and J.A. Hall, editors, Z User Workshop, Cambridge 1994, Workshops in Computing, pages 141–167. Springer-Verlag, 1994.
S. M. Brien and J. E. Nicholls. Z base standard. Technical Monograph PRG-107, Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford, UK, November 1992. Accepted for ISO standardization, ISO/IEC JTC1/SC22.
J. Goguen, A. Stevens, H. Hilberdink, and K. Hobley. 2OBJ: A metalogical theorem prover based on equational logic. Philosophical Transactions of the Royal Society, Series A, 339:69–86, 1992.
W. T. Harwood. Proof rules for Balzac. Technical Report WTH/P7/001, Imperial Software Technology, Cambridge, UK, 1991.
R. B. Jones. ICL ProofPower. BCS FACS FACTS, Series III, 1(1): 10–13, Winter 1992.
L. E. Jordan. The Z syntax supported by Balzac-II/1. Technical Report LEJ/S1/001, Imperial Software Technology, Cambridge, UK, 1991.
S. Maharaj. Implementing Z in Lego. Master's thesis, Department of Computer Science, University of Edinburgh, September 1990.
A.Martin. Machine-Assisted Theorem-Proving for Software Engineering. PhD thesis, University of Oxford, 1994.
L.C. Paulson. The foundation of a generic theorem prover. The Journal of Automated Reasoning, 5(3):363–397, 1989.
L.C. Paulson. Isabelle. A Generic Theorem Prover. Lecture Notes in Computer Science. Springer-Verlag, 1994.
F. Pfenning and C. Elliot. Higher-order abstract syntax. In Proceedings of the ACM-SIGPLAN Conference on Programming Language Design and Implementation, 1988.
J. M Spivey. The Z Notation: A Reference Manual. Series in Computer Science. Prentice Hall International, 2nd edition, 1992.
J. C. P. Woodcock and S. M. Brien. W: A logic for Z. In J. E. Nicholls, editor, Z User Workshop, York 1991, Workshops in Computing, pages 77–96. Springer-Verlag, 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kraan, I., Baumann, P. (1995). Implementing Z in Isabelle. In: Bowen, J.P., Hinchey, M.G. (eds) ZUM '95: The Z Formal Specification Notation. ZUM 1995. Lecture Notes in Computer Science, vol 967. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60271-2_130
Download citation
DOI: https://doi.org/10.1007/3-540-60271-2_130
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60271-2
Online ISBN: 978-3-540-44782-5
eBook Packages: Springer Book Archive