UniversityLibHub Documents

La méthode B AMN(Abstract Machine Notation) "Génie Logiciel II"

École Nationale des Sciences de l'Informatique (ENSI)
1/1
100%

Cours "Génie Logiciel II" Chapitre 2: La méthode B AMN(Abstract AMN(Abstract Machine Machine Notation) Niveau: II2 Enseignante: Rim DRIRA [email protected] AU: 2017/2018 1 Chapitre2: La méthode B Plan ∎ Présentation ∎ Notion de machine abstraite ∎ Les clauses d’une machine abstraite ∎ ∎ Les Les obligations obligations de de preuve preuve ∎ Définition et calcul des substitutions généralisées ∎ Notation de modélisation des données ∎ Le processus de raffinement ∎ Les obligations de preuve du raffinement ∎ La modularité 2 Présentation de B et de ses ses concepts concepts de de base base 3 Historique □ Née dans les années 80 □ Fondateur: Jean-Raymond Abrial (un informaticien français ) □ Livre de référence: « The B Book » [1] □ □ Le Le choix choix du du nom nom B B est est une une sorte sorte d'hommage aux membres du groupe BOURBAKI. ∎ C’est un groupe de mathématiciens français qui a entrepris en 1939 une refonte des mathématiques en les prenant à leur point de départ logique. 4 Présentation □ B est issue de Z et VDM. □ La particularité de B : établir une chaîne de production qui va des spécifications spécifications au au code code source source associé. associé. □ B est basée sur la théorie des ensembles et la logique du premier ordre 5 Présentation □ Les logiciels conçus avec la méthode B fonctionnent conformément à leurs spécifications ∎ Les propriétés sont exprimées par des invariants invariants et et vérifiées vérifiées par par preuves preuves formelles. □ Un exemple industriel de l’utilisation de la méthode B: le pilote automatique embarqué (PAE) de METEOR de la ligne 14 du métro parisien 6 PA: propriété abstraite PR: propriété de raffinement raffinement Preuve du raffinement Raffinement Raffinement 2 Méthode B Raffinement 2 Raffinement n-1 Raffinement n Code Modèle abstrait Raffinement 1 Preuve PA Preuve PR 1 Preuve Preuve PR PR 2 Preuve PR n-1 Preuve PR n 7 Documentation et outillage □ Documentation disponible ∎ http://www .dmi.usher b.ca/~frap pier/igl50 1/ref/B/ Ma nrefb.pdf □ Outils en licence libre ∎ Exemple: Atelier B (http://www.atelierb.eu/telechargement/) 8 Atelier B □ Développé par la société ClearSy, □ Outil qui permet une utilisation opérationnelle de la méthode formelle B pour des développements de logiciels prouvés prouvés □ Disponible en deux versions: ∎ une version communautaire accessible à tous sans limitation, ∎ une version maintenue accessible aux possesseurs d’un contrat de maintenance. http://www.atelierb.eu 9 Atelier B Source: http://www.atelierb.eu 10 Notion de machine abstraite □ Dans abstraite B, un qui composant contient: logiciel est appelé machine ∎ Des données ∎ Des opérations □ Connue Notation) aussi sous l’acronyme AMN (Abstract Machine □ □ Avec Avec B, B, ∎ On spécifie ∎ On prouve ∎ On raffine ∎ On code Une (ou plusieurs) machine(s) abstraite(s) □ Cette notion est proche de: ∎ Type abstrait, Module, Classe, Composant 12 Quelques remarques □ Les distinguées. lettres minuscules et majuscules sont □ Les deux "/*" commentaires commentaires commentaires et caractères par les deux "*/". "*/". de sont début caractères délimités de commentaire de par fin les de □ Un lettres, "_". lettre. identificateur Le premier de chiffres caractère est ou une du caractère séquence doit être une souligné de ∎ Tout doit identificateur: variable, respecter ce qu’on d’une lui les le constante, nom attribue règles d’une de nous etc. définition machine, même d’un d’une des noms 13 Principales clauses MACHINE En-tête Nom de la machine abstraite (idem nom de la classe) CONSTRAINTS Contraintes sur les paramètres d’une machine s’il y en a SETS Déclaration des ensembles abstraits et énumérés CONSTANTS Définition des constantes Partie PROPERTIES Propriétés sur les constantes - Une clause ne doit pas apparaître plus qu’une fois Partie - - L’ordre L’ordre des des clauses clauses n’est n’est pas pas imposé imposé Statique Partie dynamique Propriétés sur les constantes VARIABLES Déclaration des variables (idem attributs d’une classe) DEFINITIONS expression Contient une ou liste une d'abréviations substitution. pour un prédicat, une INVARIANT Typage et propriété des variables INITIALISATION Définition constructeur) de la valeur initiale des variables (idem OPERATIONS Déclaration des opérations (idem méthodes) END 15 Les clauses d’une machine abstraite L’en-tête □La partie en-tête contient: Nom de la machine Paramètres de la machine (pour la généricité) Contraintes sur les paramètres □Clauses □Clauses MACHINE Nom formels) de la machine abstraite (paramètres CONSTRAINTS machine Contraintes s’il y sur en a les paramètres d’une 16 Les clauses d’une machine abstraite L’en-tête □ Il formels est optionnel qu’une machine possède des paramètres □ Les paramètres d’une machine sont de deux sortes: ∎ Paramètres scalaires: □ L’identificateur minuscule doit comporter au moins un caractère □ Type: □ Type: INT, INT, BOOL, BOOL, paramètre paramètre ensemble ensemble de de la la machine machine ∎ Paramètres ensembles: □ L’identificateur minuscules ne doit pas contenir de caractères □ Exemples MACHINE MACHINE MACHINE carrefour réservation(Maxi) pile(ELEMENT)... ... CONSTRAINTS Maxi NAT... 17 Les clauses d’une machine abstraite L’en-tête □ La clause CONSTRAINTS ∎ Cette clause doit apparaître si la machine possède des paramètres scalaires formels ∎ Permet de typer les paramètres scalaires formels de la machine abstraite et d’exprimer des propriétés propriétés complémentaires complémentaires sur sur ces ces paramètres paramètres ∎ Exemple: 18 Les clauses d’une machine abstraite Les données □ Les décrites données au moyen d'une des machine clauses abstraite suivantes: sont SETS Déclaration des ensembles abstraits et énumérés CONSTANTS Définition Définition des des constantes constantes PROPERTIES Propriétés sur les constantes VARIABLES Déclaration des variables (idem attributs d’une classe) INVARIANT Typage et propriété des variables 19 Les clauses d’une machine abstraite Les données La clause SETS □ elle représente les ensembles introduits par la machine: ∎ soit des ensembles abstraits: □ définis définis par par leurs leurs noms noms □ utilisés pour désigner des objets dont on ne veut pas définir la structure au niveau de la spécification. □ Tout ensemble abstrait est implicitement fini et non vide ∎ soit des ensembles énumérés définis par leurs noms et la liste de leurs éléments. 20 Les clauses d’une machine abstraite Les données □ Exemple: POSITION est un ensemble abstrait MARCHE et DIRECTION sont des ensembles énumérés 21 Les clauses d’une machine abstraite Les données □ La clause CONSTANTS ∎ On peut aussi utiliser CONCRETE_CONSTANTS ∎ Déclare une liste de constantes concrètes (implémentable directement dans un langage informatique) informatique) ∎ Chaque constante doit être typé dans la clause PROPERTIES □ La clause PROPERTIES ∎ définit un prédicat qui type les constantes de la machine abstraite et qui définit leurs propriétés. 22 Les clauses d’une machine abstraite Les données □ Exemple 1 MACHINE MA1 CONSTANTS PosMin, PosMax □ Exemple2 MACHINE MA2 CONSTANTS PosMax Cte1, PROPERTIES PosMin INT PosMax NAT ... END Cte2 PROPERTIES Cte1 INT Cte2 NAT (Cte1 < 0 Cte2 = 0) ... END 23 Les clauses d’une machine abstraite Les données La clause VARIABLES ∎ Elle introduit la liste des variables de la machine. ∎ Ces variables représentent l ́état de la machine. ∎ Les variables sont les seules objets qui peuvent être être modifiés modifiés directement directement dans dans l'initialisation l'initialisation et et les opérations de la machine. ∎ Cette clause peut être absente si la machine n'a pas de variables. ∎ Cette clause doit être accompagnée des clauses INVARIANT et INITIALISATION. 24 Les clauses d’une machine abstraite Les données La clause INVARIANT □ regroupe un ensemble de prédicats qui: ∎ permettent de typer les variables ∎ définissent vérifier l'état les de propriétés la machine des à tout variables moment que doit □ □ Il Il variable(s) est est fondamental fondamental soit munie qu’une qu’une d’un machine machine invariant. avec avec 25 □ Exemple 1 MACHINE MA VARIABLES var1, var2, var3 INVARIANT var1 NAT var2 var2 BOOL BOOL var3 INT (var1 > var3 var2 = TRUE) INITIALISATION var1:=2|| var2:=TRUE|| var3:=-1 ... END Les clauses d’une machine abstraite Les données Invariant variables: de typage des □ Var1 naturel, booléen entier entier est relatif. relatif. var2 et un var entier est 3 est un un Propriété sur les variables □ Var1 strictement var2 doit doit être être à var3 vrai supérieur et 26 Les clauses d’une machine abstraite Les données □ Exemple2 MACHINE Chaudière SETS ETATS = {activé, désactivé} VARIABLES VARIABLES T, Alarme INVARIANT T ∈ NAT ∧ Alarme ∈ ETATS ∧ (T > 130) ⇔ (Alarme = activé) ... END 27 Les clauses d’une machine abstraite Les données □ Exemple3: Machine sans variables MACHINE Calculatrice CONSTANTS min_ent, max_ent, ENTIER PROPERTIES PROPERTIES min_ent = -2 31 max_ent = 2 31 - 1 ENTIER = min_ent .. max_ent ... END 28 Synthèse 29 Les clauses d’une machine abstraite La partie dynamique □ Composée des clauses suivantes: INITIALISATION Définition de la valeur initiale des variables OPERATIONS OPERATIONS Déclaration des opérations 30 Les clauses d’une machine abstraite La partie dynamique La clause INITIALISATION □ Permet d’attribuer une valeur initiale à chaque variable propre à la machine. □ L’initialisation □ L’initialisation doit doit satisfaire satisfaire l'invariant l'invariant de la machine. □ Clause obligatoire si la clause VARIABLE est présente: toute variable propre à la machine doit être initialisée. 31 Les clauses d’une machine abstraite La partie dynamique □ Exemple MACHINE MA VARIABLES var1, var2 INVARIANT var1 var1 NAT NAT var2 INT (var1 > var2) INITIALISATION var1, var2:=2,-1; ... END 32 Les clauses d’une machine abstraite Les opérations □ La opérations clause OPERATIONS d’une machine permet de définir les □ Une opération est composée de: ∎ Une en-tête: un nom et des paramètres (u et w) s’il y en a ∎ ∎ Une Une pré-condition pré-condition (Q) (Q) ∎ Une transformation (V) □ Définit le comportement de l’opération vis à vis de l’état de la machine ➢ Une transformation des données internes et une affectation de valeurs aux paramètres de sortie u← O (w) = PRE Q THEN V END en-tête pré-condition transformation 33 Les clauses d’une machine abstraite Les opérations Exemple MACHINE Calculatrice CONSTANTS min_ent, max_ent, ENTIER PROPERTIES min_ent = -2 31 ∧ ∧ max_ent = 2 31 - 1 ∧ ∧ ENTIER ENTIER = = min_ent min_ent .. .. max_ent max_ent OPERATIONS ecrire_nombre (a) ... ; a ← lire_nombre ... ; c ← plus (a, b) ... ; c ← moins (a, b) ... ; c ← mult (a, b) ... ; r, o ‹ — add (a, b) ... ; END 34 Les clauses d’une machine abstraite Les opérations □ Une opération peut être paramétrée en entrée (w) et en sortie (u) par une liste de paramètres. □ Les paramètres en entrée w sont typés explicitement dans la pré-condition Q de l’opération. □ La pré-condition Q permet aussi de définir les conditions de fonctionnement de l’opération □ Les paramètres en sortie u sont typés implicitement en fonction des types des expressions définissant la valeur de ces paramètres dans V u← O (w) = PRE Q THEN V END en-tête pré-condition transformation 35 Les clauses d’une machine abstraite Les opérations □ La définition des opérations s’appuie sur le langage des substitutions généralisées □ La transformation de base est la substitution simple devient égal , notée := □ Les autres transformations permettent de modéliser modéliser le le résultat résultat de de tous tous les les changements changements d’états réalisables : ∎ Choix borné ∎ Substitution gardée ∎ Choix non borné ∎ Etc. 36 Les clauses d’une machine abstraite Les opérations Exemple1 MACHINE Chaudière SETS ETATS = {activé, désactivé} VARIABLES T, Alarme INVARIANT T T ∈ ∈ NAT NAT ∧ ∧ Alarme ∈ ETATS ∧ (T > 130) ⇔ (Alarme = activé ) INITIALISATION T:=0||Alarme:=désactivé OPERATIONS changerT (v) = PRE v ∈ NAT ∧ v ≤ 130 THEN T := v END ... 37 Les clauses d’une machine abstraite Les opérations Exemple2 MACHINE Calculatrice CONSTANTS min_ent, max_ent, ENTIER PROPERTIES min_ent = -2 31 ∧ max_ent = 2 31 - 1 ∧ r, o ‹ — add (a, b) = PRE a ∈ ENTIER ∧ b ∈ ENTIER THEN IF a + b ∈ ENTIER ∧ max_ent = 2 - 1 ∧ ENTIER = min_ent .. max_ent OPERATIONS r ‹ — plus (a, b) = PRE a ∈ ENTIER ∧ b ∈ ENTIER ∧ a + b ∈ ENTIER THEN r := a + b END ; IF a + b ∈ ENTIER THEN r := a + b ||o := FALSE ELSE o := TRUE END END END 38 Les clauses d’une machine abstraite Les opérations Exercice MACHINE reservation ... OPERATIONS reserver(nbPlaces)= PRE nbPlaces ∈ NAT1 ∧ nbPlaces ≤ nbPlacesLibres THEN nbPlacesLibres := nbPlacesLibres-nbPlaces END END 39 Exercice: Réservation □ On souhaite spécifier un système de réservation de places sur un vol limité à maxi places. Les opérations à écrire sont: ∎ Réserver: permet de réserver une place si c’est possible. ∎ Libérer: permet d’annuler la réservation d’une place. □ Remarque: la gestion des numéros de places n’est pas demandée. Travail demandé: 1. Spécifier les données de la machine B associée à ce système 2. Décrire l’invariant de ce modèle 3. Donner la machine résultante 40 Solution MACHINE Reservation1 CONSTANTS maxi PROPERTIES maxi NAT VARIABLES NbPlLib NbPlLib INVARIANT NbPlLib 0..maxi INITIALISATION NbPlLib:=maxi OPERATIONS reserver= PRE NbPlLib ≠ 0 THEN NbPlLib:=NbPlLib-1 END; liberer= PRE NbPlLib ≠ maxi THEN NbPlLib:=NbPlLib+1 END END 41 Exercice : Réservation Modifier la machine précédente pour: ∎ Permettre à la machine de recevoir maxi en paramètre ∎ Améliorer «échec » ou les « opérations: succès ». elles doivent retourner en résultat 2. Ecrire libérer une un nombre nouvelle de machine places donné qui permet en paramètre. de réserver et 3. 3. Ecrire Ecrire places places une une par par nouvelle nouvelle leurs leurs numéros. numéros. machine machine permettant permettant de de gérer gérer les les 42 Solution 1/ MACHINE Reservation2(maxi) CONSTRAINTS maxi ∈ NAT SETS RESULTAT={échec, succès} VARIABLES VARIABLES NbPlLib INVARIANT NbPlLib ∈ 0..maxi INITIALISATION NbPlLib:=maxi OPERATIONS Res <-- reserver= IF NbPlLib ≠ 0 THEN NbPlLib:=NbPlLib-1 || Res:=succès ELSE Res:= échec END; Res <-- liberer= IF NbPlLib ≠ maxi THEN NbPlLib:=NbPlLib+1 || Res := succès ELSE Res:= échec END END 43 Solution 2/ MACHINE Reservation3(maxi) CONSTRAINTS maxi ∈ NAT SETS RESULTAT={échec, succès} VARIABLES NbPlLib INVARIANT NbPlLib NbPlLib ∈ ∈ 0..maxi 0..maxi INITIALISATION NbPlLib:=maxi OPERATIONS Res <-- reserver(nb) = PRE nb ∈ NAT THEN IF NbPlLib >= nb THEN NbPlLib:=NbPlLib-nb || Res:=succès ELSE Res:= échec END END; Res <-- liberer(nb)= PRE nb ∈ NAT THEN IF NbPlLib+nb <= maxi THEN NbPlLib:=NbPlLib+nb || Res := succès ELSE Res:= échec END END END Solution 3/ MACHINE Reservation4 CONSTANTS maxi, PLACES PROPERTIES maxi ∈ NAT ∧ PLACES = 0..maxi SETS RESULTAT={échec, succès} VARIABLES OCCUPES OCCUPES INVARIANT OCCUPES ⊆ PLACES INITIALISATION OCCUPES:=∅ OPERATIONS place <-- reserver = PRE PLACES ≠ OCCUPES THEN ANY pp WHERE pp ∈ PLACES - OCCUPES THEN OCCUPES:=OCCUPES ∪ {pp}||place:=pp END END; liberer(place)= PRE place ∈ PLACES ∧ place ∈ OCCUPES THEN OCCUPES:=OCCUPES - {place} END END 45 Exercice □ On souhaite spécifier le comportement d’un système de contrôle d’une barrière d’un passage à niveau en utilisant la méthode B. □ La barrière est initialement relevée. Si un train arrive alors elle est baissée et elle reste dans cet état tant qu’il ya des trains qui arrivent. Elle est relevée si le dernier train quitte la section. 1) 1) Spécifier Spécifier les les données données du du modèle modèle B B associé associé à à ce ce système système 2) Décrire les invariants de ce modèle 3) Donner le modèle résultant □ Remarque : Il est possible de commencer par construire un automate associé à ce contrôleur et, par la suite, donner le modèle résultant. 46 Solution MACHINE barriere SETS etat={relevée, baissée} VARIABLES barrier, NbT INVARIANT barrier∈etat ∈ ∧ ∧ NbT ∈ ∈ NAT ∧ ∧ ((NbT=0 ⇒ ⇒ barrier=relevée) or (NbT>0 ⇒ ⇒ barrier=baissée)) barrier=baissée)) INITIALISATION barrier:=relevée||NbT:=0 OPERATIONS arriveeTrain= IF barrier= relevée THEN NbT:=NbT+1 ||barrier:=baissée ELSE NbT:=NbT+1 END; passageTrain= PRE barrier=baissée THEN IF NbT>1 THEN NbT:=NbT-1 ELSE NbT:=0||barrier:=relevée END END END 47 Autres clauses □ Clause ASSERTIONS: liste de prédicats appelés assertions portant sur les variables. Ce sont des résultats intermédiaires déduits de l’invariant susceptibles d’aider la preuve. □ Clauses SEES, USES, INCLUDES, IMPORTS, etc. (Pour la modularité) Autres clauses La clause DEFINITIONS □ Permet de définir une liste d'abréviations pour un prédicat, une expression ou une substitution: ∎ À travers des déclarations explicites ∎ À partir de fichiers de définitions à inclure □ Les définitions sont locales à la machine où elles sont définies définies et et peuvent peuvent être être utilisées utilisées même même dans dans le le texte texte qui précède leur déclaration. □ Les définitions peuvent dépendre d’autres définitions mais ne doivent pas conduire à des dépendances cycliques. □ Les définitions explicites peuvent être paramétrées 49 Exemple1 Autres clauses La clause DEFINITIONS ... DEFINITIONS Def1 == A = jaune ∧ B = jaune; Def2(aa, bb=rouge); bb) == (aa = rouge ∧ bb ≠ rouge) ∨ (aa ≠ rouge ∧ Def3 Def3 == == Def2(A, Def2(A, B)B) CONSTANTS ... □ Le corps de la définition def1 est " A = jaune ∧ B = jaune ". □ Def2 est une définition paramétrée □ Def3 est définie par appel à Def2 50 Les obligations de preuve preuve 5151 Les obligations de preuve (Preuve de cohérence) □ Une machine abstraite est dite cohérente lorsque l’initialisation et chaque opération préservent les propriétés invariantes. □ La dernière étape de la spécification consiste à prouver prouver la la cohérence cohérence de de chaque chaque machine machine abstraite □ Une obligation de preuve est une formule mathématique à démontrer afin d'assurer qu'un composant B est correct. □ Un point fort de B est la génération automatique des obligations de preuve 52 Les obligations de preuve □ Toutes les obligations de preuve ont la structure suivante : H P où P et H sont des prédicats. □ □ Cette Cette formule formule signifie signifie qu'il qu'il faut faut démontrer le but P sous l'hypothèse H, H étant généralement une conjonction de prédicats. Les obligations de preuve □ Les machine principalement obligations abstraite : de concernent preuve relatives à une ∎ la doit correction établir l'invariant de l'initialisation de la machine; : l'initialisation ∎ ∎ la la doivent doivent correction correction préserver préserver des des l'invariant; l'invariant; opérations opérations : : les les opérations opérations Les obligations de preuve Correction de l’initialisation Les hypothèses de la correction de l'initialisation sont : □ Contraintes des paramètres de la machine abstraite □ Propriétés des constantes de la machine abstraite, Sous Sous ces ces hypothèses, hypothèses, le le but but à à démontrer démontrer est est : : □ L'invariant de la machine abstraite après application de l’initialisation Les obligations de preuve Correction des opérations Les hypothèses sont: □ Contraintes des paramètres de la machine abstraite □ Propriétés des constantes de la machine abstraite, □ □ Invariants Invariants et et assertions assertions de de la la machine machine abstraite, abstraite, □ La pré-condition de l’opération Sous ces hypothèses, le but à démontrer est : □ L'invariant de la machine abstraite, après application de la substitution définissant l’opération. Les obligations de preuve □ Soient S une substitution et P un prédicat: ∎ La prédicat notation P » P se lit « la substitution S établit le ∎ transformation P représente de le P prédicat par la substitution obtenu après S. □ Chaque précisant précisant application quelconque. substitution quel quel de la est est substitution le le généralisée prédicat prédicat à obtenu obtenu un se prédicat définit après après en □ Exemple pour la substitution simple: ∎ I occurrences représente libres de I x dans sont laquelle remplacées toutes par les E. 58 Les obligations de preuve □ Le prédicat P c’est l’invariant I et la substitution S est V, on obtient les obligations de preuve suivantes: ∎ Obligation de preuve de l’initialisation: démontrer démontrer que que le le prédicat prédicat H H ⇒ I ⇒ I est valide ∎ Obligation de preuve pour une opération: démontrer que le prédicat H ⇒ I est valide 59 MACHINE M VARIABLES V INVARIANT I INITIALISATION Init OPERATIONS u ← O(W) = PRE Q THEN V END END Exemple Les obligations de preuve Obligation de preuve pour l’initialisation: Aucun hypothèse But à prouver: I après Init (est ce que l’initialisation établit l’invariant?) I Obligation de preuve pour l’opération O: On On prouve prouve que que lorsque la machine est dans un état correct: les propriétés invariantes I sont supposées vérifiées lorsque l’opération est appelée avec la pré-condition Q: Q est supposée vérifiée alors sa transformation V amène la machine dans un état correct: → un état qui satisfait l’invariant I I ∧ Q ⇒ I après V I ∧ Q ⇒ I 60 MACHINE M VARIABLES V INVARIANT I INITIALISATION Init OPERATIONS u ← O(W) = PRE Q THEN V END END Exemple1 Les obligations de preuve Les obligations de preuve pour la machine M: I I ∧ Q ⇒ I 61 Les obligations de preuve Exemple2 MACHINE M(u) CONSTRAINTS C CONSTANTS c Obligation de preuve pour l’initialisation: C ∧R ⇒ I Obligation Obligation de de preuve preuve pour pour PROPERTIES l’opération O: C ∧R ∧ I ∧ P ⇒ I R VARIABLES x INVARIANT I INITIALISATION U OPERATIONS r op(p) = PRE P THEN K END; Exercice □ Écrire les obligations de preuve de la machine réservation 63 Éléments de modélisation en B □ Langage ensembliste: pour décrire le modèle de données □ Logique des prédicats du premier ordre ordre pour pour décrire décrire les les propriétés propriétés □ Langage des substitutions généralisées pour décrire les actions 64 Les substitutions généralisées généralisées 6565 Introduction □ Les substitutions généralisées sont utilisées pour décrire le corps de l’initialisation et des opérations d’un composant (clauses INITIALISATION et et OPERATIONS) OPERATIONS) □ La sémantique du langage des substitutions est définie par un calcul des substitutions qui permet d’effectuer les évaluations des obligations de preuve 66 Les substitutions généralisées Non déterminisme □ Une substitution possède un comportement non déterministe si elle décrit plusieurs comportements possibles sans préciser lequel lequel sera sera effectivement effectivement choisi. choisi. □ En B, les substitutions des machines et des raffinements peuvent être non déterministes. □ Le non déterminisme décroît lors du raffinement. 67 Les substitutions généralisées 68 Substitution devient égal □ Soit x une variable, e une expression et P un prédicat, alors : [ x := e ] P est le prédicat obtenu en remplaçant toutes les occurrences libres de x dans P par e. Règle de typage: □ Dans la substitution x := e, x et e doivent être du même type T. □ Dans la substitution x1,.., xn := e1, ..., en, chaque xi doit être du même type que ei. 69 Substitution devient égal □ Une prédicat variable ou dans est une dite expression libre dans si: un ∎ Elle est présente dans la formule et ∎ Elle sont sont quantificateurs quantifiée est pas pas présente sous sous de même la la introduisant portée portée dans nom. des de de sous certains certains une formules variable qui ne □ Exemple: Soit le prédicat: y est-elle libre? libre? n est-elle libre? x est-elle 70 Exemple de calcul: OP de reserver MACHINE reservation VARIABLES nbPlacesLibres INVARIANT nbPlacesLibres ∈ 0..100 ... OPERATIONS I ∧ Q ⇒ I devient: (nbPlacesLibres ∈ 0..100 ∧ nbPlaces ∈ NAT1 ∧ nbPlaces ≤nbPlacesLibres) ⇒ OPERATIONS reserver(nbPlaces)= (nbPlacesLibres ∈ 0..100) 2. (nbPlacesLibres ∈ 0..100 ∧ PRE nbPlaces ∈ NAT1 ∧ nbPlaces ≤ nbPlacesLibres THEN nbPlacesLibres-nbPlaces nbPlacesLibres := END END ``` (nbPlacesLibres ∈ 0..100 ∧ nbPlaces ∈ NAT1 ∧ nbPlaces ≤nbPlacesLibres) ⇒ (nbPlacesLibres-nbPlaces ∈ 0..100) 71 □ x, y := E, F Sémantique I ⇔ I z étant une variable distincte de x et y et non libre dans I Substitution simultanée □ Correspond à l’exécution simultanée de deux substitutions Deux syntaxes: □ x := E | | y := F 72 Substitution simultanée ∎ Exemple: permutation de 2 variables (x < y) (x < y) y] (x (x < < z) z) (y < z) (y < x) 73 Substitution choix borné □ Permet de définir un nombre fini de comportements possibles sans préciser lequel sera effectivement choisi (non déterministe). □ □ n'est n'est pas pas une une substitution substitution d'implémentation d'implémentation □ Syntaxe ∎ CHOICE S1 OR ... OR Sn END ∎ S1, ..., Sn des substitutions (avec n ≥ 2) □ Sémantique I ⇔ I ∧ ... ∧ I 74 Substitution choix borné □ Exemple : Définition des résultats de l’examen du permis de conduire CHOICE résultat := réussite || permis := permis U {candidat} OR résultat := échec END END □ Calculer : (permis PERS-MAJEUR) 75 Select (Garde et Choix Borné) □ La gardes d’exécution substitution qui définissent de l’instruction. SELECT les permet conditions d’exprimer des □ Syntaxe Sémantique I) ∧ WHEN WHEN ... WHEN SE] Q2 Q2 Qn THEN THEN THEN S2 S2 Sn (Qn ((¬Q1∧¬Q2∧...∧¬Qn) ⇒ (Q2 (Q2 ... ⇒ ⇒ I) ∧ I) ∧ ⇒ I) ∧ I) □ Les ce cas gardes le comportement peuvent ne pas est être non-déterministe. disjointes, dans 76 Select (Garde et Choix Borné) □ Exemple SELECT x ≥ 0 THEN y := x 2 WHEN WHEN x x ≤ ≤ 0 0 THEN THEN y := - x 2 END 77 Substitution identité □ La substitution identité Skip ne modifie pas le prédicat sur lequel elle est appliquée. □ Elle est notamment utilisée pour décrire décrire que que certaines certaines branches branches d’une d’une substitution IF, CASE ou SELECT ne modifient pas les variables. Sémantique: I ⇔ I 78 Condition par Cas □ La comportements expression. substitution CASE possibles permet en fonction de définir de différents la valeur d’une □ Syntaxe: CASE EITHER Sn] S2 S1 END □ Chaque non booléen). vide branche de constantes EITHER littérales et OR est (entier, constituée énuméré, d’une liste □ Les même L1, type .. , Ln que doivent E. être disjoints (déterminisme) et de □ Si skip. le ELSE est absent, l’échec des Li réalise la substitution 79 Condition par Cas Sémantique: CASE E OF EITHER L1 THEN S1 E∈{L1} I ∧ I ∧ ... ... ... ... OR Ln THEN Sn] E∈{Ln} I ∧ E∉{L1,L2...Ln} I (en l’absence de ELSE END SKIP ) 80 Condition par Cas □ Exemple: MACHINE triangle SETS TRIANG_TYPE isosceles, no_triangle} equilateral, = {scalene, OPERATIONS IF s1+s2 ≤ s1 or ≤ s1+s3 s3 or s2+s3 ≤ s2 THEN no_triangle tr_type := ELSE CASE OF card({s1, s2, s3}) OPERATIONS tr_type s3) = <-- classify(s1, s2, PRE s1 ∈ INT ∧ s1 ≠0 ∧ EITHER EITHER tr_type:=equilateral 1 1 THEN THEN OR 2 tr_type:=isosceles THEN OR 3 tr_type:=scalene THEN s2 ∈ INT ∧ s2 ≠0 ∧ END END s3 ∈ INT ∧ s3 ≠0 END THEN END END 81 Substitution conditionnelle IF □ La substitution conditionnelle IF est définie selon plusieurs formes : 1. IF P THEN S END Sémantique I S]I P P I I 2. IF P1 THEN S1 ELSE T END Sémantique I ⇔ (P1 I) ∧ (¬P1 I) 82 Substitution conditionnelle IF Forme générale du IF Syntaxe: Sémantique: IF P1 THEN S1 P1 ⇒ ⇒ I ∧ I I ∧ ∧ ... ⇔ ... ELSIF Pn THEN Sn] ¬P1∧¬P2∧...¬Pn-1∧Pn ⇒ I ∧ ¬P1∧¬P2∧...¬Pn-1∧¬Pn ⇒ I END 83 télécharger gratuitement La méthode B AMN(Abstract Machine Notation) "Génie Logiciel II"

Page 1 sur 1Lecteur de document UniversityLib

La méthode B AMN(Abstract Machine Notation) "Génie Logiciel II"

École Nationale des Sciences de l'Informatique (ENSI) · Informatique · exam

Browse all génie logiciel documents

Cours "Génie Logiciel II" Chapitre 2: La méthode B AMN(Abstract AMN(Abstract Machine Machine Notation) Niveau: II2 Enseignante: Rim DRIRA [email protected] AU: 2017/2018 1 Chapitre2: La méthode B Plan ∎ Présentation ∎ Notion de machine abstraite ∎ Les clauses d’une machine abstraite ∎ ∎ Les Les obligations obligations de de preuve preuve ∎ Définition et calcul des substitutions généralisées ∎ Notation de modélisation des données ∎ Le processus de raffinement ∎ Les obligations de preuve du raffinement ∎ La modularité 2 Présentation de B et de ses ses concepts concepts de de base base 3 Historique □ Née dans les années 80 □ Fondateur: Jean-Raymond Abrial (un informaticien français ) □ Livre de référence: « The B Book » [1] □ □ Le Le choix choix du du nom nom B B est est une une sorte sorte d'hommage aux membres du groupe BOURBAKI. ∎ C’est un groupe de mathématiciens français qui a entrepris en 1939 une refonte des mathématiques en les prenant à leur point de départ logique. 4 Présentation □ B est issue de Z et VDM. □ La particularité de B : établir une chaîne de production qui va des spécifications spécifications au au code code source source associé. associé. □ B est basée sur la théorie des ensembles et la logique du premier ordre 5 Présentation □ Les logiciels conçus avec la méthode B fonctionnent conformément à leurs spécifications ∎ Les propriétés sont exprimées par des invariants invariants et et vérifiées vérifiées par par preuves preuves formelles. □ Un exemple industriel de l’utilisation de la méthode B: le pilote automatique embarqué (PAE) de METEOR de la ligne 14 du métro parisien 6 PA: propriété abstraite PR: propriété de raffinement raffinement Preuve du raffinement Raffinement Raffinement 2 Méthode B Raffinement 2 Raffinement n-1 Raffinement n Code Modèle abstrait Raffinement 1 Preuve PA Preuve PR 1 Preuve Preuve PR PR 2 Preuve PR n-1 Preuve PR n 7 Documentation et outillage □ Documentation disponible ∎ http://www .dmi.usher b.ca/~frap pier/igl50 1/ref/B/ Ma nrefb.pdf □ Outils en licence libre ∎ Exemple: Atelier B (http://www.atelierb.eu/telechargement/) 8 Atelier B □ Développé par la société ClearSy, □ Outil qui permet une utilisation opérationnelle de la méthode formelle B pour des développements de logiciels prouvés prouvés □ Disponible en deux versions: ∎ une version communautaire accessible à tous sans limitation, ∎ une version maintenue accessible aux possesseurs d’un contrat de maintenance. http://www.atelierb.eu 9 Atelier B Source: http://www.atelierb.eu 10 Notion de machine abstraite □ Dans abstraite B, un qui composant contient: logiciel est appelé machine ∎ Des données ∎ Des opérations □ Connue Notation) aussi sous l’acronyme AMN (Abstract Machine □ □ Avec Avec B, B, ∎ On spécifie ∎ On prouve ∎ On raffine ∎ On code Une (ou plusieurs) machine(s) abstraite(s) □ Cette notion est proche de: ∎ Type abstrait, Module, Classe, Composant 12 Quelques remarques □ Les distinguées. lettres minuscules et majuscules sont □ Les deux "/*" commentaires commentaires commentaires et caractères par les deux "*/". "*/". de sont début caractères délimités de commentaire de par fin les de □ Un lettres, "_". lettre. identificateur Le premier de chiffres caractère est ou une du caractère séquence doit être une souligné de ∎ Tout doit identificateur: variable, respecter ce qu’on d’une lui les le constante, nom attribue règles d’une de nous etc. définition machine, même d’un d’une des noms 13 Principales clauses MACHINE En-tête Nom de la machine abstraite (idem nom de la classe) CONSTRAINTS Contraintes sur les paramètres d’une machine s’il y en a SETS Déclaration des ensembles abstraits et énumérés CONSTANTS Définition des constantes Partie PROPERTIES Propriétés sur les constantes - Une clause ne doit pas apparaître plus qu’une fois Partie - - L’ordre L’ordre des des clauses clauses n’est n’est pas pas imposé imposé Statique Partie dynamique Propriétés sur les constantes VARIABLES Déclaration des variables (idem attributs d’une classe) DEFINITIONS expression Contient une ou liste une d'abréviations substitution. pour un prédicat, une INVARIANT Typage et propriété des variables INITIALISATION Définition constructeur) de la valeur initiale des variables (idem OPERATIONS Déclaration des opérations (idem méthodes) END 15 Les clauses d’une machine abstraite L’en-tête □La partie en-tête contient: Nom de la machine Paramètres de la machine (pour la généricité) Contraintes sur les paramètres □Clauses □Clauses MACHINE Nom formels) de la machine abstraite (paramètres CONSTRAINTS machine Contraintes s’il y sur en a les paramètres d’une 16 Les clauses d’une machine abstraite L’en-tête □ Il formels est optionnel qu’une machine possède des paramètres □ Les paramètres d’une machine sont de deux sortes: ∎ Paramètres scalaires: □ L’identificateur minuscule doit comporter au moins un caractère □ Type: □ Type: INT, INT, BOOL, BOOL, paramètre paramètre ensemble ensemble de de la la machine machine ∎ Paramètres ensembles: □ L’identificateur minuscules ne doit pas contenir de caractères □ Exemples MACHINE MACHINE MACHINE carrefour réservation(Maxi) pile(ELEMENT)... ... CONSTRAINTS Maxi NAT... 17 Les clauses d’une machine abstraite L’en-tête □ La clause CONSTRAINTS ∎ Cette clause doit apparaître si la machine possède des paramètres scalaires formels ∎ Permet de typer les paramètres scalaires formels de la machine abstraite et d’exprimer des propriétés propriétés complémentaires complémentaires sur sur ces ces paramètres paramètres ∎ Exemple: 18 Les clauses d’une machine abstraite Les données □ Les décrites données au moyen d'une des machine clauses abstraite suivantes: sont SETS Déclaration des ensembles abstraits et énumérés CONSTANTS Définition Définition des des constantes constantes PROPERTIES Propriétés sur les constantes VARIABLES Déclaration des variables (idem attributs d’une classe) INVARIANT Typage et propriété des variables 19 Les clauses d’une machine abstraite Les données La clause SETS □ elle représente les ensembles introduits par la machine: ∎ soit des ensembles abstraits: □ définis définis par par leurs leurs noms noms □ utilisés pour désigner des objets dont on ne veut pas définir la structure au niveau de la spécification. □ Tout ensemble abstrait est implicitement fini et non vide ∎ soit des ensembles énumérés définis par leurs noms et la liste de leurs éléments. 20 Les clauses d’une machine abstraite Les données □ Exemple: POSITION est un ensemble abstrait MARCHE et DIRECTION sont des ensembles énumérés 21 Les clauses d’une machine abstraite Les données □ La clause CONSTANTS ∎ On peut aussi utiliser CONCRETE_CONSTANTS ∎ Déclare une liste de constantes concrètes (implémentable directement dans un langage informatique) informatique) ∎ Chaque constante doit être typé dans la clause PROPERTIES □ La clause PROPERTIES ∎ définit un prédicat qui type les constantes de la machine abstraite et qui définit leurs propriétés. 22 Les clauses d’une machine abstraite Les données □ Exemple 1 MACHINE MA1 CONSTANTS PosMin, PosMax □ Exemple2 MACHINE MA2 CONSTANTS PosMax Cte1, PROPERTIES PosMin INT PosMax NAT ... END Cte2 PROPERTIES Cte1 INT Cte2 NAT (Cte1 < 0 Cte2 = 0) ... END 23 Les clauses d’une machine abstraite Les données La clause VARIABLES ∎ Elle introduit la liste des variables de la machine. ∎ Ces variables représentent l ́état de la machine. ∎ Les variables sont les seules objets qui peuvent être être modifiés modifiés directement directement dans dans l'initialisation l'initialisation et et les opérations de la machine. ∎ Cette clause peut être absente si la machine n'a pas de variables. ∎ Cette clause doit être accompagnée des clauses INVARIANT et INITIALISATION. 24 Les clauses d’une machine abstraite Les données La clause INVARIANT □ regroupe un ensemble de prédicats qui: ∎ permettent de typer les variables ∎ définissent vérifier l'état les de propriétés la machine des à tout variables moment que doit □ □ Il Il variable(s) est est fondamental fondamental soit munie qu’une qu’une d’un machine machine invariant. avec avec 25 □ Exemple 1 MACHINE MA VARIABLES var1, var2, var3 INVARIANT var1 NAT var2 var2 BOOL BOOL var3 INT (var1 > var3 var2 = TRUE) INITIALISATION var1:=2|| var2:=TRUE|| var3:=-1 ... END Les clauses d’une machine abstraite Les données Invariant variables: de typage des □ Var1 naturel, booléen entier entier est relatif. relatif. var2 et un var entier est 3 est un un Propriété sur les variables □ Var1 strictement var2 doit doit être être à var3 vrai supérieur et 26 Les clauses d’une machine abstraite Les données □ Exemple2 MACHINE Chaudière SETS ETATS = {activé, désactivé} VARIABLES VARIABLES T, Alarme INVARIANT T ∈ NAT ∧ Alarme ∈ ETATS ∧ (T > 130) ⇔ (Alarme = activé) ... END 27 Les clauses d’une machine abstraite Les données □ Exemple3: Machine sans variables MACHINE Calculatrice CONSTANTS min_ent, max_ent, ENTIER PROPERTIES PROPERTIES min_ent = -2 31 max_ent = 2 31 - 1 ENTIER = min_ent .. max_ent ... END 28 Synthèse 29 Les clauses d’une machine abstraite La partie dynamique □ Composée des clauses suivantes: INITIALISATION Définition de la valeur initiale des variables OPERATIONS OPERATIONS Déclaration des opérations 30 Les clauses d’une machine abstraite La partie dynamique La clause INITIALISATION □ Permet d’attribuer une valeur initiale à chaque variable propre à la machine. □ L’initialisation □ L’initialisation doit doit satisfaire satisfaire l'invariant l'invariant de la machine. □ Clause obligatoire si la clause VARIABLE est présente: toute variable propre à la machine doit être initialisée. 31 Les clauses d’une machine abstraite La partie dynamique □ Exemple MACHINE MA VARIABLES var1, var2 INVARIANT var1 var1 NAT NAT var2 INT (var1 > var2) INITIALISATION var1, var2:=2,-1; ... END 32 Les clauses d’une machine abstraite Les opérations □ La opérations clause OPERATIONS d’une machine permet de définir les □ Une opération est composée de: ∎ Une en-tête: un nom et des paramètres (u et w) s’il y en a ∎ ∎ Une Une pré-condition pré-condition (Q) (Q) ∎ Une transformation (V) □ Définit le comportement de l’opération vis à vis de l’état de la machine ➢ Une transformation des données internes et une affectation de valeurs aux paramètres de sortie u← O (w) = PRE Q THEN V END en-tête pré-condition transformation 33 Les clauses d’une machine abstraite Les opérations Exemple MACHINE Calculatrice CONSTANTS min_ent, max_ent, ENTIER PROPERTIES min_ent = -2 31 ∧ ∧ max_ent = 2 31 - 1 ∧ ∧ ENTIER ENTIER = = min_ent min_ent .. .. max_ent max_ent OPERATIONS ecrire_nombre (a) ... ; a ← lire_nombre ... ; c ← plus (a, b) ... ; c ← moins (a, b) ... ; c ← mult (a, b) ... ; r, o ‹ — add (a, b) ... ; END 34 Les clauses d’une machine abstraite Les opérations □ Une opération peut être paramétrée en entrée (w) et en sortie (u) par une liste de paramètres. □ Les paramètres en entrée w sont typés explicitement dans la pré-condition Q de l’opération. □ La pré-condition Q permet aussi de définir les conditions de fonctionnement de l’opération □ Les paramètres en sortie u sont typés implicitement en fonction des types des expressions définissant la valeur de ces paramètres dans V u← O (w) = PRE Q THEN V END en-tête pré-condition transformation 35 Les clauses d’une machine abstraite Les opérations □ La définition des opérations s’appuie sur le langage des substitutions généralisées □ La transformation de base est la substitution simple devient égal , notée := □ Les autres transformations permettent de modéliser modéliser le le résultat résultat de de tous tous les les changements changements d’états réalisables : ∎ Choix borné ∎ Substitution gardée ∎ Choix non borné ∎ Etc. 36 Les clauses d’une machine abstraite Les opérations Exemple1 MACHINE Chaudière SETS ETATS = {activé, désactivé} VARIABLES T, Alarme INVARIANT T T ∈ ∈ NAT NAT ∧ ∧ Alarme ∈ ETATS ∧ (T > 130) ⇔ (Alarme = activé ) INITIALISATION T:=0||Alarme:=désactivé OPERATIONS changerT (v) = PRE v ∈ NAT ∧ v ≤ 130 THEN T := v END ... 37 Les clauses d’une machine abstraite Les opérations Exemple2 MACHINE Calculatrice CONSTANTS min_ent, max_ent, ENTIER PROPERTIES min_ent = -2 31 ∧ max_ent = 2 31 - 1 ∧ r, o ‹ — add (a, b) = PRE a ∈ ENTIER ∧ b ∈ ENTIER THEN IF a + b ∈ ENTIER ∧ max_ent = 2 - 1 ∧ ENTIER = min_ent .. max_ent OPERATIONS r ‹ — plus (a, b) = PRE a ∈ ENTIER ∧ b ∈ ENTIER ∧ a + b ∈ ENTIER THEN r := a + b END ; IF a + b ∈ ENTIER THEN r := a + b ||o := FALSE ELSE o := TRUE END END END 38 Les clauses d’une machine abstraite Les opérations Exercice MACHINE reservation ... OPERATIONS reserver(nbPlaces)= PRE nbPlaces ∈ NAT1 ∧ nbPlaces ≤ nbPlacesLibres THEN nbPlacesLibres := nbPlacesLibres-nbPlaces END END 39 Exercice: Réservation □ On souhaite spécifier un système de réservation de places sur un vol limité à maxi places. Les opérations à écrire sont: ∎ Réserver: permet de réserver une place si c’est possible. ∎ Libérer: permet d’annuler la réservation d’une place. □ Remarque: la gestion des numéros de places n’est pas demandée. Travail demandé: 1. Spécifier les données de la machine B associée à ce système 2. Décrire l’invariant de ce modèle 3. Donner la machine résultante 40 Solution MACHINE Reservation1 CONSTANTS maxi PROPERTIES maxi NAT VARIABLES NbPlLib NbPlLib INVARIANT NbPlLib 0..maxi INITIALISATION NbPlLib:=maxi OPERATIONS reserver= PRE NbPlLib ≠ 0 THEN NbPlLib:=NbPlLib-1 END; liberer= PRE NbPlLib ≠ maxi THEN NbPlLib:=NbPlLib+1 END END 41 Exercice : Réservation Modifier la machine précédente pour: ∎ Permettre à la machine de recevoir maxi en paramètre ∎ Améliorer «échec » ou les « opérations: succès ». elles doivent retourner en résultat 2. Ecrire libérer une un nombre nouvelle de machine places donné qui permet en paramètre. de réserver et 3. 3. Ecrire Ecrire places places une une par par nouvelle nouvelle leurs leurs numéros. numéros. machine machine permettant permettant de de gérer gérer les les 42 Solution 1/ MACHINE Reservation2(maxi) CONSTRAINTS maxi ∈ NAT SETS RESULTAT={échec, succès} VARIABLES VARIABLES NbPlLib INVARIANT NbPlLib ∈ 0..maxi INITIALISATION NbPlLib:=maxi OPERATIONS Res <-- reserver= IF NbPlLib ≠ 0 THEN NbPlLib:=NbPlLib-1 || Res:=succès ELSE Res:= échec END; Res <-- liberer= IF NbPlLib ≠ maxi THEN NbPlLib:=NbPlLib+1 || Res := succès ELSE Res:= échec END END 43 Solution 2/ MACHINE Reservation3(maxi) CONSTRAINTS maxi ∈ NAT SETS RESULTAT={échec, succès} VARIABLES NbPlLib INVARIANT NbPlLib NbPlLib ∈ ∈ 0..maxi 0..maxi INITIALISATION NbPlLib:=maxi OPERATIONS Res <-- reserver(nb) = PRE nb ∈ NAT THEN IF NbPlLib >= nb THEN NbPlLib:=NbPlLib-nb || Res:=succès ELSE Res:= échec END END; Res <-- liberer(nb)= PRE nb ∈ NAT THEN IF NbPlLib+nb <= maxi THEN NbPlLib:=NbPlLib+nb || Res := succès ELSE Res:= échec END END END Solution 3/ MACHINE Reservation4 CONSTANTS maxi, PLACES PROPERTIES maxi ∈ NAT ∧ PLACES = 0..maxi SETS RESULTAT={échec, succès} VARIABLES OCCUPES OCCUPES INVARIANT OCCUPES ⊆ PLACES INITIALISATION OCCUPES:=∅ OPERATIONS place <-- reserver = PRE PLACES ≠ OCCUPES THEN ANY pp WHERE pp ∈ PLACES - OCCUPES THEN OCCUPES:=OCCUPES ∪ {pp}||place:=pp END END; liberer(place)= PRE place ∈ PLACES ∧ place ∈ OCCUPES THEN OCCUPES:=OCCUPES - {place} END END 45 Exercice □ On souhaite spécifier le comportement d’un système de contrôle d’une barrière d’un passage à niveau en utilisant la méthode B. □ La barrière est initialement relevée. Si un train arrive alors elle est baissée et elle reste dans cet état tant qu’il ya des trains qui arrivent. Elle est relevée si le dernier train quitte la section. 1) 1) Spécifier Spécifier les les données données du du modèle modèle B B associé associé à à ce ce système système 2) Décrire les invariants de ce modèle 3) Donner le modèle résultant □ Remarque : Il est possible de commencer par construire un automate associé à ce contrôleur et, par la suite, donner le modèle résultant. 46 Solution MACHINE barriere SETS etat={relevée, baissée} VARIABLES barrier, NbT INVARIANT barrier∈etat ∈ ∧ ∧ NbT ∈ ∈ NAT ∧ ∧ ((NbT=0 ⇒ ⇒ barrier=relevée) or (NbT>0 ⇒ ⇒ barrier=baissée)) barrier=baissée)) INITIALISATION barrier:=relevée||NbT:=0 OPERATIONS arriveeTrain= IF barrier= relevée THEN NbT:=NbT+1 ||barrier:=baissée ELSE NbT:=NbT+1 END; passageTrain= PRE barrier=baissée THEN IF NbT>1 THEN NbT:=NbT-1 ELSE NbT:=0||barrier:=relevée END END END 47 Autres clauses □ Clause ASSERTIONS: liste de prédicats appelés assertions portant sur les variables. Ce sont des résultats intermédiaires déduits de l’invariant susceptibles d’aider la preuve. □ Clauses SEES, USES, INCLUDES, IMPORTS, etc. (Pour la modularité) Autres clauses La clause DEFINITIONS □ Permet de définir une liste d'abréviations pour un prédicat, une expression ou une substitution: ∎ À travers des déclarations explicites ∎ À partir de fichiers de définitions à inclure □ Les définitions sont locales à la machine où elles sont définies définies et et peuvent peuvent être être utilisées utilisées même même dans dans le le texte texte qui précède leur déclaration. □ Les définitions peuvent dépendre d’autres définitions mais ne doivent pas conduire à des dépendances cycliques. □ Les définitions explicites peuvent être paramétrées 49 Exemple1 Autres clauses La clause DEFINITIONS ... DEFINITIONS Def1 == A = jaune ∧ B = jaune; Def2(aa, bb=rouge); bb) == (aa = rouge ∧ bb ≠ rouge) ∨ (aa ≠ rouge ∧ Def3 Def3 == == Def2(A, Def2(A, B)B) CONSTANTS ... □ Le corps de la définition def1 est " A = jaune ∧ B = jaune ". □ Def2 est une définition paramétrée □ Def3 est définie par appel à Def2 50 Les obligations de preuve preuve 5151 Les obligations de preuve (Preuve de cohérence) □ Une machine abstraite est dite cohérente lorsque l’initialisation et chaque opération préservent les propriétés invariantes. □ La dernière étape de la spécification consiste à prouver prouver la la cohérence cohérence de de chaque chaque machine machine abstraite □ Une obligation de preuve est une formule mathématique à démontrer afin d'assurer qu'un composant B est correct. □ Un point fort de B est la génération automatique des obligations de preuve 52 Les obligations de preuve □ Toutes les obligations de preuve ont la structure suivante : H P où P et H sont des prédicats. □ □ Cette Cette formule formule signifie signifie qu'il qu'il faut faut démontrer le but P sous l'hypothèse H, H étant généralement une conjonction de prédicats. Les obligations de preuve □ Les machine principalement obligations abstraite : de concernent preuve relatives à une ∎ la doit correction établir l'invariant de l'initialisation de la machine; : l'initialisation ∎ ∎ la la doivent doivent correction correction préserver préserver des des l'invariant; l'invariant; opérations opérations : : les les opérations opérations Les obligations de preuve Correction de l’initialisation Les hypothèses de la correction de l'initialisation sont : □ Contraintes des paramètres de la machine abstraite □ Propriétés des constantes de la machine abstraite, Sous Sous ces ces hypothèses, hypothèses, le le but but à à démontrer démontrer est est : : □ L'invariant de la machine abstraite après application de l’initialisation Les obligations de preuve Correction des opérations Les hypothèses sont: □ Contraintes des paramètres de la machine abstraite □ Propriétés des constantes de la machine abstraite, □ □ Invariants Invariants et et assertions assertions de de la la machine machine abstraite, abstraite, □ La pré-condition de l’opération Sous ces hypothèses, le but à démontrer est : □ L'invariant de la machine abstraite, après application de la substitution définissant l’opération. Les obligations de preuve □ Soient S une substitution et P un prédicat: ∎ La prédicat notation P » P se lit « la substitution S établit le ∎ transformation P représente de le P prédicat par la substitution obtenu après S. □ Chaque précisant précisant application quelconque. substitution quel quel de la est est substitution le le généralisée prédicat prédicat à obtenu obtenu un se prédicat définit après après en □ Exemple pour la substitution simple: ∎ I occurrences représente libres de I x dans sont laquelle remplacées toutes par les E. 58 Les obligations de preuve □ Le prédicat P c’est l’invariant I et la substitution S est V, on obtient les obligations de preuve suivantes: ∎ Obligation de preuve de l’initialisation: démontrer démontrer que que le le prédicat prédicat H H ⇒ I ⇒ I est valide ∎ Obligation de preuve pour une opération: démontrer que le prédicat H ⇒ I est valide 59 MACHINE M VARIABLES V INVARIANT I INITIALISATION Init OPERATIONS u ← O(W) = PRE Q THEN V END END Exemple Les obligations de preuve Obligation de preuve pour l’initialisation: Aucun hypothèse But à prouver: I après Init (est ce que l’initialisation établit l’invariant?) I Obligation de preuve pour l’opération O: On On prouve prouve que que lorsque la machine est dans un état correct: les propriétés invariantes I sont supposées vérifiées lorsque l’opération est appelée avec la pré-condition Q: Q est supposée vérifiée alors sa transformation V amène la machine dans un état correct: → un état qui satisfait l’invariant I I ∧ Q ⇒ I après V I ∧ Q ⇒ I 60 MACHINE M VARIABLES V INVARIANT I INITIALISATION Init OPERATIONS u ← O(W) = PRE Q THEN V END END Exemple1 Les obligations de preuve Les obligations de preuve pour la machine M: I I ∧ Q ⇒ I 61 Les obligations de preuve Exemple2 MACHINE M(u) CONSTRAINTS C CONSTANTS c Obligation de preuve pour l’initialisation: C ∧R ⇒ I Obligation Obligation de de preuve preuve pour pour PROPERTIES l’opération O: C ∧R ∧ I ∧ P ⇒ I R VARIABLES x INVARIANT I INITIALISATION U OPERATIONS r op(p) = PRE P THEN K END; Exercice □ Écrire les obligations de preuve de la machine réservation 63 Éléments de modélisation en B □ Langage ensembliste: pour décrire le modèle de données □ Logique des prédicats du premier ordre ordre pour pour décrire décrire les les propriétés propriétés □ Langage des substitutions généralisées pour décrire les actions 64 Les substitutions généralisées généralisées 6565 Introduction □ Les substitutions généralisées sont utilisées pour décrire le corps de l’initialisation et des opérations d’un composant (clauses INITIALISATION et et OPERATIONS) OPERATIONS) □ La sémantique du langage des substitutions est définie par un calcul des substitutions qui permet d’effectuer les évaluations des obligations de preuve 66 Les substitutions généralisées Non déterminisme □ Une substitution possède un comportement non déterministe si elle décrit plusieurs comportements possibles sans préciser lequel lequel sera sera effectivement effectivement choisi. choisi. □ En B, les substitutions des machines et des raffinements peuvent être non déterministes. □ Le non déterminisme décroît lors du raffinement. 67 Les substitutions généralisées 68 Substitution devient égal □ Soit x une variable, e une expression et P un prédicat, alors : [ x := e ] P est le prédicat obtenu en remplaçant toutes les occurrences libres de x dans P par e. Règle de typage: □ Dans la substitution x := e, x et e doivent être du même type T. □ Dans la substitution x1,.., xn := e1, ..., en, chaque xi doit être du même type que ei. 69 Substitution devient égal □ Une prédicat variable ou dans est une dite expression libre dans si: un ∎ Elle est présente dans la formule et ∎ Elle sont sont quantificateurs quantifiée est pas pas présente sous sous de même la la introduisant portée portée dans nom. des de de sous certains certains une formules variable qui ne □ Exemple: Soit le prédicat: y est-elle libre? libre? n est-elle libre? x est-elle 70 Exemple de calcul: OP de reserver MACHINE reservation VARIABLES nbPlacesLibres INVARIANT nbPlacesLibres ∈ 0..100 ... OPERATIONS I ∧ Q ⇒ I devient: (nbPlacesLibres ∈ 0..100 ∧ nbPlaces ∈ NAT1 ∧ nbPlaces ≤nbPlacesLibres) ⇒ OPERATIONS reserver(nbPlaces)= (nbPlacesLibres ∈ 0..100) 2. (nbPlacesLibres ∈ 0..100 ∧ PRE nbPlaces ∈ NAT1 ∧ nbPlaces ≤ nbPlacesLibres THEN nbPlacesLibres-nbPlaces nbPlacesLibres := END END ``` (nbPlacesLibres ∈ 0..100 ∧ nbPlaces ∈ NAT1 ∧ nbPlaces ≤nbPlacesLibres) ⇒ (nbPlacesLibres-nbPlaces ∈ 0..100) 71 □ x, y := E, F Sémantique I ⇔ I z étant une variable distincte de x et y et non libre dans I Substitution simultanée □ Correspond à l’exécution simultanée de deux substitutions Deux syntaxes: □ x := E | | y := F 72 Substitution simultanée ∎ Exemple: permutation de 2 variables (x < y) (x < y) y] (x (x < < z) z) (y < z) (y < x) 73 Substitution choix borné □ Permet de définir un nombre fini de comportements possibles sans préciser lequel sera effectivement choisi (non déterministe). □ □ n'est n'est pas pas une une substitution substitution d'implémentation d'implémentation □ Syntaxe ∎ CHOICE S1 OR ... OR Sn END ∎ S1, ..., Sn des substitutions (avec n ≥ 2) □ Sémantique I ⇔ I ∧ ... ∧ I 74 Substitution choix borné □ Exemple : Définition des résultats de l’examen du permis de conduire CHOICE résultat := réussite || permis := permis U {candidat} OR résultat := échec END END □ Calculer : (permis PERS-MAJEUR) 75 Select (Garde et Choix Borné) □ La gardes d’exécution substitution qui définissent de l’instruction. SELECT les permet conditions d’exprimer des □ Syntaxe Sémantique I) ∧ WHEN WHEN ... WHEN SE] Q2 Q2 Qn THEN THEN THEN S2 S2 Sn (Qn ((¬Q1∧¬Q2∧...∧¬Qn) ⇒ (Q2 (Q2 ... ⇒ ⇒ I) ∧ I) ∧ ⇒ I) ∧ I) □ Les ce cas gardes le comportement peuvent ne pas est être non-déterministe. disjointes, dans 76 Select (Garde et Choix Borné) □ Exemple SELECT x ≥ 0 THEN y := x 2 WHEN WHEN x x ≤ ≤ 0 0 THEN THEN y := - x 2 END 77 Substitution identité □ La substitution identité Skip ne modifie pas le prédicat sur lequel elle est appliquée. □ Elle est notamment utilisée pour décrire décrire que que certaines certaines branches branches d’une d’une substitution IF, CASE ou SELECT ne modifient pas les variables. Sémantique: I ⇔ I 78 Condition par Cas □ La comportements expression. substitution CASE possibles permet en fonction de définir de différents la valeur d’une □ Syntaxe: CASE EITHER Sn] S2 S1 END □ Chaque non booléen). vide branche de constantes EITHER littérales et OR est (entier, constituée énuméré, d’une liste □ Les même L1, type .. , Ln que doivent E. être disjoints (déterminisme) et de □ Si skip. le ELSE est absent, l’échec des Li réalise la substitution 79 Condition par Cas Sémantique: CASE E OF EITHER L1 THEN S1 E∈{L1} I ∧ I ∧ ... ... ... ... OR Ln THEN Sn] E∈{Ln} I ∧ E∉{L1,L2...Ln} I (en l’absence de ELSE END SKIP ) 80 Condition par Cas □ Exemple: MACHINE triangle SETS TRIANG_TYPE isosceles, no_triangle} equilateral, = {scalene, OPERATIONS IF s1+s2 ≤ s1 or ≤ s1+s3 s3 or s2+s3 ≤ s2 THEN no_triangle tr_type := ELSE CASE OF card({s1, s2, s3}) OPERATIONS tr_type s3) = <-- classify(s1, s2, PRE s1 ∈ INT ∧ s1 ≠0 ∧ EITHER EITHER tr_type:=equilateral 1 1 THEN THEN OR 2 tr_type:=isosceles THEN OR 3 tr_type:=scalene THEN s2 ∈ INT ∧ s2 ≠0 ∧ END END s3 ∈ INT ∧ s3 ≠0 END THEN END END 81 Substitution conditionnelle IF □ La substitution conditionnelle IF est définie selon plusieurs formes : 1. IF P THEN S END Sémantique I S]I P P I I 2. IF P1 THEN S1 ELSE T END Sémantique I ⇔ (P1 I) ∧ (¬P1 I) 82 Substitution conditionnelle IF Forme générale du IF Syntaxe: Sémantique: IF P1 THEN S1 P1 ⇒ ⇒ I ∧ I I ∧ ∧ ... ⇔ ... ELSIF Pn THEN Sn] ¬P1∧¬P2∧...¬Pn-1∧Pn ⇒ I ∧ ¬P1∧¬P2∧...¬Pn-1∧¬Pn ⇒ I END 83 télécharger gratuitement La méthode B AMN(Abstract Machine Notation) "Génie Logiciel II"