IO - refinement in Z

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

PDF Language: English
Download this file (PDF/215kB)	Preview
Request a format suitable for use with assistive technology e.g. a screenreader

Abstract

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. http://www1.bcs.org.uk/DocsRepository/02700/2702/boiten.pdf on BCS website; see also chapter 10 in /pubs/2001/1200/.

Item Type:	Conference or workshop item (Paper)
Additional information:	http://www.ewic.org.uk/
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:	05 Nov 2024 09:59 UTC
Resource URI:	https://kar.kent.ac.uk/id/eprint/21600 (The current URI for this page, for reference purposes)

University of Kent Author Information

Boiten, Eerke Albert.

Creator's ORCID:	https://orcid.org/0000-0002-9184-8968
CReDIT Contributor Roles:

Derrick, John.

Creator's ORCID:
CReDIT Contributor Roles:

Depositors only (login required):

Total Views

Total unique views of this page since July 2020. For more details click on the image.