Skip to main content
SpringerLink
Log in

Loose Specification and Refinement in Z

  • Conference paper
  • First Online:
ZB 2002:Formal Specification and Development in Z and B (ZB 2002)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2272))

Included in the following conference series:

Abstract

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.

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. J.-R. Abrial. The B-Book: Assigning programs to meanings. Cambridge University Press, 1996.

    Google Scholar 

  2. R. Barden, S. Stepney, and D. Cooper. Z in Practice. Prentice Hall, 1994.

    Google Scholar 

  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. 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. http://www.ewic.org.uk/.

  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. A.L.C. Cavalcanti and J.C.P. Woodcock. ZRC — a Refinement Calculus for Z. FormalAsp ects of Computing, 10(3):267–289, 1998.

    Article  MATH  Google Scholar 

  7. J. Derrick and E.A. Boiten. Refinement in Z and Object-Z: Foundations and Advanced Applications. Springer-Verlag, 2001.

    Google Scholar 

  8. I.J. Hayes and J.W. Sanders. Specification by interface separation. FormalAsp ects of Computing, 7(4):430–439, 1995.

    Article  MATH  Google Scholar 

  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. M.C. Henson and S. Reeves. Revising Z: Part I-Logic and semantics. Formal Aspects of Computing, 11(4):359–380, 1999.

    Article  MATH  Google Scholar 

  11. M.C. Henson and S. Reeves. Revising Z: Part II-Logical development. Formal Aspects of Computing, 11(4):381–401, 1999.

    Article  MATH  Google Scholar 

  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. G. Smith. The Object-Z Specification Language. Kluwer Academic Publishers, 2000.

    Google Scholar 

  14. J. M. Spivey. The Z notation: A reference manual. Prentice Hall, 2nd edition, 1992.

    Google Scholar 

  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.

    Chapter  Google Scholar 

  16. J.C.P. Woodcock and J. Davies. Using Z: Specification, Refinement, and Proof. Prentice Hall, 1996.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computing Laboratory, University of Kent at Canterbury, CT2 7NF, Canterbury Kent, UK

    Eerke Boiten

Authors
  1. Eerke Boiten
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Laboratoire LSR, IMAG, CNRS, 681,rue de la Passerelle, 38402, Saint Martin d’Hères Cedex, France

    Didier Bert

  2. SCISM, Centre for Applied Fromal Methods, SouthBank University, Borough Road, SE1 0AA, London, UK

    Jonathan P. Bowen

  3. Department of Computer Science, University of Essex, Wivenhoe Park, CO4 3SQ, Colchester, UK

    Martin C. Henson

  4. CAESER, The School of Computer Science and Engineering, The University of New South Wales, UNSW, 2052, Sydney, NSW, Australia

    Ken Robinson

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Boiten, E. (2002). Loose Specification and Refinement in Z. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds) ZB 2002:Formal Specification and Development in Z and B. ZB 2002. Lecture Notes in Computer Science, vol 2272. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45648-1_12

Download citation

  • DOI: https://doi.org/10.1007/3-540-45648-1_12

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43166-4

  • Online ISBN: 978-3-540-45648-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation