Notation Z

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

History

Notation Z was created by J.R. Abrial. Z appeared for the first time in a book, at the time of the edition in 1980 of the work of Meyer and Baudouin, Méthodes of programming, Eyrolles. There did not exist whereas notes of Jean-Raymond Abrial, interns at EDF. They made following the article that it had published in 1974, entitled Data Semantics (in Dated Base Management (Kimbie, Koffeman, eds, North-Holland, 1974, pp. 1-59).

In 1983, Delobel and Adiba use notation Z of origin in their book “Databases and systems relational” (Dunod). Under the name of “binary relational model”, it is used to them to introduce the “n-ary relational model” of Ted Codd. A graphic notation uses this binary relational model, it is NIAM (Nijssen Information Analysis Method), (H. Habrias, the binary relational model, Eyrolles, 1988) developed within Control Dated in Brussels.

J.R. Abrial carried Z in Programming Group of Oxford in September 1987.

J.R. Abrial gave up Z to propose the Méthode B in the Eighties.

The first international standard (ISO) on Z was published in July 2002.

Z in a few words

a specification in Z is a predicate. The specification of the invariant and the specification of the operations have the form of a predicate.
the specification is structured in diagrams.
Z uses the naive set theory and the logic of the predicates of order one.

Z for the example

One uses, when it is possible, the ASCII notation of B. One will find the correspondence with the notation B with Méthode B.

Basic units

GROUP

STUDENT, and GROUP are basic types (the SETS of B)

A diagram

Here what in Z, one calls of the diagrams:

______MaPetiteEcole______________
promotion: POW (STUDENT)
aPourGroupe: STUDENT +-> GROUPE
_________________
promotion = dom (aPourGroupe)
___________________________________

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

that top is called part “typing”. One declares the variables and their type there.

Here, promotion belongs to all the parts (one also says, together subsets) of STUDENT.

Let us recall that POW ({1, 2}) = {{}, {1}, {2}, {1,2}}

STUDENT +-> GROUP is the whole of the functions partial of STUDENT towards GROUP. What paraphrase: a student is member of with more the one group.
When one passes from one line to the other, implicitly one writes a conjunction.

that of bottom is called “predicative” part (notice that the high part also makes up of predicates! … of typing)

Here, one has a predicate of equality which paraphrase: the whole of the students of promotion is equal to the field of the function aPourGroupe, which in current French gives: “very studying promotion is member of a group”.

A diagram of operation

_____Inscription__________________
Δ MaPetiteEcole
nouvEtud? : ETUDIANT
gpe? : GROUP ______________ nouvEtud? /: promo
promo' = promotion \/{nouvEtud? |- > gpe?}
___________________________________

Δ declares: promotion, promo', aPourGroupe, aPourGroupe'. The premium expresses the state after the operation.

Caution!

You read well. Above, we wrote = (predicate of equality) and not: = (substitution). A diagram is a predicate. The jump of line expresses a conjunction (⩓).
The Inscription diagram gives the predicate which must be respected by the operation of inscription.

An operation of interrogation

______ChercherGroupe______________
Χ MaPetiteEcole
etud? : STUDENT
grpe! : GROUP ________________
etud? : promo
grpe! : aPourGroupe (etud?) _____________________________________

Χ declares: promotion, promo', aPourGroupe, aPourGroupe' and constraints:
promotion = promo'
aPourGroupe' = aPourGroupe

What means that it is not wanted that the operation of interrogation modifies the state of the data.

A diagram will make it possible to specify an initial state, which, as out of B, is used to make sure that one can have a state satisfying well the constraints.

Diagram of initialization

______InitMaPetiteEcole________________
MaPetiteEcole _____________________
promotion = {}
aPourGroupe = {} ______________________________________

A free type

REPORT/RATIO:: = ok | déjàConnu | nonConnu

REPORT/RATIO is a free type.

Diagrams with free type

____Succès______________________________
result! : REPORT/RATIO ___________________
result! = ok ______________________________________

____DéjàConnu_________________________ KHI MaPetiteEcole
etud? : ETUDIANT
result! : REPORT/RATIO _____________________ etud? : promo
result! = déjàConnu ______________________________________

Use of the diagram calculus

One will have a robust specification

RInscription == (Inscription & Success) gold DéjàConnu

There are other operators that it & and gold for the calculation of diagrams.

etc

We presented closed diagrams. The declarations are local with these diagrams.

Open diagrams

There exist open diagrams (axiomatic description) which introduce one or more aggregate variables and possibly specify constraints on their values.

Example:

square: NAT --> NAT _________________
! b: NAT • square (N) = N * N

Notation Z for the description of the whole in comprehension

{… | … • …}

One distinguishes three parts {declaration | constraint • expression}

example:

{X: NAT | par (X) • X * X} is the whole of the squares of the even numbers.

Diagrams like types

One can take a diagram like type.

A diagram is then seen like the whole of the states which respect the diagram. A variable of the diagram type can then take as value one of these states which respect the diagram indicated like type of the variable.

Generics

Exemple

======= Y =============================
first: X * Y --> X
___________________
! X: X; there: Y • first (X, there) = X _______________________________________

Random links: