Programming Research Group Technical Monograph PRG-62

Roger Gimson

August 1987, 112 pages, ISBN 0-902928-44-9

The formal documentation for a low-level data storage service is presented. The service allows blocks of data to be stored on behalf of clients in a distributed system. The documentation includes both a User Manual, presenting the clients' view of the service, and an Implementor Manual, describing how the service may be implemented. It is called formal documentation because, as well as informal text giving the conventional overviews to the casual reader, it includes precise specfications of the behaviour of the service, written in the formal specification language Z.

Though applied here to the example of a block storage service, the illustrated style of documentation can equally well be applied to describing any such system components. This style has been developed as a part of a project on designing and specifying components of a distributed operating system. The monograph includes a discussion of the design choices considered for the service, and the experience gained through its design, implementation and documentation.