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 | |
| Additional URLs: |
|
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, |
| Institutional Unit: | Schools > School of Computing |
| Former Institutional Unit: |
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: | 20 May 2025 10:09 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: |
- Link to SensusAccess
- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV
- Depositors only (login required):
Total Views
Total Views
