School of Computing

IO - refinement in Z

E.A. Boiten and J. Derrick

In A Evans, D Duke, and T Clark, editors, 3rd BCS-FACS Northern Formal Methods Workshop, Electronic Workshops in Computing, pages 182-196. Springer Verlag, September 1998.

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.

 

Paper on BCS website; see also chapter 10 in Refinement in Z and Object-Z.



Bibtex Record

@conference{608,
author = {E.A. Boiten and J. Derrick},
title = {{IO} - refinement in {Z}},
month = {September},
year = {1998},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1998/608},
    booktitle = {3rd BCS-FACS Northern Formal Methods Workshop},
    editor = {A Evans and D Duke and T Clark},
    isbn = {1-902505-14-X},
    note = {http://www.ewic.org.uk/},
    publisher = {Springer Verlag},
    refereed = {yes},
    series = {Electronic Workshops in Computing},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014