Grey Box Data Refinement

Boiten, Eerke Albert and Derrick, John (1998) Grey Box Data Refinement. In: International Refinement Workshop & Formal Methods Pacific '98, 1998; Sep, Canberra, Australia. (Full text available)

Download (226kB)


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.

Item Type: Conference or workshop item (Paper)
Additional information: Held as a joint conference. Also known as IRW/FMP '98. Also incorporates the 7th Australasian refinement workshop and the 4th New Zealand formal program development colloquium
Uncontrolled keywords: data refinement, observability, abstract data type, black box, visibility
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Science Technology and Medical Studies > School of Computing > Theoretical Computing Group
Faculties > Science Technology and Medical Studies > School of Computing > Systems Architecture Group
Depositing User: Eerke Boiten
Date Deposited: 25 Aug 2009 15:36
Last Modified: 20 Oct 2015 14:25
Resource URI: (The current URI for this page, for reference purposes)
ORCiD (Boiten, Eerke Albert):
  • Depositors only (login required):


Downloads per month over past year