ISO 13568

ISO 13568

Notation Z

La notation Z est un langage de spécification utilisé pour décrire et modéliser les systèmes informatiques.

Sommaire

Historique

La notation Z a été créée par J.R. 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, pp. 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.

J.R. Abrial a porté Z au Programming Group d'Oxford en septembre 1987.

J.R. Abrial a abandonné Z pour proposer la Méthode B dans les années 80.

La première norme internationale (ISO) sur Z a été publiée en juillet 2002.

Z en quelques mots

  • 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 et la logique des prédicats d'ordre un.

Z par l'exemple

On 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

[ETUDIANT, GROUPE]

ETUDIANT, et GROUPE sont des types de base (les SETS de B)

Un schéma

Voici 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

_____Inscription__________________
Δ MaPetiteEcole
nouvEtud ? : ETUDIANT
gpe ? : GROUPE ________________ nouvEtud ? /: promo
promo' = promo \/ {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

   ______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

   ______InitMaPetiteEcole________________
MaPetiteEcole _____________________
promo = { }
aPourGroupe = { } ________________________________________

Un type libre

RAPPORT ::= ok | déjàConnu | nonConnu

RAPPORT est un type libre.

Schémas avec type libre

   ____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

On 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

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 peut alors 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.

  • 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)

Voyez également

Liens externes

  • http://vl.zuser.org/ : The Z Notation (L'information en anglais)
  • voir une bibliographie détaillée et commentée [1]
Ce document provient de « Notation Z ».

Wikimedia Foundation. 2010.

Contenu soumis à la licence CC-BY-SA. Source : Article ISO 13568 de Wikipédia en français (auteurs)

Игры ⚽ Нужен реферат?

Regardez d'autres dictionnaires:

  • Iso 216 — Dimensions ISO 216 (mm × mm) Séries A A0 841 × 1189 A1 594 × 841 A2 420 × 594 A3 297 × 420 A4 210 × 297 A5 148 × 210 A6 …   Wikipédia en Français

  • ISO/CEI 8859 — ISO 8859 ISO 8859, également appelée plus formellement ISO/CEI 8859, est une norme commune de l ISO et de la CEI de codage de caractères sur 8 bits pour le traitement informatique du texte. Le standard est divisé en parties numérotées publiées… …   Wikipédia en Français

  • ISO/IEC 8859 — ISO 8859 ISO 8859, également appelée plus formellement ISO/CEI 8859, est une norme commune de l ISO et de la CEI de codage de caractères sur 8 bits pour le traitement informatique du texte. Le standard est divisé en parties numérotées publiées… …   Wikipédia en Français

  • ISO 3166-1 — est une des parties de la norme ISO 3166. Publiée pour la première fois en 1974 par l’ISO, elle attribue 3 codes pour les pays du monde : ISO 3166 1 alpha 2 : codes à deux lettres pour de nombreuses applications, notamment les domaines… …   Wikipédia en Français

  • ISO 8859 — ISO 8859, également appelée plus formellement ISO/CEI 8859, est une norme commune de l ISO et de la CEI de codage de caractères sur 8 bits pour le traitement informatique du texte. Le standard est divisé en parties numérotées publiées séparément …   Wikipédia en Français

  • Iso 8859 — ISO 8859, également appelée plus formellement ISO/CEI 8859, est une norme commune de l ISO et de la CEI de codage de caractères sur 8 bits pour le traitement informatique du texte. Le standard est divisé en parties numérotées publiées séparément …   Wikipédia en Français

  • ISO 4217 — (ИСО 4217) Коды для представления валют и фондов Codes for the representation of currencies and funds  (англ.) Codes pour la représentation des monnaies et types de fonds  (фр.) …   Википедия

  • ISO 9000 — ISO 9000  серия международных стандартов, описывающих требования к системе менеджмента качества организаций и предприятий. Серия стандартов ISO 9000 разработана Техническим комитетом 176 (ТК 176) Международной организации по стандартизации.… …   Википедия

  • ISO 3166-1 — ISO 3166 1  часть стандарта ISO 3166, содержащая коды названий стран и подчинённых территорий. Впервые опубликована в 1974 году. Определяет три разных кода для каждой страны: ISO 3166 1 alpha 2 (англ.)русск., двухбуквенная система …   Википедия

  • ISO 3166 — is a standard published by the International Organization for Standardization (ISO). It defines codes for the names of countries, dependent territories, special areas of geographical interest, and their principal subdivisions (e.g., provinces or… …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”