School of Computing

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.


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 kbytes

Bibtex Record

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 = {},
    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},

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

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

Last Updated: 21/03/2014