Notation Z
La notation Z est un langage de spécification utilisé pour décrire et modéliser les systèmes informatiques.
Historique
modifierLa notation Z a été créée par Jean-Raymond Abrial. Z est apparu pour la première fois dans un livre, lors de l'édition en 1980 de l'ouvrage de Meyer et Baudouin, Méthodes de programmation, Eyrolles. Il n'existait alors que des notes de Jean-Raymond Abrial, internes à EDF. Elles faisaient suite à l'article qu'il avait publié en 1974, intitulé Data Semantics in Data Base Management (Kimbie, Koffeman, eds, North-Holland, 1974, p. 1-59).
En 1983, Delobel et Adiba utilisent la notation Z d'origine dans leur livre « Bases de données et systèmes relationnels » (Dunod). Sous le nom de « modèle relationnel binaire », il leur sert à introduire le « modèle relationnel n-aire » de Ted Codd. Une notation graphique utilise ce modèle relationnel binaire, c'est NIAM (Nijssen Information Analysis Method), (H. Habrias, Le modèle relationnel binaire, Eyrolles, 1988) développée au sein de Control Data à Bruxelles.
Abrial a porté Z au Programming Group d'Oxford en . Il a abandonné Z pour proposer la Méthode B dans les années 1980. La première norme internationale (ISO) sur Z a été publiée en .
Z en quelques mots
modifier- Une spécification en Z est un prédicat. La spécification de l'invariant et la spécification des opérations ont la forme d'un prédicat.
- La spécification est structurée en schémas.
- Z utilise :
- la théorie naïve des ensembles,
- la logique des prédicats du premier ordre,
- le calcul des propositions (et, ou, non, implication, etc.),
- les quantificateurs existentiels et universels (il existe, quel que soit),
- les relations (partie du produit cartésien de plusieurs ensembles).
Z par l'exemple
modifierOn utilise, quand c'est possible, la notation ASCII de B. On trouvera la correspondance avec la notation B à Méthode B.
Les ensembles de base
modifier[ETUDIANT, GROUPE]
ETUDIANT et GROUPE sont des types de base (les SETS de B)
Un schéma
modifierVoici ce qu'en Z, on appelle des schémas :
______MaPetiteEcole______________
promo : POW (ETUDIANT)
aPourGroupe : ETUDIANT → GROUPE
_________________
promo = dom (aPourGroupe)
_____________________________________
Un schéma a un nom, ici MaPetiteEcole, deux parties :
- celle du haut est appelée partie « typage ». On y déclare les variables et leur type.
- Ici, promo appartient à l'ensemble des parties (on dit aussi, ensemble des sous-ensembles) de ETUDIANT.
Rappelons que POW({1, 2}) = { {}, {1}, {2}, {1,2} }
- ETUDIANT → GROUPE est l'ensemble des fonctions partielles de ETUDIANT vers GROUPE. Ce qui se paraphrase : un étudiant est membre d'au plus un groupe.
- Quand on passe d'une ligne à l'autre, implicitement on écrit une conjonction.
- celle du bas est appelée partie « prédicative » (remarquons que la partie haute est aussi constituée de prédicats !...de typage)
- Ici, on a un prédicat d'égalité qui se paraphrase : l'ensemble des étudiants de la promo est égal au domaine de la fonction aPourGroupe, ce qui en français courant donne : « tout étudiant de la promo est membre d'un groupe ».
Un schéma d'opération
modifier_____Inscription__________________
Δ MaPetiteEcole
nouvEtud ? : ETUDIANT
gpe ? : GROUPE ________________ nouvEtud ? /: promo
promo' = promo \/ {nouvEtud ?}
aPourGroupe' = aPourGroupe \/ {nouvEtud ? |→ gpe ?}
_____________________________________
Δ déclare : promo, promo', aPourGroupe, aPourGroupe'. Le prime exprime l'état après l'opération.
Attention !
Vous avez bien lu. Ci-dessus, nous avons écrit = (prédicat d'égalité) et non := (substitution). Un schéma est un prédicat. Le saut de ligne exprime une conjonction (⩓).
Le schéma Inscription donne le prédicat qui doit être respecté par l'opération d'inscription.
Une opération d'interrogation
modifier______ChercherGroupe________________
Χ MaPetiteEcole
etud ? : ETUDIANT
grpe ! : GROUPE ________________
etud ? : promo
grpe ! : aPourGroupe (etud ?) _______________________________________
Χ déclare : promo, promo', aPourGroupe, aPourGroupe'et les contraintes :
promo = promo'
aPourGroupe' = aPourGroupe
Ce qui signifie qu'on ne veut pas que l'opération d'interrogation modifie l'état des données.
Un schéma va permettre de spécifier un état initial, lequel, comme en B, sert à s'assurer que l'on peut bien avoir un état satisfaisant les contraintes.
Schéma d'initialisation
modifier______InitMaPetiteEcole________________
MaPetiteEcole _____________________
promo = { }
aPourGroupe = { } ________________________________________
Un type libre
modifierRAPPORT ::= ok | déjàConnu | nonConnu
RAPPORT est un type libre.
Schémas avec type libre
modifier____Succès______________________________
résultat! : RAPPORT ___________________
résultat! = ok ________________________________________
____DéjàConnu___________________________
KHI MaPetiteEcole
etud ? : ETUDIANT
résultat! : RAPPORT
_______________________
etud ? : promo
résultat! = déjàConnu
________________________________________
Utilisation du schéma calculus
modifierOn va avoir une spécification robuste
RInscription == (Inscription & Succès) or DéjàConnu
Il y a d'autres opérateurs que le & et le or pour le calcul de schémas.
etc.
Nous avons présenté des schémas fermés. Les déclarations sont locales à ces schémas.
Schémas ouverts
modifierIl existe des schémas ouverts (description axiomatique) qui introduisent une ou plusieurs variables globales et éventuellement spécifient une contrainte sur leurs valeurs.
Exemple :
carré : NAT → NAT _________________
! n: NAT • carré(n) = n * n
La notation Z pour la description des ensembles en compréhension
modifier{...| ...• ...}
On distingue trois parties {déclaration | contrainte • expression }
exemple :
{x : NAT | pair (x) • x * x} est l'ensemble des carrés des nombres pairs.
Les schémas comme types
modifierOn peut prendre un schéma comme type.
Un schéma est alors vu comme l'ensemble des états qui respectent le schéma. Une variable de type schéma peut alors prendre comme valeur un de ces états qui respectent le schéma indiqué comme type de la variable.
Généricité
modifierExemple
=====[X, Y] ===================
first : X * Y → X
___________________
!x : X ; y : Y • first(x, y) = x _________________________________________
Bibliographie
modifierEn français, trois livres sur Z.
- David Lightfoot, Spécification formelle avec Z, Teknea (ISBN 2-87717-038-1), traduit par Henri Habrias et Pierre-Marie Delpech (un petit livre d'introduction).
- J. M. Spivey, La Notation Z, Masson, Prentice-Hall (ISBN 2-225-84367-8), traduit par M. Lemoine (plus complet).
- Pascal André et Alain Vailly, Exercices corrigés de conception logicielle : modélisation des systèmes d'information par la pratique (ISBN 272981289X).
