Skip to main content

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 World Congress on Formal Methods in the Development of Computing Systems. Lecture Notes In Computer Science, 2 . Springer-Verlag Berlin, Berlin, Germany, pp. 1477-1496. ISBN 978-3-540-66588-5. E-ISBN 978-3-540-48118-8. (doi:10.1007/3-540-48118-4_28) (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) (KAR id:17280)

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.
Official URL:
http://dx.doi.org/10.1007/3-540-48118-4_28

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.

Item Type: Book section
DOI/Identification number: 10.1007/3-540-48118-4_28
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: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Eerke Boiten
Date Deposited: 14 Jun 2009 19:40 UTC
Last Modified: 16 Nov 2021 09:55 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/17280 (The current URI for this page, for reference purposes)

University of Kent Author Information

Derrick, John.

Creator's ORCID:
CReDIT Contributor Roles:

Boiten, Eerke Albert.

Creator's ORCID: https://orcid.org/0000-0002-9184-8968
CReDIT Contributor Roles:
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.