Skip to main content
SpringerLink
Log in

Z and HOL

  • Conference paper
Book cover Z User Workshop, Cambridge 1994

Part of the book series: Workshops in Computing ((WORKSHOPS COMP.))

Abstract

A simple ‘shallow’ semantic embedding of the Z notation into the HOL logic is described. The Z notation is based on set theory and first order predicate logic and is typically used for human-readable formal specification. The HOL theorem proving system supports higher order logic and is used for machine-checked verification. A well-known case study is used as a running example. The presentation is intended to show people with some knowledge of Z how a tool such as HOL can be used to provide mechanical support for the notation, including mechanization of proofs. No specialized knowledge of HOL is assumed.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Andrews PD. An Introduction to Mathematical Logic and Type Theory: To Truth through Proof. Computer Science and Applied Mathematics Series. Academic Press, 1986.

    Google Scholar 

  2. Boulton RJ, Gordon AD, Harrison JR, Herbert JMJ, Van Tassel J. Experience with embedding hardware description languages in HOL. In Stavridou V, Melham TF, Boute RT (eds), Theorem Provers in Circuit Design: Theory, Practice and Experience: Proceedings of the IFIP TC10/WG 10.2 International Conference, IFIP Transactions A-10, pp 129–156. North-Holland, 1992.

    Google Scholar 

  3. Bowen JP. Comp.specification.z and Z FORUM frequently asked questions. In Bowen JP, Hall JA (eds), Z User Workshop, Cambridge 1994, Workshops in Computing. Springer-Verlag, 1994.

    Google Scholar 

  4. Bowen JP, Stavridou V. Safety-critical systems, formal methods and standards. IEE/BCS Software Engineering Journal, 8 (4): 189–209, 1993.

    Article  Google Scholar 

  5. Brien SM, Nicholls JE. Z base standard. Technical Monograph PRG-107, Oxford University Computing Laboratory, UK, 1992. Accepted for ISO standardization, ISO/IEC JTC1/SC22.

    Google Scholar 

  6. Church A. A formulation of the simple theory of types. The Journal of Symbolic Logic, 5: 56–68, 1940.

    Article  MathSciNet  MATH  Google Scholar 

  7. Collinson R. A simple demonstration of Balzac. Technical report, GCHQ, Fiddlers Green Lane, Cheltenham, Gloucestershire, UK, 1992.

    Google Scholar 

  8. Diller A. Z: An Introduction to Formal Methods. Wiley, 1990.

    Google Scholar 

  9. Gordon MJC, Melham TF (eds). Introduction to HOL: A Theorem-proving Environment for Higher-Order Logic. Cambridge University Press, 1993.

    Google Scholar 

  10. Gordon MJC, Milner R, Wadsworth CP. Edinburgh LCF: A Mechanised Logic of Computation, vol 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979.

    Google Scholar 

  11. Harwood WT. Proof rules for Balzac. Technical Report WTH/P7/001, Imperial Software Technology, Cambridge, UK, 1991.

    Google Scholar 

  12. Jones RB. ICL ProofPower. BCS FACS FACTS, Series III, 1 (1): 10–13, 1992.

    Google Scholar 

  13. Macdonald R, Randell GP, Sennett CT. Pattern matching in ML: A case study in refinement. Report No. 89004, RSRE (now DRA), Defence Research Agency, St. Andrews Road, Malvern, Worcestershire WR14 3PS, UK, 1989.

    Google Scholar 

  14. Maharaj S. Implementing Z in LEGO. Master’s thesis, University of Edinburgh, UK, 1990.

    Google Scholar 

  15. Maharaj S. Encoding Z schemas in type theory. In Geuves H (ed), Informal Proceedings of the 1993 Workshop on Types for Proofs and Programs, pp 209–218, 1993. Distributed electronically.

    Google Scholar 

  16. Martin A. Encoding W: A logic for Z in 2OBJ. In Woodcock JCP, Larsen PG (eds), FME’93: Industrial-Strength Formal Methods, vol 670 of Lecture Notes in Computer Science, pp 462–481. Springer-Verlag, 1993.

    Google Scholar 

  17. Melham T. Using recursive types to reason about hardware in Higher Order Logic. In Milne GJ (ed), The Fusion of Hardware Design and Verification, Proceedings of the IFIP WG10.2 Working Conference, pp 27–50. North-Holland, 1988.

    Google Scholar 

  18. Milner R, Tofte M, Harper R. The Definition of Standard ML. The MIT Press, 1990.

    Google Scholar 

  19. Neilson D. Machine support for Z: the zedB tool. In Nicholls JE (ed), Z User Workshop, Oxford 1990, Workshops in Computing, pp 105–128. Springer-Verlag, 1991.

    Google Scholar 

  20. Neilson D, Prasad D. zedB: A proof tool for Z built on B. In Nicholls JE (ed), Z User Workshop, York 1991, Workshops in Computing, pp 243–258. Springer-Verlag, 1992.

    Google Scholar 

  21. Paulson LC. Logic and Computation: Interactive Proof with Cambridge LCF, vol 2 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1987.

    Google Scholar 

  22. Paulson LC. A fixedpoint approach to implementing (co-)inductive definitions. Technical report, University of Cambridge, Computer Laboratory, UK, 1993. Draft.

    Google Scholar 

  23. Potter BF, Sinclair JE, Till D. An Introduction to Formal Specification and Z. Prentice Hall International Series in Computer Science, 1990.

    Google Scholar 

  24. Saaltink M. Z and EVES. Technical Report TR–91–5449–02, Odyyssey Research Associates, 265 Carling Avenue, Suite 506, Ottawa, Ontario K1S 2E1, Canada, 1991.

    Google Scholar 

  25. Saaltink M. Z and Eves. In Nicholls JE (ed), Z User Workshop, York 1991, Workshops in Computing, pp 223–242. Springer-Verlag, 1992.

    Google Scholar 

  26. Smith A. On recursive free types in Z. In Nicholls JE (ed), Z User Workshop, York 1991, Workshops in Computing, pp 3–39. Springer-Verlag, 1992.

    Google Scholar 

  27. Spivey JM. An introduction to Z and formal specifications. IEE/BCS Software Engineering Journal, 4 (1): 40–50, 1989.

    Article  Google Scholar 

  28. Spivey JM. The fuzz Manual. Computing Science Consultancy, 2 Willow Close, Garsington, Oxford OX9 9AN, UK, 2nd edition, 1992.

    Google Scholar 

  29. Spivey JM. The Z Notation: A Reference Manual. Prentice Hall International Series in Computer Science, 2nd edition, 1992.

    Google Scholar 

  30. Woodcock JCP, Brien SM. W: A logic for Z. In Nicholls JE (ed), Z User Workshop, York 1991, Workshops in Computing, pp 77–96. Springer-Verlag, 1992.

    Google Scholar 

  31. Xiaoping Jia. ZTC: A Type Checker for Z User’s Guide. Institute for Software Engineering, Department of Computer Science and Information Systems, DePaul University, Chicago, IL 60604, USA (e-mail: j is@cs. depaul. edu), 1994.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Oxford University Computing Laboratory, Programming Research Group, Wolfson Building Parks Road, Oxford, OX1 3QD, UK

    Jonathan Bowen

  2. University of Cambridge, Computer Laboratory New Museums Site, Pembroke Street, Cambridge, CB2 3QG, UK

    Mike Gordon

Authors
  1. Jonathan Bowen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mike Gordon
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Programming Research Group, Oxford University Computing Laboratory, Wolfson Buliding, Parks Road, OX1 3QD, Oxford, UK

    J. P. Bowen MA

  2. Praxis Systems plc, 20 Manvers Street, BA1 1PX, Bath, UK

    J. A. Hall MA, DPhil, CEng

Rights and permissions

Reprints and permissions

Copyright information

© 1994 British Computer Society

About this paper

Cite this paper

Bowen, J., Gordon, M. (1994). Z and HOL. In: Bowen, J.P., Hall, J.A. (eds) Z User Workshop, Cambridge 1994. Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3452-7_9

Download citation

  • DOI: https://doi.org/10.1007/978-1-4471-3452-7_9

  • Publisher Name: Springer, London

  • Print ISBN: 978-3-540-19884-0

  • Online ISBN: 978-1-4471-3452-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation