Non-atomic refinement in Z

Derrick, John and Boiten, Eerke Albert (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. (doi: (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 currently available from this repository. You may be able to access a copy if URLs are provided. (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 > Sciences > School of Computing
Depositing User: E.A. Boiten
Date Deposited: 14 Jun 2009 19:40 UTC
Last Modified: 20 Oct 2015 14:25 UTC
Resource URI: (The current URI for this page, for reference purposes)
Boiten, Eerke Albert:
  • Depositors only (login required):