La notation formelle Z

Z
L'exemple classique (fourni par Mike Spivey dans La notation Z, Masson, traduit par Michel Lemoine, 1994)
Le carnet d'anniversaire
Nous utilisons, quand c'est possible, la notation ASCII de B.
 

[NOM, DATE]

NOM et DATE sont des types de base (les SETS de B)
Voici de qu'en Z, on appelle des schémas :
 

______CarnetDAnniversaire______________
    connu : POW (NOM)
    anniversaire : NOM +-> DATE
_________________
    connu = dom (naissance)
_____________________________________

_____AjoutAnniversaire__________________
    DELTACarnetDAnniversaire
    nom? : NOM
    date? : DATE
________________
     nom? /: connu
    anniversaire' = anniversaire \/ {nom? |-> date?}
_____________________________________

DELTA déclare : connu, connu', anniversaire, anniversaire'. Le prime exprime l'état après l'opération.
 
Attention !
Vous avez bien lu. Ci-dessus, nous avons écrit = et non :=. Un schéma est un prédicat. Le saut de ligne exprime une conjection.
Le schéma AjoutAnniversaire donne le prédicat qui doit être respecté par l'opération d'ajout.
 

______ChercherAnniversaire________________
    KHICarnetDAnniversaire
    nom? : NOM
    date! : DATE
________________
    nom? : connu
    date! : anniversaire (nom?)
_______________________________________

  KHI déclare : connu, connu', anniversaire, anniversaire' et les contraintes :
connu = connu'
anniversaire' = anniversaire
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.

 
______InitCarnetDAnniversaire________________
    CarnetDAnniversaire
_____________________
    connu = { }
________________________________________ RAPPORT ::= ok | déjàConnu | nonConnu

RAPPORT est un type libre.
 

____Succès______________________________
    résultat! : RAPPORT
___________________
    résultat! = ok
________________________________________

____DéjàConnu___________________________
    KHICarnetDAnniversaire
    nom? : NOM
    résultat! : RAPPORT
_______________________
    nom? : connu
    résultat! = déjàConnu
________________________________________

Utilisation du schéma calculus :
On va avoir une spécification robuste

 
RAjoutAnniversaire == (AjoutAnniversaire & 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.
Il existe des schémas ouverts (description axiomatique) qui introduisent une ou plusieurs variables globales et éventuellement spécifient une contraintes sur leurs valeurs.
Exemple :
 

    carré : NAT --> NAT
_________________
    ! b: NAT . carré(n) = n * n

La notation Z pour la description des ensembles en compréhension :
{...| ... ....}
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
On 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 est alors une variable qui peut prendre comme valeur un de ces états qui respectent le schéma indiqué comme type de la variable.
 
Généricité
Exemple
 

=======[X, Y] =============================
    first : X * Y --> X
___________________
    !x : X ; y : Y . first(x, y) = x
_________________________________________

Bibliographie
En français, deux livres sur Z.
Une introduction avec
D. Lightfoot, Spécification formelle avec Z, Teknea, traduit par H. Habrias
J.M. Spivey, La notation Z, Masson, traduit par M. Lemoine