School of Computing

Liberating data refinement

E.A. Boiten and J. Derrick

In R.C. Backhouse and J.N. Oliveira, editors, Mathematics of Program Construction, 5th International Conference, Ponte de Lima, volume 1837 of Lecture Notes in Computer Science, pages 182-196. Springer, July 2000.


Traditional rules for refinement of abstract data types suggest a software development process in which much of the detail has to be present already in the initial specification. In particular, the set of available operations and their interfaces need to be fixed. In contrast, many formal and informal software development methods rely on changes of granularity and require introduction of detail in a gradual way during the development process.

This paper discusses several generalisations and extensions of the traditional refinement rules, which are compatible with each other and, more importantly, with the semantic grounding of data refinement. Together they should provide a semantic justification to a larger spectrum of development steps.

The discussion takes place in the context of the formal specification language Z and its relational underpinnings.

Bibtex Record

author = {E.A. Boiten and J. Derrick},
title = {Liberating data refinement},
month = {July},
year = {2000},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {},
    booktitle = {Mathematics of Program Construction, 5th International Conference, Ponte de Lima},
    editor = {R.C. Backhouse and J.N. Oliveira},
    publication_type = {conference},
    publisher = {Springer},
    refereed = {yes},
    series = {Lecture Notes in Computer Science},
    submission_id = {10948_954496997},
    volume = {1837},
    ISBN = {3-540-67727-5},

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

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

Last Updated: 21/03/2014