The Z notation is a specification language used to describe and model the computer systems.
History
The Z rating was created by JeanRaymond 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 JeanRaymond Abrial, internal EDF. They followed the article published in 1974, entitled Data Semantics in Data Base Management (Kimbie, Koffeman, eds, NorthHolland, 1974, pp. 159 ).
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 “naire 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, GROUP]
STUDENT and GROUP are basic types (ESETS)
A schema
Here is what in Z we call schemas:
______MaPetiteEcole______________ 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
_____Inscription__________________ Δ 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
______SearchGroup________________ Χ MaPetiteEcole etud ? : STUDENT GROUP! : GROUP ________________ 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
______InitMaPetiteEcole________________ MaPetiteEcole _____________________ 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 ? : STUDENT RESULTS! : REPORT _______________________ 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.
Etc.
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.
Example:
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.
Genericity
Example
===== [X, Y] ================= first: X * Y → X ___________________ ! X: X; Y: Y • first (x, y) = x _________________________________________
Bibliography
In French, three books on Z.
 David Lightfoot, Formal specification with Z, Teknea, ( ISBN 2877170381 ) translated by Henri Habrias and PierreMarie Delpech (a short introductory book)
 JM Spivey, The Z score, Masson, PrenticeHall, ( ISBN 2225843678 ) translated by M. Lemoine (more complete)
 Pascal André and Alain Vailly, Corrected software design exercises: modeling of information systems by practice, ( ISBN 272981289X ) .