×

Understanding Z. A specification language and its formal semantics. (English) Zbl 0658.68005

Cambridge Tracts in Theoretical Computer Science, 3. Cambridge etc.: Cambridge University Press. VIII, 131 p. $ 27.95; £17.50 (1988).
This book is a monograph on the denotational semantics of a specification language designed to understand the mathematics and meaning of the well known language Z.
The book first introduces into the language Z by discussing a simple data base example and then discusses general questions: The importance of formal semantics, the concept of meta-circularity (giving semantics to a language in that language), and other approaches to formal specification (namely VDM and CLEAR).
It next introduces basic concepts like axiomatic set theory and its relation to Z-notations, types, structures, schemata and notation from denotational semantics.
Chapter 3 then is the core of the book and gives a summary of the specification language and defines its denotational semantics using the specification language itself.
The next chapter discusses left over questions like generic definitions, referential transparency, and topics of partiality. Also a short discussion of CLEAR-semantics is added. The final chapter is concerned with studies in Z-style. The book is concluded with references, a summary of notation and an index of definitions.
The reader finds a well written book on a special rather technical topic which tries to discuss its questions in a little wider scope. As such it is valuable for those who seek to understand the language Z in more detail or who are interested in denotational semantics of set-based specification languages. A larger audience, I am afraid, will have a reference to Z but not really a help in utilizing mathematical notation for the specification of larger systems. In this context I found the discussion of CLEAR a little bit superficial and also not very knowledgeable. The goal of the book, to support a standardization of Z, however, will certainly be achieved by the author.
Reviewer: B.Mahr

MSC:

68-02 Research exposition (monographs, survey articles) pertaining to computer science
68Q55 Semantics in the theory of computing
03E30 Axiomatics of classical set theory and its fragments
68Q60 Specification and verification (program logics, model checking, etc.)
03E99 Set theory
PDFBibTeX XMLCite