Abstract :
In the specification notation known as Z, schemas are used to structure mathematical descriptions. The article describes the language of schemas and the conventions that are employed in their use. It also describes how proof obligations are generated during specification, and how these obligations may be discharged. Many examples, mostly taken from the specification of the user interface to a small, but realistic, software component are also included
