Bibliographical Notes

The embedding of Z ADTs in the relational setting and the embedding of inputs and outputs as used here were first described by Woodcock and Davies [209]. The description in this chapter presents much more of the detail, and adds the behavioural interpretation, which has also been described by Bolton, Davies and Woodcock [25].

A more general Z ADT, which mentions the global state explicitly, is described by Stepney, Cooper and Woodcock [193,208]. We will discuss this approach further in Chapter 10, as it is closely related to the generalisations introduced there.