Computing
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:
- Graeme Smith. The Object-Z Specification Language. Kluwer Academic Publishers, 2000. ISBN 978-0-7923-8684-1.
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. ISBN 0333801237.
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. Springer-Verlag, 2001. ISBN 978-1-85233-245-7.
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.
Sources[]
- Based on The Object-Z Home Page in the Virtual Library↑.