Formal Methods Wiki

Virtual Library
Software engineering
Formal methods
Z notation

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 two books on the language:

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.

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:

Tool support for Object-Z is available from the CZT initiative.

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

An older version of this page (not updated since 2004) can be found here.