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

 

 

Cours « Génie Logiciel II » 

Chapitre 2: La méthode B AMN(Abstract AMN(Abstract Machine Machine Notation) 

Niveau: II2 Enseignante: Rim DRIRA rim.drira@ensi-uma.tn 

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 raffinementRaffinement 

Raffinement 2 

Méthode B 

Raffinement 2 

Raffinement n-1 

Raffinement n 

Code 

Modèle abstrait 

Raffinement 1 

Preuve PA 

Preuve PR1 

Preuve Preuve PR 

PR2 

Preuve PRn-1 

Preuve PRn 

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 SETSDé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 SETSDé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 = -231 max_ent = 231 – 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 = -231 ∧ ∧ max_ent = 231 – 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é} VARIABLEST, Alarme INVARIANTT 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 = -231 ∧ max_ent = 231– 1 ∧ 

r, o ‹ — add (a, b) = PREa ∈ ENTIER ∧ 

b ∈ ENTIER THENIF a + b ∈ ENTIER 

∧ max_ent = 2 – 1 ∧ ENTIER = min_ent .. max_ent OPERATIONS 

r ‹ — plus (a, b) = PREa ∈ ENTIER ∧ b ∈ ENTIER ∧ 

a + b ∈ ENTIER THENr := 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)= 

PREnbPlaces ∈ 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 

1. 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 » [S] P se lit « la substitution S établit le ∎ [S] 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: 

∎ [x:=E]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 ⇒[Init]I ⇒[Init]I est valide 

∎ Obligation de preuve pour une opération: 

démontrer que le prédicat H ⇒ [V]I est valide 

59 

MACHINE 

M VARIABLES V INVARIANT 

I 

INITIALISATION Init OPERATIONS 

u ← O(W) = PRE 

Q THENV 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?) [Init]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 ⇒ [V] I 

60 

MACHINE 

M VARIABLES V INVARIANT 

I 

INITIALISATION Init OPERATIONS 

u ← O(W) = PRE 

Q THENV END END 

Exemple1 

Les obligations de preuve 

Les obligations de preuve pour la machine M: 

[Init]I I ∧ Q ⇒ [V] I 

61 

Les obligations de preuve 

Exemple2 MACHINE M(u) CONSTRAINTS CCONSTANTS c 

Obligation de preuve pour l’initialisation: C ∧R ⇒[U]I 

Obligation Obligation de de preuve preuve pour pour PROPERTIES 

l’opération O: C ∧R ∧ I ∧ P ⇒ [K] I RVARIABLES xINVARIANT IINITIALISATION UOPERATIONS 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 ⇒ [V]I devient: 

1. (nbPlacesLibres ∈ 0..100 ∧ nbPlaces ∈ NAT1 ∧ nbPlaces ≤nbPlacesLibres) ⇒[nbPlacesLibres := nbPlacesLibres-nbPlaces] 

OPERATIONS 

reserver(nbPlaces)= 

(nbPlacesLibres ∈ 0..100) 2. (nbPlacesLibres ∈ 0..100 ∧ 

PREnbPlaces ∈ NAT1 ∧ 

nbPlaces ≤ nbPlacesLibres THEN 

nbPlacesLibres-nbPlaces nbPlacesLibres := END END « ` 

2. (nbPlacesLibres ∈ 0..100 ∧ nbPlaces ∈ NAT1 ∧ nbPlaces ≤nbPlacesLibres) ⇒ (nbPlacesLibres-nbPlaces ∈ 0..100) 

71 

□ x, y := E, F Sémantique 

[x, y := E, F] I ⇔ 

[z := F][x := E][y := z]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 := y, x] (x < y) 

[z := x][x := y][y := z] (x < y) 

[z [z := := x][x x][x := := y] y] (x (x < < z) z) 

[z := x] (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 

[CHOICE S1 OR … OR Sn END] I ⇔ [S1] I ∧ … ∧ [Sn] 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 : 

[CHOICE résultat := réussite || permis := permis U {candidat} 

OR résultat := échec END] (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 

[SELECT Q1 THEN S1 (Q1 ⇒ ⇒ 

[S1]I) ∧ WHEN WHEN … WHEN [ELSE END] 

SE] Q2 Q2 Qn THEN THEN THEN S2 S2 Sn (Qn ((¬Q1∧¬Q2∧…∧¬Qn)⇒ (Q2 (Q2 … ⇒ ⇒ [S2]I)∧ [S2]I)∧ ⇒ [Sn]I) ∧ [SE]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 := x2 

WHEN WHEN x x ≤ ≤ 0 0 THEN THEN 

y := – x2 

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: 

[skip] 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 [OR …OR OR E Ln Ln OF L2 THEN THEN THEN L1 THEN Sn] Sn] S2 S1 [ELSE SE] 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} [S1]I ∧ [OR L2 THEN S2 E∈{L2} [S2]I ∧ … … … … OR Ln THEN Sn] E∈{Ln} [Sn]I ∧ [ELSE SE] E∉{L1,L2…Ln} [SE]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 

[P [P S]I S]I P P [S]I [S]I 2. IF P1 THEN S1 ELSE T END Sémantique [IF P1 THEN S1 ELSE T END]I ⇔ (P1 [S1]I) ∧ (¬P1 [T]I) 

82 

Substitution conditionnelle IF 

3. Forme générale du IF Syntaxe: Sémantique: 

IF P1 THEN S1 P1 ⇒ ⇒ 

[S1]I ∧ [ELSIF [ELSIF P2 P2 THEN THEN S2 S2 ¬P1∧P2 ¬P1∧P2 ⇒ ⇒ [S2]I [S2]I ∧ ∧ … ⇔ … ELSIF Pn THEN Sn] ¬P1∧¬P2∧…¬Pn-1∧Pn ⇒ [Sn]I ∧ [ELSE SE] ¬P1∧¬P2∧…¬Pn-1∧¬Pn ⇒ [SE]I END 

83 

télécharger gratuitement La méthode B AMN(Abstract Machine  Notation) « Génie Logiciel II »