Towards a Z Method: Axiomatic Specification in Z
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.
KeywordsProof Obligation Denotational Semantic Safety Critical System Prototype Verification System Order Sort
Unable to display preview. Download preview PDF.
- S. Brien, J. Nicholls: “Z Base Standard Version 1.0”. (1992).Google Scholar
- 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
- J.A. Goguen: “Theorem Proving and Algebra”. Prentice-Hall International, to appear. (1992).Google Scholar
- J.G. Hall: “Type and Value Calculations in Z”. To appear.Google Scholar
- 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
- J.M. Spivey: “The Z Notation: A Reference Manual” Second Edition. Prentice Hall International Series in Computer Science (1992).Google Scholar
- P.J. Whysall: “Object Oriented Specification and Refinement”. D.Phil. Thesis, York University (1991).Google Scholar