Loose Specification and Refinement in Z
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.
KeywordsZ refinement semantics model containment states-andoperations loose specification
Unable to display preview. Download preview PDF.
- 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
- 7.J. Derrick and E.A. Boiten. Refinement in Z and Object-Z: Foundations and Advanced Applications. Springer-Verlag, 2001.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
- 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
- 16.J.C.P. Woodcock and J. Davies. Using Z: Specification, Refinement, and Proof. Prentice Hall, 1996.Google Scholar