A Z Specification of Use Cases

We seek to clarify the notion of use case and the related terminology by means of a specification written in Z. 1 Introduction The use case concept is a tool for capturing the requirements of a system. A single use case describes a subset of a system's functionality in terms of the interactions between the system and a set of users or actors. A use case is initiated by a particular user, and serves the purpose of delivering some meaningful unit of work, service, or value to the initiator. When capturing requirements, a use case views the system as a black box. Use cases have assumed a prominent role in methodologies for object-oriented software development for the capturing of user requirements, and for traceability of software artefacts from across the entire software lifecycle to the user requirements. Due to their popularity, the concept of use cases has been abused to some extent, and been applied to specifying the "requirements" of all sorts of things, such as those of a subsyste..