Z: GRAMMAR AND CONCRETE AND ABSTRACT SYNTAXES (Version 2.0)

Abstract

In this monograph we give a comprehensive description of the syntax for the specification language Z. The language has already been described informally in [Sufrin 86] and in [Haye, 87]. The aim of this document is to prepare for the standardisation of the syntax of Z. The abstract syntax of Z is defined and a concrete representation of all language constructs is given. The paper suggests a terminology for the constructs and the concepts of the Z language. The syntax describes a language which is as close as possible to that which is used in existing case studies. However, some syntactic variants of constructs in the language which have been used in the past have been omitted. The paper gives an informal introduction to the scope rules for identifiers, the type rules for terms and the precedence rules for operators, functions and relation symbols. This description is informal, and the description of the type rules is concise and complex, and may be passed over if the reader desires.