Towards a Formal Semantics for the Z Notation

Abstract

The Z notation [Sufrin 84, Morgan 84] is a language for expressing formal specifications of computing systems. It is based on a typed set theory, and the notion of a "schema"' is one of its central features. A schema consists of a collection of named objects specified by some axioms, and Z provides a system of notation for combining schemas which conveniently allows large specifications to be built up in stages.