Non-atomic refinement in Z

Derrick, John and Boiten, Eerke (1999) Non-atomic refinement in Z. In: Wing, Jeannetter M. and Woodchck, Jim and Davies, Jim, eds. FM’99 — Formal Methods. Lecture Notes In Computer Science, 1709 . Springer-Verlag Berlin, Berlin, Germany pp. 1477-1496. ISBN 978-3-540-66588-5. (The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided)

The full text of this publication is not available from this repository. (Contact us about this Publication)
Official URL


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.

Item Type: Conference or workshop item (Paper)
Additional information: Conference Information: Event title: 1st World Congress on Formal Methods in the Development of Computing Systems (FM 99); Event location: Toulouse, France; Event dates: Sep 20-24, 1999; AMAST; Aerospatiale Airbus; Alcatel Space; CCIT; CEPIS; CNES; CNRS; Cap Gemimi; Carnegie Mellon Univ; Conseil Reg Midi Pyrenees; DGA; EATCS; ESA; ETAPS; European Union; FACS; FME; France Telecom; IFIP; INRIA; IPSJ; IRIT; JSSST; LAAS; Mairie Toulouse; Matra Marconi Space; ONERA; Tech Univ Delft; Tech Univ Denmark; Tech Univ Graz; Translimina; Univ Oxford; Univ Reading
Uncontrolled keywords: specification; refinement; Z; non-atomic refinement; non-atomic operations
Subjects: Q Science
Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Science Technology and Medical Studies > School of Computing
Depositing User: M. Nasiriavanaki
Date Deposited: 14 Jun 2009 19:40
Last Modified: 13 May 2014 08:34
Resource URI: (The current URI for this page, for reference purposes)
  • Depositors only (login required):