The Development of Z

 Brien, S. (1994). The Development of Z. In: Andrews, D.J., Groote, J.F., Middelburg, C.A. (eds) Semantics of Specification Languages (SoSL). Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3229-5_1

 

Z is a model-oriented specification language, which originated in the early 1980s. The first description by Abrial included a structuring mechanism called a class, which was very similar to a schema (i.e. a combination of a declaration and a constraining predicate). The Z style has developed as a result of tackling practical examples and adapting the notation to their needs; this has resulted in a style and notation that is widely applicable to the description of certain kinds of computer system, particularly the client-server model.

With the publication of Sufrin’s Z Handbook the development and understanding of Z had progressed. A type inference system and rules for reasoning were provided and the notions of schemas and generic types had evolved into their now familiar form. The first formal semantics was given by Spivey using a variety-based denotational semantics where the metalanguage used was Z itself, and included a brief sketch of a possible proof theory.

The standardisation process for Z provided a powerful motivation to attempt this exercise again. The standard semantics uses a relational approach, and attempts a loose definition of the meaning of undefined elements so as to accommodate some of the different possible treatments while ensuring that the logic is two-valued. This paper traces the evolution of the semantics of Z from the early efforts to the definition in the Z standard, comparing the various approaches to defining the model, presenting the semantics and dealing with undefinedness.

 

1 The Early Days
The origins of the development of Z can be traced back to the Software Engi-
neering Project at the Programming Research Group in Oxford. This project
started in 1978 with both Tony Hoare and Bernard Sufrin associated with it
from the beginning. It was the first of many projects which supported re-
searchers engaged in work on specification. At around the same time Jean-
Raymond Abrial was giving lectures on specification at Queen's University
Belfast. The language was based on three principles: a strict formalism, recog-
nition of set theory as a sound basis, and the necessity of a strong structur-
ing mechanism. These course notes were published with Steve Schumann and
Bertrand Meyer in a paper simply called "Specification Language" [4].
D. J. Andrews et al. (eds.), Semantics of Specification Languages (SoSL)
© British Computer Society 1994
2
In late 1979 Abrial moved to Oxford. He presented a seminar course to re-
search staff and students on his specification language. This language included
schema-like objects called classes which were a combination of declarations and
a constraining predicates:

class (1)
a :Xj
b: Y
where
p
end

Notably, there were no semantics for this language. Rod Burstall observed at
the time that the language had a strong flavour of "Bourbaki" . .
In 1980 Abrial produced two papers on Z [1, 2] a Basic Library and a Syntax
and "Semantics". The basic library was a series of chapters of Z specifications
of sets, functions, relations and other mathematical structures. This was an
early forerunner of the mathematical toolkit which was published in Spivey's
Reference Manual [42]. The syntax and semantics paper included an outline
proof system for the mathematical sublanguage, which lay somewhat neglected
for many years.
Soon afterwards Abrial, Sorensen and Clement started a project suggested
by Bernie Cohen, then of STL, to formally specify and implement CAVIAR
(Computer Aided Visitor Information and Reception) System [14].
During this project the notation underwent a redesign and the notion of
a class conjunction was introduced. The notation that resulted from this re-
working was essentially the same as the current mathematical language of Z,
however the concrete notation used keywords. For example, the definition of
set union was as follows:

op(U) = In Sl, S2 -+ S3 then (2)
S3 = set X whereX E SI or X E S2 end end;

The style reverted to a more familiar notation "under the impact" of Dana
Scott's verdict that it was too verbose. Although there was some form of generic
definition, there was no formal type system and only an informal semantics.
Impetus for the further development of schemas came from the realisation
that the standard mathematical forms of extending states and promoting op-
erations on them were too unwieldy for use in the specification of large scale
systems. Experience in VDM[26, 25], influenced by the presence of in the PRG
of Cliff Jones, suggested that what was needed was a formalism in which ex-
tension and promotion were simply expressible, and for which proof rules could
be given directly.
These efforts produced the nucleus of what later became known as the
schema calculus. Generated mostly from problems encountered in defining [...]