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. 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 subsystem of the system architecture. In this paper we seek to answer that question, by providing a specification of a use case and its related concepts using the Z formalism.