Bibliographical Notes

We first presented these ideas for allowing implicit observations and modifications at the 1998 International Refinement Workshop [20], as the very last talk of the workshop. Before that, many of the other presentations had touched on issues of framing and displays. Groves [103] dealt with the framing problem for modification by providing explicit frames, based on an approach by Mahoney. Woodcock illustrated his paper [208] with a web browser example whose outputs were changing constantly. De Groot and Robinson needed snapshots (``probe points") of the ADT state for the refinement analogue of error tracing [58].

An extensive discussion of the framing problem in a Z context may be found in a paper by Daniel Jackson [125].

Approaches to modelling human-computer interaction using formal methods are closely related to our treatment of displays and observations. In particular, work by Duke and Harrison [74,75] and Sufrin and He [198] discusses notions of observation and refinement.

``Normal variables" in the treatment by de Roever and Engelhardt [60] play a similar rôle to modifiable components in grey boxes. By constraining simulation relations to those which are unaffected by normal variables, they minimise the adverse effects that could be caused by operations on normal variables. From the observation that Z inputs and outputs would also be modelled by normal variables in their approach, it seems we could make the link between IO and observations/modifications in Z more direct as well.