Remerciez-le!

Remerciez @Admin pour avoir partagé cet document gratuitement, de la manière la plus simple, en partageant sur les réseaux sociaux.

Chapitre 6 : Méthode Z Olfa Mosbahi olfamosbahi@gmail.com Modélisation des Syst

Chapitre 6 : Méthode Z Olfa Mosbahi olfamosbahi@gmail.com Modélisation des Systèmes GL3 2 Le langage Z a été développé à l’Université d’Oxford à la suite des travaux de Jean Abrial. C’est un langage formel qui utilise : les notions ensemblistes, le calcul des propositions (et, ou, non, implication, etc.) 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). Introduction 3 Ensembles Exemple : Le document de spécification contient tout d’abord une introduction informelle du problème traité. Introduction : Cette spécification concerne l’enregistrement des passagers à bord d’un avion. Les places ne sont pas numérotées. Les passagers sont autorisés à embarquer selon la règle du ‘premier arrivé, premier servi’. Sont ensuite décrits tous les types et toutes les variables utiles dans la spécification. La spécification utilise des ‘ensembles donnés’ dont on ne donne que le nom (‘given sets’). Elle utilise aussi une boîte à outils mathématique avec des ensembles prédéfinis comme les entiers naturels ( N) ou les booléens. 4 Types [PERSONNE] ensemble des personnes identifiées de manière unique capacité : N capacité de l’avion (entier naturel) OUIOUNON ::= oui | non ( la barre | indique un ou) REPONSE ::= OK | déjàABord | plein | deuxErreurs Puis vient la description de l’état du système. Il prend la forme d’un schéma avec : un nom, des déclarations précisant les types, et des propriétés (prédicats) précisant les valeurs. Ensembles 5 Etat du système C’est l’ensemble des personnes à bord. Il ne peut excéder la capacité de l’avion. Ensembles On décrit ensuite l’état initial du système comme un autre schéma. PX : est un élément de l’ensemble des sous ensembles de X, c’est à dire un ensemble d’éléments de X. #X : indique le cardinal de l’ensemble X (nb éléments) ; Cette propriété doit toujours être vraie ; C’est un invariant du système. 6 Etat initial du système : Ensembles On décrit les opérations qui peuvent faire évoluer l’état du système : embarquer, débarquer. Les schémas correspondants font référence au schéma Avion qui indique l’évolution du schéma Avion avant et après l’appel d’une opération (les états après l’opération sont marqués par une apostrophe). 7 Ensembles Avion : l’évolution du schéma Avion avant et après l’appel d’une opération. #àBord : état avant l’opération #àBord ’ : état après l’opération 8 Ensembles 9 n! est une sortie de l’opération Ensembles Les interrogations laissent l’état du système inchangé. Ce qu’indique le Xschéma (‘ksi schéma’) suivant : 10 et représentent le ‘et’ et le ‘ou’ Enfin, le traitement des erreurs peut être spécifié dans plusieurs schémas. Ensembles 11 Traitement des erreurs On donne en exemple le schéma lié aux erreurs d’embarquement. Ensembles 12 Les fonctions (ou plus généralement les relations) sont le moyen de relier les uns aux autres les ensembles utilisés dans la spécification. Une fonction f est définie dans un ensemble (son domaine, noté ‘dom f’) et prend ses valeurs dans un autre ensemble (son image, noté ‘ran f’ pour ‘range’). Une fonction est partielle si toutes les valeurs de départ n’ont pas d’image par la fonction f. Notation : Une fonction est totale si toutes les valeurs de départ ont une image par la fonction f. Notation : Fonctions 13 Fonctions  L’ajout d’un couple de valeurs à la fonction se note :  La modification du couple (x, y) par le couple (x, y’) se note :  La suppression du couple (x, y) se note : 14 Fonctions On donne ci-dessous un exemple de spécification de gestion d’un stock. Le niveau de stock est défini pour les produits stockés. Il peut exister des articles non stockés. [ARTICLES] : L’ensemble des articles (stockés ou non) Exemple : niveau est une fonction partielle car seuls les articles stockés ont un niveau) 15 Fonctions 16 Fonctions 17 Fonctions 18 Conclusion 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 des ensembles et la logique des prédicats d'ordre un. Un schéma a un nom, et deux parties : o celle du haut est appelée partie « typage ». On y déclare les variables et leur type. Quand on passe d'une ligne à l'autre, implicitement on écrit une conjonction. o celle du bas est appelée partie « prédicative » (prédicats de typage) uploads/Litterature/ chapitre-6-methode-z.pdf