Le langage Z

Résumé du document

Cours détaillé sur le Langage Z : comment est né le langage Z ? A quoi sert-il ? Quels sont les démarches de spécification ? Le langage Z mathématique ? Le langage Z schématique ? Qu'est-ce que le raffinement ?

Extraits

[...] Modélisation des données Types [PATIENT] δ 20 MAX = La spécification utilise : un ensemble ‘PATIENT' qui représente l'ensemble des patients identifiés de manière unique. ‘MAX' est une constante dont la valeur est de 20. elle indique la capacité de la salle selon le nombre de patients. Etat du système Le systeme represente l'ensemble des patients se trouvant dans la salle d'attente de l'hôpital. SalleAttenteHôpital patients :seq PATIENT . #patients MAX j #patients / i j patients patients(j) patients est un élément de seq PATIENT, tel que seq PATIENT est l'ensemble de toutes les séquences formées par les éléments de l'ensemble PATIENT. [...]

[...] -Le langage Historique du langage Z Le langage Z a été développé à l'Université d'Oxford à la suite des travaux de Jean René Abrial. Ce langage 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 pp. [...]

[...] Le schéma S T est défini ci-dessous : b:B Un même membre déclaré dans les deux schémas doit être du même type (tel que sinon la conjonction serait impossible. La conjonction de deux schémas peut se faire aussi par l'inclusion schématique (vue cité cidessus). Décorations schématiques Il est facile, quand on rédige des spécifications formelles, d'atteindre rapidement l'illisibilité. Un mécanisme fournit par le langage schématique de Z pour alléger les écritures s'appelle la décoration des membres. La présence de décorations dans un schéma indique la nature orientée opération de celui-ci. [...]

[...] On note : x y ou encore y). Notation Z des relations : Soit deux ensembles x et toute relation ayant comme ensemble de départ et y comme ensemble d'arrivée sera R : P(x Par volonté de simplification, on utilise habituellement une notation différente qui aura exactement le même sens x y Domaine, image, relation inverse : Soit deux ensembles, x et y et la relation R : x y . En les ensembles suivants sont définis : Domaine de R : dom x y Image de R : ran R Relation inverse ~ R : X ; y : Y x y x y y Restrictions de domaine et d'image : il est possible de définir une relation par restriction de valeurs de l'ensemble domaine d'une relation R aux valeurs contenues dans un sous ensemble de X. [...]

[...] La normalisation ISO de Z ne fera qu'accroître son utilisation dans l'industrie. Cependant, l'usage du et les méthodes formelles en général n'est pas fréquent faute de les maîtriser : en effet, les méthodes formelles nécessitent beaucoup de pratiques et d'entraînements pour être appliquées efficacement. De plus, Z n'est pas adapté pour tous les problèmes notamment pour les problèmes de concurrence. Aujourd'hui, la méthode B et son langage également développés par J.R. Abrial, tend à remplacer la Z. B s'intéresse au processus qui va de la spécification formelle au programme. [...]