A case study in partial specification: consistency and refinement for Object-Z

The `viewpoint´ approach, in which a system is described by several partial specifications, has been proposed as a way of making complex computing systems more understandable. The ISO´s Open Distributing Processing (ODP) framework is an architecture for open distributed systems, involving five named viewpoints. This paper compares two partial specifications of a lending library-from the ODP´s Enterprise and Information Viewpoints-and discusses the relation between them. Both specifications are written in Object-Z, an object-oriented variant of Z. Examining how such partial specifications might be unified raises broader issues of refinement and mutual consistency of partial specifications in Object-Z