Boiten, E.A. and Derrick, J. (1998) IO - refinement in Z. In: Evans, A. and Duke, D. and Clark, T., eds. 3rd Northern Formal MethodsWorkshop, 1998. Electronic Workshops in Computing. Springer Verlag ISBN 1-902505-14-X.
|
Download (191Kb)
|
![[img]](http://kar.kent.ac.uk/style/images/fileicons/application_pdf.png)
|
|
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: | Faculties > Science Technology and Medical Studies > School of Computing > Theoretical Computing Group Faculties > Science Technology and Medical Studies > School of Computing > Systems Architecture Group |
| Depositing User: | Mark Wheadon |
| Date Deposited: | 25 Aug 2009 15:46 |
| Last Modified: | 06 Sep 2011 03:59 |
| Resource URI: | http://kar.kent.ac.uk/id/eprint/21600 (The current URI for this page, for reference purposes) |
- Depositors only (login required):
