Abstract
Despite being widely regarded as a gloss on first-order logic and set theory, Z has not been found to be very supportive of proof. This paper attempts to distinguish between the different philosophies of proof in Z. It discusses some of the issues which must be addressed in creating a proof technology for Z, namely schemas, undefinedness, and what kind of logic to use.
Acknowledgements
If I have any insight in this area, it has been gained in discussions with members of the Z Standards panel. Anthony Hall helped to make stark the choices faced in dealing with undefinedness, and discussions with Martin Henson have greatly helped my understanding and exposition.
Paper written at the University of Southampton.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
R. D. Arthan. Undefinedness in Z: Issues for specification and proof, 1996. Presented at CADE-13 Workshop on Mechanization of Partial Functions.
Peter Baumann. Private Communication, April 1994.
Anthony Bloesch, Ed Kazmierczak, Peter Kearney, and Owen Traynor. The Cogito methodology and system. In Asia-Pacific Software Engineering Conference’ 94, pages 345–355, 1994.
J. P. Bowen, A. Fett, and M. G. Hinchey, editors. ZUM’98: The Z Formal Specification Notation, 11th International Conference of Z Users, Berlin, Germany, 24-26 September 1998, volume 1493 of Lecture Notes in Computer Science. Springer-Verlag, 1998.
J. P. Bowen and M. J. C. Gordon. A shallow embedding of Z in HOL. Information and Software Technology, 37(5-6):269–276, 1995.
Stephen Brien and Andrew Martin. A calculus for schemas in Z. J. Symbolic Computation, 2000. To appear.
Stephen M. Brien. A Logic and Model for the Z Standard. D.Phil. thesis, University of Oxford, 1998.
Herbert B. Enderton. A Mathematical Introduction to Logic. Academic Press, 1972.
M. C. Henson and S. Reeves. A logic for the schema calculus. In Bowen et al. [4], pages 172–191.
Martin Henson and Steve Reeves. New foundations for Z. In Jim Grundy, Martin Schwenke, and Trevor Vickers, editors, IRW/FMP’98. Springer-Verlag, 1998.
Martin C. Henson and Steve Reeves. Investigating Z. Technical Report CSM-317, Department of Computer Science, University of Essex, 1998. Journal of Logic and Computation, to appear.
Cliff B. Jones. Systematic Software Development Using VDM. Prentice-Hall Intenational, second edition, 1990.
R. B. Jones. ICL ProofPower. BCS FACS FACTS, Series III, 1(1):10–13, Winter 1992.
Kolyang, T. Santen, and B. Wolff. A structure preserving encoding of Z in Isabelle/HOL. In 1996 International Conference on Theorem Proving in Higher Order Logic. Springer-Verlag, 1996.
Ina Kraan and Peter Baumann. Implementing Z in Isabelle. In Jonathan P. Bowen and Michael G. Hinchey, editors, ZUM’95: The Z Formal Specification Notation, volume 967 of LNCS, pages 355–373. Springer-Verlag, 1995.
Peter J. L. Lupton. Z and undefinedness. Technical Report PRG/91/68, Z Standards Panel / Programming Research Group, 1991.
A. Martin. Encoding W: A logic for Z in 2OBJ. In J. C. P. Woodcock and P. G. Larsen, editors, FME’93: Industrial-Strength Formal Methods, volume 670 of Lecture Notes in Computer Science, pages 462–481. Formal Methods Europe, Springer-Verlag, 1993.
Andrew Martin. Why effective proof tool support for Z is hard. Technical report 97-34, Software Verification Research Centre, School of Information Technology, The University of Queensland, Brisbane 4072. Australia, November 1997.
Elliott Mendelson. Introduction to Mathematical Logic. Mathematics Series. Wadsworth and Brooks/Cole, 1987.
John Nicholls, editor. Z Notation. Z Standards Panel, ISO Panel JTC1/SC22/WG19 (Rapporteur Group for Z), 1995. Version 1.2, ISO Committee Draft; CD 13568.
S. Owre, S. Rajan, J.M. Rushby, N. Shankar, and M.K. Srivas. PVS: Combining specification, proof checking, and model checking. In Rajeev Alur and Thomas A. Henzinger, editors, Computer-Aided Verification, CAV’ 96, number 1102 in Lecture Notes in Computer Science, pages 411–414, New Brunswick, NJ, July/August 1996. Springer-Verlag.
B. F. Potter, J. E. Sinclair, and D. Till. An Introduction to Formal Specification and Z. Prentice Hall International Series in Computer Science, 2nd edition, 1996.
M. Saaltink. The Z/EVES system. In J. P. Bowen, M. G. Hinchey, and D. Till, editors, ZUM’97: The Z Formal Specification Notation, volume 1212 of Lecture Notes in Computer Science, pages 72–85. Springer-Verlag, 1997.
T. Santen. On the semantic relation of Z and HOL. In Bowen et al. [4], pages96–115.
J. M. Spivey. Understanding Z: A Specification Language and its Formal Semantics, volume 3 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, January 1988.
J. M. Spivey. The Z Notation: A Reference Manual. Prentice-Hall, second edition, 1992.
I. Toyn. Formal reasoning in the Z notation using CADiZ. In Proc. 2nd Workshop on User Interfaces to Theorem Provers, York, July 1996.
J. C. P. Woodcock and S. M. Brien. W: A Logic for Z. In Proceedings 6th Z User Meeting. Springer-Verlag, 1992.
[29] J. C. P. Woodcock and J. Davies. Using Z: Specification, Proof and Refinement. Prentice Hall International Series in Computer Science, 1996.
[30] J. C. P. Woodcock and M. Loomes. Software Engineering Mathematics: Formal Methods Demystified. Pitman, 1988.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Spinger-Verlag Berlin Heidelberg
About this paper
Cite this paper
Martin, A. (1999). Relating Z and first-order logic. In: Wing, J.M., Woodcock, J., Davies, J. (eds) FM’99 — Formal Methods. FM 1999. Lecture Notes in Computer Science, vol 1709. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48118-4_17
Download citation
DOI: https://doi.org/10.1007/3-540-48118-4_17
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66588-5
Online ISBN: 978-3-540-48118-8
eBook Packages: Springer Book Archive