Towards a Z Method: Axiomatic Specification in Z

  • Jon Hall
  • John McDermid
Conference paper
Part of the Workshops in Computing book series (WORKSHOPS COMP.)


Z is a rich and expressive specification language. It is possible to use Z to produce clear, abstract and elegant specifications; it is also possible to use Z to produce meaningless specifications.

One of the overall aims of the research work in York is to produce a Z-based method for the meaningful specification and development of safety critical systems. Our primary aim, in this paper, is to address the narrower technical issues of the rôle of axiomatic specification techniques in the production of Z specifications. We return to the discussion of broader methodological issues in the conclusions.


Proof Obligation Denotational Semantic Safety Critical System Prototype Verification System Order Sort 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    S. Brien, J. Nicholls: “Z Base Standard Version 1.0”. (1992).Google Scholar
  2. [2]
    J.A. Goguen: “Order-Sorted Algebra I: Equational Deduction for Multiple Inheritance, Overloading, Exceptions and Partial Operations”. Technical Report SRI-CSL-89–10, SRI International, Computer Science Lab., (July 1989).Google Scholar
  3. [3]
    J.A. Goguen: “Theorem Proving and Algebra”. Prentice-Hall International, to appear. (1992).Google Scholar
  4. [4]
    J.G. Hall: “Type and Value Calculations in Z”. To appear.Google Scholar
  5. [5]
    N. Shankar, S. Owre, J.M. Rushby: “A Tutorial on Specification and Verification Using PVS (Beta Release)”. Computer Science Laboratory, SRI International (March 1993).Google Scholar
  6. [6]
    J.M. Spivey: “The Z Notation: A Reference Manual” Second Edition. Prentice Hall International Series in Computer Science (1992).Google Scholar
  7. [7]
    P.J. Whysall: “Object Oriented Specification and Refinement”. D.Phil. Thesis, York University (1991).Google Scholar

Copyright information

© British Computer Society 1994

Authors and Affiliations

  • Jon Hall
    • 1
  • John McDermid
    • 1
  1. 1.Department of Computer ScienceUniversity of YorkYorkUK

Personalised recommendations