vignette|Exemple de spécification dans le langage Z formel.
La notation Z est un langage de spécification utilisé pour décrire et modéliser les systèmes informatiques.
Historique La notation Z a été créée par Jean-Raymond Abrial. Elle est apparue pour la première fois dans le manuel Méthodes de programmation. 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.
En 1983, Delobel et Adiba utilisent la notation Z d'origine dans leur livre « Bases de données et systèmes relationnels ». Sous le nom de « modèle relationnel binaire », il leur sert à introduire le « modèle relationnel n-aire » de Ted Codd. La notation graphique NIAM (Nijssen Information Analysis Method) développée au sein de Control Data à Bruxelles utilise ce modèle relationnel binaire.
La première norme internationale (ISO) sur la notation Z a été publiée en .
Description Une spécification en Z est un prédicat structuré en schémas. La spécification de l'invariant et la spécification des opérations ont la forme d'un prédicat.
La notation 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).
Notes et références
Annexes Bibliographie En français, trois livres sur Z. David Lightfoot, Spécification formelle avec Z, Teknea , traduit par Henri Habrias et Pierre-Marie Delpech (un petit livre d'introduction). J. M. Spivey, La Notation Z, Masson, Prentice-Hall , 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 .
Articles connexes Méthode formelle Méthode B
Catégorie:Méthode formelle Catégorie:Développement logiciel