Loose Specification and Refinement in Z

  • Eerke Boiten
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2272)


Z is a specification notation with a model-based semantics, but in contrast to most such languages, its normal refinement relation is not defined in terms of model containment. This paper investigates this phenomenon, leading to a variety of observations concerning the relation between Z semantics and refinement.


refinement semantics model containment states-andoperations loose specification 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    J.-R. Abrial. The B-Book: Assigning programs to meanings. Cambridge University Press, 1996.Google Scholar
  2. 2.
    R. Barden, S. Stepney, and D. Cooper. Z in Practice. Prentice Hall, 1994.Google Scholar
  3. 3.
    E.A. Boiten, H. Bowman, J. Derrick, and M. Steen. Viewpoint consistency in Z and LOTOS: A case study. In J. Fitzgerald, C.B. Jones, and P. Lucas, editors, FME’97: Industrial Application and Strengthened Foundations of FormalMethods, volume 1313 of Lecture Notes in Computer Science, pages 644–664. Springer-Verlag, September 1997.Google Scholar
  4. 4.
    E.A. Boiten and J. Derrick. IO-refinement in Z. In A. Evans, D. Duke, and T. Clark, editors, 3rd BCS-FACS Northern FormalMetho ds Workshop. Springer-Verlag, September 1998.
  5. 5.
    C. Bolton, J. Davies, and J.C.P. Woodcock. On the refinement and simulation of data types and processes. In K. Araki, A. Galloway, and K. Taguchi, editors, International conference on Integrated FormalMetho ds 1999 (IFM’99), pages 273–292, York, July 1999. Springer-Verlag.Google Scholar
  6. 6.
    A.L.C. Cavalcanti and J.C.P. Woodcock. ZRC — a Refinement Calculus for Z. FormalAsp ects of Computing, 10(3):267–289, 1998.zbMATHCrossRefGoogle Scholar
  7. 7.
    J. Derrick and E.A. Boiten. Refinement in Z and Object-Z: Foundations and Advanced Applications. Springer-Verlag, 2001.Google Scholar
  8. 8.
    I.J. Hayes and J.W. Sanders. Specification by interface separation. FormalAsp ects of Computing, 7(4):430–439, 1995.zbMATHCrossRefGoogle Scholar
  9. 9.
    M.C. Henson and S. Reeves. New foundations for Z. In J. Grundy, M. Schwenke, and T. Vickers, editors, InternationalR efinement Workshop & FormalMetho ds Pacific’ 98, Discrete Mathematics and Theoretical Computer Science, pages 165–179, Canberra, September 1998. Springer-Verlag.Google Scholar
  10. 10.
    M.C. Henson and S. Reeves. Revising Z: Part I-Logic and semantics. Formal Aspects of Computing, 11(4):359–380, 1999.zbMATHCrossRefGoogle Scholar
  11. 11.
    M.C. Henson and S. Reeves. Revising Z: Part II-Logical development. Formal Aspects of Computing, 11(4):381–401, 1999.zbMATHCrossRefGoogle Scholar
  12. 12.
    ISO/IEC. Formal Specification — Z Notation — Syntax, Type and Semantics: 2nd Final Committee Draft. International Standard CD 13568.2, International Standards Organization, 2000.Google Scholar
  13. 13.
    G. Smith. The Object-Z Specification Language. Kluwer Academic Publishers, 2000.Google Scholar
  14. 14.
    J. M. Spivey. The Z notation: A reference manual. Prentice Hall, 2nd edition, 1992.Google Scholar
  15. 15.
    S.H. Valentine. Inconsistency and undefinedness in Z — a practical guide. In J. P. Bowen, A. Fett, and M. G. Hinchey, editors, ZUM’98: The Z Formal Specification Notation, volume 1493 of Lecture Notes in Computer Science, pages 233–249. Springer-Verlag, September 1998.CrossRefGoogle Scholar
  16. 16.
    J.C.P. Woodcock and J. Davies. Using Z: Specification, Refinement, and Proof. Prentice Hall, 1996.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Eerke Boiten
    • 1
  1. 1.Computing LaboratoryUniversity of Kent at CanterburyCanterbury KentUK

Personalised recommendations