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
- 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:
- (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 « `
- (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
- 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 »
