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.
Keywords
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
J.-R. Abrial. The B-Book: Assigning programs to meanings. Cambridge University Press, 1996.
R. Barden, S. Stepney, and D. Cooper. Z in Practice. Prentice Hall, 1994.
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.
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/.
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.
A.L.C. Cavalcanti and J.C.P. Woodcock. ZRC — a Refinement Calculus for Z. FormalAsp ects of Computing, 10(3):267–289, 1998.
J. Derrick and E.A. Boiten. Refinement in Z and Object-Z: Foundations and Advanced Applications. Springer-Verlag, 2001.
I.J. Hayes and J.W. Sanders. Specification by interface separation. FormalAsp ects of Computing, 7(4):430–439, 1995.
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.
M.C. Henson and S. Reeves. Revising Z: Part I-Logic and semantics. Formal Aspects of Computing, 11(4):359–380, 1999.
M.C. Henson and S. Reeves. Revising Z: Part II-Logical development. Formal Aspects of Computing, 11(4):381–401, 1999.
ISO/IEC. Formal Specification — Z Notation — Syntax, Type and Semantics: 2nd Final Committee Draft. International Standard CD 13568.2, International Standards Organization, 2000.
G. Smith. The Object-Z Specification Language. Kluwer Academic Publishers, 2000.
J. M. Spivey. The Z notation: A reference manual. Prentice Hall, 2nd edition, 1992.
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.
J.C.P. Woodcock and J. Davies. Using Z: Specification, Refinement, and Proof. Prentice Hall, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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