SPECIFYING SYSTEM IMPLEMENTATIONS IN Z

Abstract

In an introductory chapter, an outline is presented of some techniques for specifying the building of systems from subsystems using the formal notation Z. These techniques have been applied to the specification of implementations for services in a distributed system. The major part of the monograph consists of an extended example showing bow the implementation of a simple file server can he specified using some of the outlined techniques. The example file service is implemented in terms of a lower-level storage service. The specification includes the handling of errors that may arise because of this dependency.