Skip to main content

IO - refinement in Z

Boiten, Eerke Albert, Derrick, John (1998) IO - refinement in Z. In: 3rd Northern Formal MethodsWorkshop,, 1998. (KAR id:21600)

Language: English
Click to download this file (215kB) Preview
[thumbnail of IO_-_refinement_in_Z.pdf]
This file may not be suitable for users of assistive technology.
Request an accessible format


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. on BCS website; see also chapter 10 in /pubs/2001/1200/.

Item Type: Conference or workshop item (Paper)
Additional information:
Uncontrolled keywords: data refinement, Z, interface refinement, input/output
Subjects: 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: 25 Aug 2009 15:46 UTC
Last Modified: 16 Nov 2021 09:59 UTC
Resource URI: (The current URI for this page, for reference purposes)
Boiten, Eerke Albert:
  • Depositors only (login required):

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