IO-refinement in Z

We present a generalisation of data refinement in Z, called IO-refinement , that allows changes in input and output parameters of operations. Several informal motivations for the desirability of such a refinement relation are given, followed by a formal derivation that demonstrates its theoretical soundness. It is proved that IO-refinement indeed generalizes data refinement. Several theorems are presented that give sufficient conditions for IO-refinement to hold in simpler situations, e.g. just adding inputs and outputs. Some examples of the use of IO-refinement are also given.

Content

Author and article information

Conference

Publication date: September 1998

Publication date (Print): September 1998

Pages: 1-18

Affiliations

[0001]Computing Laboratory, University of Kent

Canterbury, Kent, U.K.

Article

DOI: 10.14236/ewic/NFM1998.3

SO-VID: 2fe94927-ca68-42e8-b95c-ee0cecfd1d0c

License:

This work is licensed under a Creative Commons Attribution 4.0 Unported License. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/

Conference name: 3rd BCS-FACS Northern Formal Methods Workshop

Conference acronym: NFM

Conference number: 3

Conference location: Ilkley, UK

Conference date: 14-15 September 1998

Conference sponsor: Electronic Workshops in Computing (eWiC)

Conference theme: BCS-FACS Northern Formal Methods Workshop

History

Product

1477-9358 BCS Learning & Development

Self URI (article page): https://www.scienceopen.com/hosted-document?doi=10.14236/ewic/NFM1998.3

Self URI (journal page): https://ewic.bcs.org/

Celebrating 65 years of The Computer Journal - free-to-read perspectives - bcs.org/tcj65

IO-refinement in Z

Abstract