© University of Kent - Contact | Feedback | Legal
The University of Kent, Canterbury, Kent, CT2 7NZ, T +44 (0)1227 764000
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 144-166. Springer, July 2000.Abstract
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
@conference{1023,
author = {E.A. Boiten and J. Derrick},
title = {Liberating data refinement},
month = {July},
year = {2000},
pages = {144-166},
keywords = {Refinement, formal methods, Z},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2000/1023},
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},
}