Notation Z
Logiciels:
* Z-Eves
* Ztec (vérification de types)
* Accepte les format de fichier LateX, ZSL et ZBX pour la notation Z.
* Zans (animation des spec. Z)
En Z, on modélise les actions
a) les opérations modifient les variables du système (écriture/modification/ajout)
b) les requêtes ne modifient pas les variables du système (lecture)
Le système est représenté par un schéma d'état:
a) une partie déclaration
b) une partie prédicative où sont énoncés les invariants.
Rappel: un invariant est une condition qui doit toujours être vraie pour chaque état du système.
Un document Z se séparent en 7 sections distinctes:
1) les types utilisés
2) les définitions axiomatiques
3) le schéma d'états (peut être construit avec plusieurs petit schémas)
4) Initialisation du système (sous forme de schéma)
5) Opérations et les requêtes (sous forme de schéma)
6) Traitement des cas "anormaux" (sous forme de schéma)
7) Les versions finales des opérations.
1) les types utilisés
global
identifiant: type
Exemple
global
monEntier: Z
monNaturel: N
monNaturelSansZero: N1
2) les définitions axiomatiques (ou les définitions de constantes)
axiom
monEntier = 5
end axiom
3) le schéma d'états (peut être construit avec plusieurs petit schémas)
4) Initialisation du système (sous forme de schéma)
%%init-schema NomSchema
5) Opérations et les requêtes (sous forme de schéma)
6) Traitement des cas "anormaux" (sous forme de schéma)
7) Les versions finales des opérations.
Langage
A) Les types de base:
- prédéfinis: Z (entier), N (naturel), N1 (naturel sans zéro)
- inventé: [TYPE1, TYPE2, TYPE3]
Ce qui veut dire: une variable peut être de type TYPE1, TYPE2 ou TYPE3.
Exemple: variable1: TYPE1
variable2: TYPE2
variable3: TYPE3
- énuméré: ETAT ::= on | off | idle
Ce qui veut dire: un variable de type ETAT peut avoir seulement les valeurs on, off ou idle.
Exemple: variable1: ETAT
variable1' = on
variable1' = off
variable1' = idle
- Équilalence: TYPE2 == TYPE1
Exemple: DE == 1..6
ENTIER == Z
NODOC == {4,8,42,56}
B) Les variables
Déclaration: identifiant : type
Variable d'entrée: identifiant? : type
Varable de sortie: identifiant! : type
Exemple:
[PERSONNE, STUDENT]
ETAT ::= a | b | c
DE == 1..6
var1 : PERSONNE
var2 : ETAT
var3 : {2,4,16,22}
var4 : DE
tested : P STUDENT (P signifie Powerset, un ensemble de type STUDENT]
listeEtat : P ETAT
C) Expressions arithmétiques
- arithmétiques: +, -, mod, div, *, succ x (successeur, x=x+1)
- relation : =, /= (pas égal), <, <=, >, >=
- ensemble : sub (sous ensemble), subeq (sous ensemble ou égal), {} (ensemble vide0,
in, notin,
|| (union), && (intersection), \, #, P (powerset), & (multiplication x)
Note: l'opérateur & (multiplication) produit des paires
- logique: true, false, not, <=>, =>, and, or
D) Ensemble
- description simple
- sous forme d'intervalle 1..6
- en compréhension {1,2,3,4,5,6,7}
E) Les fonctions
Fonction partielle +->
Fonction totale -->
Fonction injective partielle >+>
Fonction injective totale >->
Fonction subjective partielle +>>
Fonction subjective totale ->>
Bijection >->>
F) Les relations
Relation: R : A <-> B
R~ : relation inverse de R, B vers A (R doit etre une fonction)
Forme un couple entre les éléments de l'ensemble A avec les éléments de l'ensemble B
On peut aussi l'écrire: Relation : P (A x B)
Opérateur:
dom Rel : retourne le domaine de la relation (un ensemble)
ran Rel : retourne l'image de la relation (un ensemble)
G) Ensemble et quantificateurs
{ declaration | predicat @ expression }
{ declaration | predicat }
{ declaration @ expression }
Exemple:
Ensemble des nombres de 200 à 300
NB1 = {i : 0..200 | i >= 100 and i <= 150 @ 2*i}
Ce lit: Place dans l'ensemble NB1, la liste des nombres "i multipliés par 2",
tel que i est plus grand ou égale à 100 et plus petit ou égale à 150
depuis l'ensemble de départ des nombres de 0 à 200.
Ensemble des nombres de 100 à 150
NB2 = {i : 0..200 | i >= 100 and i <=150 }
Place dans l'ensemble NB2, la liste des nombres i
tel que i est plus grand ou égale à 100 et plus petit ou égale à 150
depuis l'ensemble de départ des nombres de 0 à 200.
Ensemble des conditions vraie / fausses de 0 à 200
NB3 = {i : 0..200 @ i >= 100 ET i <=150 }
Place dans l'ensemble NB3, le résultat booléen de la condition
"i est plus grand ou égale à 100 et plus petit ou égale à 150"
depuis l'ensemble de départ des nombres de 0 à 200.
Ce qui donne faux de 0 à 99, vrai de 100 à 150 et faux de 151 à 200
Ensemble de couple (d'une fonction)
COUPLE = { x, y : Z | y= 3x + 8 @ (x,y) }
Place dans l'ensemble COUPLE, les couples formés de x et de y
tel que y = 3x + 8
depuis les deux ensembles x (entiers) et y (entiers)
Quantificateurs
Pour tous les éléments de l'ensemble (ou des ensemble), le prédicat est vrai tant que la contrainte est respectée.
forAll declaration | contrainte @ predicat
Il existe au moins un élément de l'ensemble (ou des ensemble) tel que le prédicat est vrai si on respecte la contrainte.
exists declaration | contrainte @ predicat
Il existe seulement un élément de l'ensemble (ou des ensemble) tel que le prédicat est vrai si on respecte la contrainte.
exists1 declaration | contrainte @ predicat
2. Schémas
2.1 Définition axiomatique pour définir des constantes en Z
Définition:
| déclaration
+------------
| prédicative
Exemple 1:
| capacite : N
| lampe : {on, off}
+------------------
| capacite = 468
Exemple 2:
global
capacite: N;
lampe : {on, off}
axiom
capacite = 468
lampe = on
end axiom
2.2. Schéma
+--- Nom ----
| déclaration
+------------
| prédicat
+------------
schema nom
déclaration
where
prédicat
end schema
+--- Avion -------------
| abord : P Personne
+-----------------------
| #abord >= capacite
+-----------------------
Opérations sur les schémas
A) Inclusions
B) Inclusions décorées
C) Inclusion Delta : modification du système
D) Inclusion Xi.
A) Inclusion
+--- S ---
| avion
+---------
|
+---------
Le résultat: le schéma S comprend toutes les déclaration de "avion" et tous ses prédicats
Les prédicats sont fusionnés à ceux qui existent dans S (avec and)
Utilisation: sert à construire un schéma du système par morceau
B) Inclusion dérivée
+--- S ---
| avion'
+---------
|
+---------
Résultat: le schéma S contient toutes les déclarations des variables' du schéma "avion"
Tous les prédicats de avion dans leurs versions prime '
Utiliser pour l'action d'initialisation des schémas.
C) Inclusion Delta
+--- S ---
| delta avion
+---------
|
+---------
Résultat: Les déclarations de l'avion en version prime' et non prime
Les prédicats de avion en version ' et non '
Utiliser pour spécifier les opérations
Exemple:
+--- Embarquer ---
| delta avion
| p? : PERSONNE
| m! : MESSAGE
+---------
| #abord < capacite
| p? notin abord
| abord' = abord || {p?}
| m! = OK
+---------
Signifie en objet:
avion::test_embarquer(PERSONNE p?) {
si avion.abord.length < avion.capacite AND p? notin avion.abord {
abordtmp = avion.abord
MESSAGE m! = avion.embarquer(p?);
assert( avion.abord = ( abordtmp || {p?} ) );
assert( m! == OK );
}
}
D) Inclusion Xi
+--- S ---
| [-] avion
+---------
|
+---------
Résultat: pareil que Delta
Dans la partie prédicative, pour chaque variable système, on voit apparaître variable' = variable.
Utiliser pour spécifier des requêtes ou des actions
qui ne modifient pas l'état du système.
Version Finale
===============
action =^= action0 \/ action1 \/ action2 \/ ...
Exemple:
+-- debarquer0 ----
| delta avion
| p? : PERSONNE
| m! : MESSAGE
+------------------
| p? in abord
|
| abord' = abord \ {p?}
| m! = OK
+------------------
+-- debarquer1 ----
| [-] avion
| p? : PERSONNE
| m! : MESSAGE
+------------------
| p? notin abord
| m! = FAILED
+------------------
debarquer =^= debarquer0 \/ debarquer1
Règle 1: Les associations deviennent des fonctions ou des relations.
Exemple:
PERSONNE --> DATE
PERSONNE +-> DATE
ensemble' = ensemble || {(x?,d?)}
ensemble' = ensemble || {x?->d?}
Règle 2: parmis tous les attributs des éléments du domaine, qu'est-ce qui permet de distinguer 2 éléments?
anniversaire : NOM +-> DATE
Qu'arrive-t-il au auxtres attributs
Former des paires...
Ajout : Union ||
Soustraction: \
Mise à jour : (+) +=
Exemple: ann' = ann \ { x? -> d? } || { x? -> d? }
ann' = ann' \ { x? -> ann(x?) } || { x? -> d? }
ann' += { x? -> d? }
Le résultat est une fonction qui "fonctionne" comme f partout
dans le domaie sauf pour les éléments qui concernent "g".
Zans se sert des invariants pour complétés les post-conditions
Exemple:
scheme Retrait
Delta Carnet;
nom? : NOM;
where
nom? in amis;
ann' = ann \ { x? -> ann(x?)}
amis' = amis \ { nom? }
end schema
Parenthèse:
En Z, les schémas sevent à construire des preuves
exists x in N | filtre @ predicat;
exists Carnet? @ ajout
exists amis ? P nom; ann : NOM +-> DATE | amis' = dom ann @ ...
la caractéristique (attribut) qui rend un objet unique
nous permet d'écrire des fonctions ayant pour domaine l'ensemble des attributs
Que faire avec les attribus qui reste?
+--- choix ---
| amis : P NOM
| adresse : NOM +-> ADRESSE
| courriel: NOM +-> COURRIEL
| ann : NOM +-> DATE
+-------------
Test d'appartenance
===================
Choix 1 : nom? in amis
Choix 2 : exists d: date and a:adresse and c: courriel @ (nom?, d, a, c) in amis
Choix 3 : amis : P nom
info : nom +-> P (adresse & courriel & date)
Carte! = { a:amis | ann(a) = aujourdhui? @ a }
{ n:nom | n in amis and ann(n) = aujourdhui? @ n }
{ a:amis | (a, aujourdhui?) in ann @ a }
{ n:nom | (a:adresse, c:courriel @ (n, aujourdhui?,c,a) in amis) @ n }
1 à N
emprunts : client +-> P video
emprunts : client <-> video
P (client & video)
Pour toute relations:
R |> s : restreindre l'image de R à l'ensemble s
s <| R : restreindre le domaine de R à s
R +> s : restreindre l'image de R à tout ce qui n'est pas dans s
s <+ R : restreindre le domaine de R à tout ce qui n'est pas dans s
Exemple:
{42} <| emprunts : retourne seulement les enregistrements dont le domaine est 42.
fonction param = fonction(param)
Séquence
========
Une séquence est un tableau (ensemble d'index associé à un ensemble d'élément)
Fonction de N -> [x]
chaineCaractere: seq CHAR
nomSequence: seq TYPE ex: route = <<MTL, QC, TOR, MTL>>
nomSequence: iseq TYPE ex: route = <<MTL, QC, TOR>> (pas de doublons)
Route correspond à un ensemble de paire avec index { (1, MTL), (2, QC), (3, TOR), (4, MTL) }
Accès à une valeur: nomSequence(index) (index commence à 1)
Opérateur: first nomSequence (retourne la première valeur)
last nomSequence (retourne la dernière valeur)
tail nomSequence (retourne une sequence de tous les éléments sauf la première valeur)
front nomSequence (retourne une sequence de tous les éléments sauf la derniere valeur)
Concaténation: nomSequence ^ nomSequence2
Longueur: #nomSequence
Test:
élément fais partie de la séquence : élement in ran sequence
élément ne fait pas partie de la séquence: élément not in ran sequence
Pour convertir un ensemble de paire en séquence, on utilise
squash( ensemble_de_paire )
Initialisation:
schema SeqInit
NomSchema'
where
sequence' = <<>>
end schema
Représenter une suite de caractère:
1. Définir le caractère.
[CHAR]
2. Créer un schéma texte qui contient une variable avec une séquence de caractère (suite avec ordre = séquence)
+- text --
| chaine : seq CHAR
+---------
Retourner la position d'une chaine dans une chaine. pos = strstr(text, chaineChercher)
S'il est vrai qu'il existe une chaine "avant" concaténé à la chaine pat? concaténé à la chaine apres
qui équivaut à ma chaine alors la position est égale au nombre de caractère avant ma chaine + 1.
Si ce n'est pas vrai (condition contraire), alors je retourne 0.
+---------
| [-] text
| pat?: seq CHAR
| pos!: N
+---------
| ( (exists avant, apres: seq CHAR @ avant ^ pat? ^ apres = chaine ) /\ pos! = #before + 1 )
| \/
| ( not (!exists avant, apres: seq CHAR @ avant ^ pat ? ^ apres = chaine ) /\ pos! = 0 )
+---------
Notation: ( pre1 est vrai ET post1 est vrai ) OU ( pre2 est vrai ET post2 est vrai )
Note, qu'il pourrait exister plusieurs before, mais que c'est seulement le premier qui est retourné
Hyperliens...