© University of Kent - Contact | Feedback | Legal | FOI | Cookies
Grey box data refinement
E.A. Boiten and J. Derrick
In J. Grundy, M. Schwenke, and T. Vickers, editors, International Refinement Workshop & Formal Methods Pacific '98, Discrete Mathematics and Theoretical Computer Science, pages 182-196, Canberra, September 1998. Springer-Verlag.Abstract
We introduce the concepts of grey box and display box data types. These make explicit the idea that state variables in abstract data types are not always hidden. Programming languages have visibility rules which make representations observable and modifiable. Specifications in model-based notations may have implicit assumptions about visible state components, or are used in contexts where the representation does matter. Grey box data types are like the ``standard'' black box data types, except that they contain explicit subspaces of the state which are modifiable and observable. Display boxes indirectly observe the state by adding displays to a black box. Refinement rules for both these alternative data types are given, based on their interpretations as black boxes. Download publication 72 kbytesBibtex Record
@inproceedings{613,
author = {E.A. Boiten and J. Derrick},
title = {Grey Box Data Refinement},
month = {September},
year = {1998},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1998/613},
ISBN = {981-4021-16-4},
address = {Canberra},
booktitle = {International Refinement Workshop & Formal Methods Pacific '98},
editor = {J. Grundy and M. Schwenke and T. Vickers},
publisher = {Springer-Verlag},
refereed = {yes},
series = {Discrete Mathematics and Theoretical Computer Science},
}