INTRODUCTION

La langage Z a été développé à l’Université d’Oxford à la suite des travaux de Jean

René Abrial. C’est un langage formel qui utilise : les notions ensemblistes, le calcul des
propositions (et, ou, non, implication) et des prédicats (quantificateurs existentiels, il existe, et
universel, quel que soit), les relations (partie du produit cartésien de plusieurs ensembles) et
fonctions (relations avec au plus une image par valeur du domaine de définition), les
séquences ou suites (fonctions des entiers naturels dans un autre ensemble pour imposer un
ordre aux valeurs).

I- LA METHODE Z
La méthode Z est un langage de programmation formelle qui se distingue des méthodes
semi-formelles et informelles. Autrement dit la méthode Z offre un descriptif précis à l’usage
d’un logiciel ou d’une application pour éviter l’erreur de développement. C’est un langage de
spécification utiliser pour décrire et modéliser les systèmes informatiques.

1- SA STRUCTURE
Elle se présente sous la forme d’une collection de schémas décrivant les éléments du système
et a une structure encapsulant la description : des états possibles d’une partie ou du système
entier (collections de types et des variables de ces types), des relations qu’entretiennent les
variables, des effets des actions qui portent sur les variables.
Les schémas sont sous deux aspects :
▪ Aspects Statiques :
-États du système ;
-Propriétés invariantes pour un état et pour tous les états ;
▪ Aspects Dynamiques :
-Opérations qui modifient l’état ;
-Opérations qui consultent l’état (sans le modifier) ;
-Relations entre les entrées et les sorties.

a. Syntaxe

GENIE LOGICIEL 1
 b. Structure d’un schéma Z

Déclarations de variable de la forme :

< identificateur > : < type >
Les prédicats précisent les propriétés des variables et les relations entre variables.
Un schéma est utilisé afin de décrire un état ou une opération.
• Dans la description d’un état :
-Les variables déclarées représentent les composantes de l’état,
-Les prédicats expriment les propriétés invariantes de l’état.
• Dans la description d’une opération :
-Les déclarations incluent les composantes de l’état initial et celles de l’état
final, ainsi que tous les entrées et les sorties de l’opération.
-Les prédicats expriment les relations entre les entrées et les sorties, et
entre l’état initial et l’état final.

c. Schéma de ≪Prêts≫

2- SON BUT
La spécification formelle donne toujours une description de ce que doit faire le logiciel et
non pas comment elle doit le faire des spécifications formelles puisqu’elles reposent sur les
base mathématique le but est d’éliminer les ambiguïtés, les malentendus et les mauvaises
interprétations qui prouvent survenir dans la description en langage naturel.

3- SES OBJECTIFS
- Assurer de la fiabilité ainsi que de l’absence de bugs informatique d’un système par des
preuves mathématique ;
- Réaliser des interceptions ;
- Créer des sous-ensembles ;
- Compiler des sous-ensembles ;
- Intégrer ou exclure des éléments spécifiques ;
- Préciser l’existence d’ensembles vides au sein des lignes de code ;

GENIE LOGICIEL 2
 4- SON PRINCIPE
Principe de modularité : décomposition de la spécification en parties de
taille raisonnable, les schémas, portant sur un seul aspect du système à la
fois.

II- LES AUTRES METHODES DE SPECIFICATION

FORMELLES EN SYSTEME D’INFORMATION

➢ La méthode VDM ;
➢ La méthode B ;
➢ La méthode LOTOS ;
➢ La méthode Merise ;
➢ La méthode NIAM ;
➢ La méthode EXPRESS G ;
➢ La méthode UML ;
➢ La méthode OMT ;

CONCLUSION
La méthode Z est manifestement celle qui nous semble la plus prometteuse, elle est
applicable à tous les domaines de l’informatique, est statique et non-procédural, a une base
théorique saine ; elle est complète, combine la précision des mathématiques avec l’élégance
d’expression de langage de programmation actuels.

GENIE LOGICIEL 3
 Formalismes de spécification :
Langages formels de spécification catégorisés en deux grandes catégories :
Notations basées sur la théorie des modèles (adaptées aux spécifications de systèmes
d’information) :
-Les états cohérents du système et les opérations appropriées ;
Ex : le langage Z, Vienna Développent Method (VDM).
Notations basées sur des algèbres de processus : adaptées aux spécifications de systèmes
concurrentes :
-Correction des protocoles de communication inter-processus ;
Ex : Communicating Sequential Processes (CSP), CCS, LOTOS.

GENIE LOGICIEL 4