Boiten, E.A. and Derrick, J. (1998) Grey Box Data Refinement. In: International Refinement Workshop & Formal Methods Pacific '98, 1998; Sep, Canberra, Australia.
|
Download (221Kb)
|
![[img]](http://kar.kent.ac.uk/style/images/fileicons/application_pdf.png)
|
|
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.
| 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: | Mark Wheadon |
| Date Deposited: | 25 Aug 2009 15:36 |
| Last Modified: | 06 Sep 2011 04:00 |
| Resource URI: | http://kar.kent.ac.uk/id/eprint/21607 (The current URI for this page, for reference purposes) |
- Depositors only (login required):
