David Duke & Graeme Smith

Specification with class: A brief history of Object-Z

Dramatis personae

To simplify the narrative, we use initials to refer to key players and organisations.

• AG Alena Griffiths
• DC David Carrington
• DD David Duke
• GR Gordon Rose
• GS Graeme Smith
• JSD Jin Song Dong
• OTC Overseas Telecommunications Commission, Australia
• PK Paul King
• RD Roger Duke
• UQ University of Queensland, Australia

The end of the 1980's saw a growing interest in object orientation as both a design and programming methodology with the advent of programming languages like C++ and Eiffel. The trend was taken up by some in the formal methods community, including a team of researchers in Australia. Their contribution was a formal specification language, Object-Z, which had immediate industrial impact, gained rapid international recognition, and then two decades later began to fade, along with some of its contemporaries, from the formal methods scene.

The seed from which Object-Z grew was a comment from a software engineer in industry: why couldn't a Z specification (that UQ was developing for OTC) be structured to make it easier to read; in particular, why couldn't it be structured like C++? This was in 1988. The engineer was working for OTC developing the specified system in C++. The recipient of the comment was GR, who a few days later called together RD and GS and showed them his idea for what became an Object-Z class. Over the next year, GR, RD and GS were joined by DC, DD and PK in defining the first version of Object-Z. GS rewrote the specification of the OTC system and, along with RD, attempted to verify (by hand) its critical properties. Doing this, they discovered two errors in the design. OTC was deeply impressed. Object-Z was a success and funding for it continued until OTC was merged with Telecom Australia in 1992.

By that time, DD and GS had completed PhDs on Object-Z. DD's thesis provided a denotational semantics based on `histories' which formed the basis of future work on the integration of Object-Z with other formalisms such as CSP. These PhDs were followed, throughout the 1990's, by several others on applications and further developments of Object-Z. Perhaps the most controversial development was to give Object-Z a reference semantics. GR and RD argued this would make it easier to translate Object-Z to programming languages like C++. GS argued that it would unnecessarily complicate reasoning. However, the decision was made and a new PhD student, AG, was given the task of defining the reference semantics. Another PhD student, JSD, added a number of features based on this semantics including self and mutually recursive classes.

By the mid-1990's, Object-Z was appearing in publications from outside of UQ. The number of such publications grew over the next decade and a half: on a webpage that GS maintained until 2004 there were 59 such publications. Since then interest has noticeably waned. It is interesting to reflect on why this is the case and, in particular, to compare Object-Z's fate with that of other specification languages of the time.