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 methode z GL Modélisation des Systèmes Chapitre Méthode Z Olfa Mosbahi olfamosbahi gmail com CIntroduction 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

GL Modélisation des Systèmes Chapitre Méthode Z Olfa Mosbahi olfamosbahi gmail com CIntroduction 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 quanti ?cateurs 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é ?nition les séquences ou suites fonctions des entiers naturels dans un autre ensemble pour imposer un ordre aux valeurs CEnsembles Exemple Le document de spéci ?cation contient tout d ? abord une introduction informelle du problème traité Introduction Cette spéci ?cation 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éci ?cation La spéci ?cation 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é ?nis comme les entiers naturels N ou les booléens CEnsembles Types PERSONNE ensemble des personnes identi ?é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 CEnsembles Etat du système C ? est l ? ensemble des personnes à bord Il ne peut excéder la capacité de l ? avion 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 On décrit ensuite l ? état initial du système comme un autre schéma CEnsembles Etat initial du système 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 CEnsembles ? 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 CEnsembles CEnsembles Les interrogations laissent l ? état du système inchangé Ce qu ? indique le Xschéma ? ksi schéma ? suivant n est une sortie de l ?