Notation Z

The Z notation is a specification language used to describe and model the computer systems.


The Z rating was created by Jean-Raymond Abrial . Z appeared for the first time in a book, during the 1980 edition of Meyer et Baudouin ‘s book , Méthodes de programmation, Eyrolles. There were only notes from Jean-Raymond Abrial, internal EDF. They followed the article published in 1974, entitled Data Semantics in Data Base Management (Kimbie, Koffeman, eds, North-Holland, 1974, pp. 1-59 ).

In 1983, Delobel and Adiba used the original Z notation in their book “Databases and Relational Systems” (Dunod). Under the name of “binary relational model,” it is used to introduce Ted Codd’s “n-aire relational model.” A graphical notation uses this binary relational model, NIAM (Nijssen Information Analysis Method), (H. Habrias, The binary relational model, Eyrolles, 1988) developed within Control Data in Brussels.

Abrial brought Z to the Oxford Programming Group in September 1987. He abandoned Z to propose Method B in the 1980s. The first international standard (ISO) on Z was published in July 2002.

Z in a few words

  • A Z specification is a predicate. The specification of the invariant and the specification of the operations have the form of a predicate.
  • The specification is structured into diagrams.
  • Z uses the naive theory of sets and the logic of first order predicates .

Z by the example

Is used, when possible, the ASCII notation B. can be found correspondence with the notation B Method B .

The basic sets


STUDENT and GROUP are basic types (E-SETS)

A schema

Here is what in Z we call schemas:

 promo: POW (STUDENT) 
 aForGroup: STUDENT + → GROUP 
 promo = dom (aForGroup) 

A schema has a name, here MaPetiteEcole, two parts:

  • The top one is called the “typing” part.The variables and their type are declared.
    • Here, promo belongs to all the parts (also called, set of subsets) of STUDENT.

Recall that POW ({1, 2}) = {{}, {1}, {2}, {1,2}}

    • STUDENT + → GROUP is the set of partial functions of STUDENT to GROUP. What is paraphrased: a student is a member of at most one group.
    • When one passes from one line to another, implicitly one writes a conjunction.
  • That of the bottom is called the “predicative” part (note that the upper part is also made up of predicates! … of typing)
    • Here, we have a parity predicate of equality: all the students of the promo are equal to the domain of the function aForGroup, which in common French gives: “all student of the promotion is member of a group” .

An Operation Scheme

 Δ MaPetiteEcole 
 nouvEtud? : STUDENT 
 gpe? : GROUP
 NouvEtud? /: Promo 
 promo '= promo \ / {nouvEtud?} 
 AForGroup' = aForGroup \ / {newEnd? | → gpe?} 

Δ declares: promo, promo ‘, aForGroup, aForGroup’. The premium expresses the state after the operation.

Warning !

You read correctly. Above, we wrote = (predicate of equality) and not: = (substitution). A schema is a predicate. The line break expresses a conjunction (& And;).
The registration scheme gives the predicate that must be respected by the registration operation.

An interrogation operation

 Χ MaPetiteEcole etud 
 Etud? : 
 Promotion grpe! : AForGroup (etude?)

Χ declares: promo, promo, aPourGroupe, aPourGroupe’and the constraints:
promo = promo ‘
aPourGroupe’ = aPourGroupe

This means that you do not want the query operation to change the state of the data.

A scheme will make it possible to specify an initial state, which, as in B, serves to ensure that one can have a state satisfying the constraints.

Initialization scheme

 promo = {} 
 aForGroup = {}

A free type

REPORT :: = ok | AlreadyContacts | Unknown

REPORT is a free type.

Schemes with free type

 ____ Success ______________________________ 
 result! : REPORT
 result! = Ok
 ____Already known___________________________
 KHI MaPetiteEcole etud 
 Etud? : Promo 
 result! = AlreadyConnected

Using the schema calculus

We will have a robust specification

 RInscription == (Registration & Success) or DéjàConnu

There are other operators than the & and the gold for the calculation of schemes.


We have presented closed diagrams. The statements are local to these schemas.

Open Schemes

There are open schemes (axiomatic description) that introduce one or more global variables and possibly specify constraints on their values.


 Square: NAT → NAT
 ! N: NAT • square (n) = n * n

The notation Z for the description of sets in comprehension

{… | … • …}

There are three parts (declaration | Constraint • expression}

For example:

 {X: NAT | Even (x) • x * x} is the set of squares of even numbers.

Schemas as Types

One can take a schema as a type.

A schema is then seen as the set of states that respect the scheme. A variable of type schema can then take as value one of these states which respect the schema indicated like type of the variable.



 ===== [X, Y] ================= 
 first: X * Y → X 
 ! X: X; Y: Y • first (x, y) = x


In French, three books on Z.

  • David Lightfoot, Formal specification with Z, Teknea, ( ISBN  2-87717-038-1 ) translated by Henri Habrias and Pierre-Marie Delpech (a short introductory book)
  • JM Spivey, The Z score, Masson, Prentice-Hall, ( ISBN  2-225-84367-8 ) translated by M. Lemoine (more complete)
  • Pascal André and Alain Vailly, Corrected software design exercises: modeling of information systems by practice, ( ISBN  272981289X ) .