Z (pronounced *zed*) is a set of conventions for presenting
mathematical text, chosen to make it convenient to use simple
mathematics to describe computing systems. I say computing
*systems* because Z has been used to model hardware as well as
software.

Z is a *model-based notation*. In Z you usually model a system by
representing its *state* -- a collection of *state variables*
and their values -- and some *operations* that can change its state. A
model that is characterized by the operations it describes is called an *
abstract data type* (ADT). This modelling style is a good match to
imperative, procedural programming languages that provide a rich collection
of data types, and also to some physical systems (such as digital
electronics) that include storage elements. Z is also a natural fit to
object-oriented programming. Z state variables are like instance variables
and the operations are like methods; Z even provides a kind of inheritance.
However, Z is not limited just to ADT's and object-oriented style; you can
also use Z in a functional style, among others.

Z dictates few assumptions about what can be modelled. Z is just a notation, it is not a method; the Z notation can support many different methods. The meaning of a Z text is determined by its authors. It can be understood to model only the behavior of a system: it is an abstract formal specification. Or, the elements of a Z text can be understood to represent structures in code: modules, data types, procedures, functions, classes, objects. In that case the Z model is a detailed design.

Z is not an executable notation. In general, Z specifications cannot be
interpreted or compiled into a running program (or prototype or
simulation). *Z is not a programming language.* Z texts are not just
programs written in very high-level language. What would be the point of
writing the program twice?

Z was designed for people, not machines. For years Z was exclusively a pencil-and-paper notation. Z encourages a style where formulas are annotated liberally with prose. Z documents usually include more prose than formal text. Novices can be intimidated by the appearance of Z: a mixture of boxes, text, Greek letters, and invented pictorial symbols. But the notation is easy to learn; once assimilated, its advantages become clear. The boxes and pictorial symbols in Z help your eye grasp the structure of the model even before you read it.

Z actually includes two notations. The first is the notation of
ordinary discrete mathematics. The second notation provides
structure to the mathematical text: it provides several
structuring constructs called *paragraphs*. The most conspicuous
kind of Z paragraph is a macro-like abbreviation and naming construct
called the *schema*. Z defines a *schema calculus* you can
use to build big schemas from small ones. The schema is the
feature that most distinguishes Z from other formal notations.

The mathematical notation of Z consists of a small core, supplemented
by a larger collection of useful objects and operators called the *
Z mathematical tool-kit*. The tool-kit is not software, it is a
collection of mathematical theories: definitions and laws concerning
objects such as sets, tuples, relations, functions, sequences and
their operators. In Z we use these mathematical objects to model data
structures and other components of computing systems. The tool-kit
plays somewhat the same role in Z that a standard library of types and
functions does in an executable programming language.

Z is supported by tools. The notation is defined with sufficient precision that Z texts can be processed by machine. Software tools are available for writing and displaying the special Z symbols and typesetting documents, for checking Z texts for syntax and type errors in much the same way that a compiler checks code in an executable programming language, and even for assisting in proving claims about the behavior of systems modelled in Z. These tools are invaluable for serious work, but you do not need them to begin learning and using Z.

Z is a mature notation. Conceived in the late 1970's, it developed through the 1980's in collaborative projects between Oxford University and industrial partners including IBM and Inmos (a semiconductor producer). The first Z reference manual to be widely published benefited from this long experience when it finally appeared in 1989. An international Z standard was completed in 2002. Z has served as the basis for other notations, including several variants adapted for object-oriented programming.

From chapter 4 in The Way of Z

Links to some Z examples

Other pages about Z and formal methods

Jonathan Jacky