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. 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.