Abstract
This paper discusses the refinement of systems specified in Z when we relax the assumption that the refinement will preserve the atomicity of operations. Data refinement is a well established technique for transforming specifications of abstract data types into ones which are closer to an eventual implementation. To verify a refinement a retrieve relation is used which relates the concrete to abstract states and allow the comparison between the data types to be made on a step by step basis by comparing an abstract operation with its concrete counterpart. A step by step comparison is possible because the two abstract data types are assumed to be conformal, i.e. there is a one-one correspondence between abstract and concrete operations, so each abstract operation has a concrete counterpart. In this paper we relax that assumption to discuss refinements where an abstract operation is refined by, not one, but a sequence of concrete operations. Such non-conformal or non-atomic refinements arise naturally in a number of settings and we illustrate our derivations with a simple example of a bank accounting system.
Chapter PDF
Similar content being viewed by others
References
Jean-Raymond Abrial and Louis Mussat. Specification and design of a transmission protocol by successive refinements using B. In Manfred Broy and Birgit Schieder, editors, Mathematical Methods in Program Development, volume 158 of NATO ASI Series F: Computer and Systems Sciences, pages 129–200. Springer, 1997.
L. Aceto. Action refinement in process algebras. CUP, London, 1992.
E.A. Boiten and J. Derrick. IO-refinement in Z. In 3rd BCS-FACS Northern Formal Methods Workshop, Electronic Workshops in Computing. Springer Verlag, September 1998.
M. Butler. An approach to the design of distributed systems with B AMN. In J. P. Bowen, M. G. Hinchey, and D. Till, editors, ZUM’97: The Z formal specification notation, LNCS 1212, pages 223–241, Reading, April 1997. Springer-Verlag.
I.J. Hayes and J.W. Sanders. Specification by interface separation. Formal Aspects of Computing, 7(4):430–439, 1995.
He Jifeng and C.A.R. Hoare. Prespecification and data refinement. In Data Refinement in a Categorical Setting, Technical Monograph, number PRG-90. Oxford University Computing Laboratory, November 1990.
J. Sinclair and J. Woodcock. Event refinement in state-based concurrent systems. Formal Aspects of Computing, 7:266–288, 1995.
J. M. Spivey. The Z notation: A reference manual. Prentice Hall, 1989.
S. Stepney, D. Cooper, and J. C. P. Woodcock. More powerful data refinement in Z. In J. P. Bowen, A. Fett, and M. G. Hinchey, editors, ZUM’98: The Z Formal Specification Notation, volume 1493 of LNCS, pages 284–307. Springer-Verlag, 1998.
J. 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
© 1999 Spriger-Verlag Berlin Heidelberg
About this paper
Cite this paper
Derrick, J., Boiten, E. (1999). Non-atomic refinement in Z. In: Wing, J.M., Woodcock, J., Davies, J. (eds) FM’99 — Formal Methods. FM 1999. Lecture Notes in Computer Science, vol 1709. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48118-4_28
Download citation
DOI: https://doi.org/10.1007/3-540-48118-4_28
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66588-5
Online ISBN: 978-3-540-48118-8
eBook Packages: Springer Book Archive