THE FORMAL DOCUMENTATION OF A BLOCK STORAGE SERVICE

Abstract

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 Implementer 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 specifications of the behaviour of the service, written in the formal specification language Z.