Z is a language for describing patterns of declaration and constraint; it can be used to produce structured, mathematical descriptions. It was developed through application to the specification and design of large, complex software systems. It is well-suited to the description of system or component state, and of transactions upon that state.
This book introduces the mathematical language of Z: logic, sets, relations, and schemas. It introduces also a theory of refinement: a set of rules that can be used to prove that two different designs are consistent in terms of their externally-observable, transactional behaviour.
To obtain an electronic version, click here .