What is Object-Z?

Object-Z is an extension of the formal specification language Z to facilitate specification in an object-oriented style. It is a conservative extension in the sense that the existing syntax and semantics of Z are retained in Object-Z. It has been developed by a team of researchers at the Software Verification Research Centre, University of Queensland, Australia. 

What books are available on Object-Z? 

Currently there are two books available on Object-Z:

• 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. 

There is also a book on refinement in Object-Z.

• John Derrick and Eerke Boiten. Refinement in Z and Object-Z, Foundations and Advanced Applications. Springer-Verlag, 2001.

What tools are available for Object-Z?

LaTeX style files are available for typesetting Object-Z specifications.

Wizard is a type-checker for Object-Z specifications written in LaTeX.

Moby/OZ is a graphical editor for Object-Z specifications. 

 ZML is an XML/XSL web browsing tool for Z, Object-Z and TCOZ.

For ongoing work on tool support see the publications page.  

Why is there more than one version/semantics of Object-Z?

Prior to 1993, Object-Z was developed with a value semantics where a variable whose type is a class is the value of an object of that class. Since 1993, a reference semantics has been adopted where a variable whose type is a class is a reference to an object of that class. The adoption of the reference semantics facilitates the refinement of specification to code in object-oriented programming languages (which also have reference semantics). It also allows specifications in which self and mutual recursion are possible. 

What happened to history predicates?

Temporal logic history predicates were used to capture liveness properties in early papers on Object-Z. They are not, however, included in the recent semantics of Object-Z and are not supported by the Wizard type checker. This omission does not preclude the future use of history predicates in Object-Z. It simply reflects the instability of their syntactic and semantic definition at present. 

How is object creation and destruction modelled in Object-Z?

Object creation and destruction are not explicitly supported in Object-Z. However, the creation of an object can be modelled by introducing its identity (or reference) into a specification in which this identity is not currently available (e.g. adding the identity to a specified set of object identities). Similarly, object destruction can be modelled by removing the identity of an object from a specification (e.g. removing the identity from a specified set).

Can an operation be used as a predicate?

Operations cannot be used as predicates as schemas are in Z. They are not the same as schemas since they include, as well as declarations and predicates, a delta-list listing those variables which the operation may change. An operation's predicate can be included in another operation, however, using the operation conjunction operator. 

Are there other object-oriented extensions of Z? 

There have been a number of object-oriented extensions of Z proposed as well as methods for using standard Z in an object-oriented fashion. A good summary is provided by the following books.

• K. Lano and H. Haughton, editors. Object Oriented Specification Case Studies. Prentice Hall, 1994. 
• S. Stepney, R. Barden and D. Cooper, editors. Object Orientation in Z. Springer-Verlag, 1992.