The Object-Z Specification Language

Object-Z is an object-oriented extension of the formal specification language Z. It was developed by a team of researchers at the Software Verification Research Centre, The University of Queensland. There are numerous publications on Object-Z including 2 books on the language:

• Graeme Smith. The Object-Z Specification Language. Kluwer Academic Publishers, 2000.

This book provides a comprehensive description of the language including semantics issues, type rules, informal and semi-formal descriptions of all language constructs, specification guidelines and a full formal syntax.

• Roger Duke and Gordon Rose. Formal Object-Oriented Specification Using Object-Z. MacMillan, 2000.

This book illustrates (through numerous and varied case studies) various stylistic and architectural approaches, the integration of graphical techniques with Object-Z specifications, and includes the syntax of Object-Z, a glossary of its symbolism and selected examples of its semantics.

and one on its theory of refinement:

• John Derrick and Eerke Boiten. Refinement in Z and Object-Z, Foundations and Advanced Applications, 2nd edition. Springer-Verlag, 2014.
• 
  

Latex macros for typesetting Object-Z specifications are available here.