Méthode B

La Méthode B est une méthode formelle de développement logiciel qui permet de modéliser de façon abstraite en langage B le comportement d'un programme, puis par raffinements successifs, d'aboutir à un modèle concret, sous-ensemble du langage transcodable en Ada ou en C.

Une activité de preuve formelle permet de vérifier la cohérence du modèle abstrait et la conformité de chaque raffinement avec le modèle supérieur (prouvant ainsi la conformité de l'ensemble des implantations concrètes avec le modèle abstrait).

On distingue le « B classique » du « B événementiel », ce dernier étant proche des « Actions Systems ».

Sommaire
1 Historique de B
2 Buts de B
3 B méthode formelle
4 Couverture de B
5 La notation B par l'exemple

5.1 Une première machine abstraite en B
5.2 Une autre machine abstraite B

6 Le concept de précondition
7 B et spécifications algébriques
8 Différence fondamentale entre Z et B
9 Partie de la notation ASCII utilisée en B (vocabulaire français)
10 Bibliographie
11 Qui enseigne B dans le monde ?
12 Liens externes
13 Les conférences internationales B

Historique de B

B, une déjà longue histoire (source : cours vidéo de J.R. Abrial)

Buts de B

B méthode formelle

Couverture de B

B couvre :

La notation B par l'exemple

Une première machine abstraite en B

Cette machine est écrite en notation B Ascii. Il existe aussi une « notation mathématiques », fournie plus loin, qui utilise les symboles usuels de la mathématique ensembliste et de la logique des prédicats.

MACHINE

reservation (max_siege)

/* Le nom de la machine est réservation. On lui passe en paramètre la variable max_sieges. */

CONSTRAINTS

max_sieges : NAT

/* Prédicat d'appartenance. max_sieges appartient à l'ensemble des nombres naturels implantables */

VARIABLES

nb_sieges_dispos

/* nb_sieges_dispos est une variable. On va apprendre dans la rubrique INVARIANT quel est son type. */

INVARIANT

nb_sieges_dispos : 0..max_sieges


/* L'invariant est un prédicat qui doit respecter l'état de la machine. On apprend ici que nb_sieges_dispos est un élément (: est la notation ascii pour l'appartenance ensembliste) de l'ensemble qui va de 0 à max_sieges, max_sieges ayant été passé en paramètre à la machine. nb_sieges_dispos est donc un nombre entier. C'est le nombre de sièges disponibles. On le comprendra avec l'opération réserver.*/

INITIALISATION

nb_sieges_dispos := max_siege


/* La rubrique INITIALISATION permet de vérifier que la spécification a au moins un modèle, une instanciation qui satisfait l'invariant L'opérateur := se lit devient égal à. Il s'agit de la spécification d'une opération. Il s'agit également d'une substitution simple. Cette opération, lorsqu'elle est appliquée au prédicat qui représente la contrainte que l'état de la machine doit respecter, modélise la transformation de la mémoire opérée par l'initialisation : [ nb_sieges_dispos := max_sieges] (siege : 0..max_sieges) <=> max_siege : 0..max_sieges et produit le prédicat qui représente la condition minimale que l'état doit vérifier avant l'exécution de l'opération pour que, après l'exécution, les propriétés de l'état soient toujours vérifiées. [ nb_sieges_dispos := max_sieges] (nb_sieges_dispos : 0..max_sieges) se lit : « nb_sieges_dispos devient égal à max_sieges établit que nb_sieges_dispos : 0.. max_sieges. » Plus généralement, si I désigne un prédicat qui doit être respecté par l'état de la machine et si x := E modélise une des opérations de la machine, alors [x := E] I représente la plus faible condition pour que l'exécution x := E se termine et établisse I. Explications :

[x := E] I remplace les occurrences libres de x dans I par l'expression E.
Par exemple, [x := x+1] (x : N) donne x+1 : N ;
[S] I est interprété ainsi :
I est la condition désirée « après » (on dit aussi post-condition). C'est un prédicat.
[S] I est la condition nécessaire et suffisante « avant ».

Ainsi toute substitution S définit ce qu'on appelle un « transformateur de prédicat » qui associe à toute post-condition R la plus faible pré-condition, notée [S] I, permettant de garantir que R est vraie juste après l'exécution de l'opération. Lorsque c'est bien le cas (R est vraie après l'exécution de l'opération S), on dit que S établit R. La notion de plus faible précondition (weakest precondition) a été introduite par E.W. Dijkstra avec la notation wp(S,I).

Exemple : condition désirée après : x <=10 substitution : x := x+1 condition nécessaire et suffisante « avant » :

[x := x+1] (x<=9)
x+1 <= 10
x <= 9
x<=9 est la condition nécessaire et suffisante pour que x <= 10 soit vrai après la substitution.*/

OPERATIONS

/* Cette rubrique (en B, on dit aussi clause) contient la définition des opérations offertes par la machine abstraite (on dit aussi, opérations faisant partie du répertoire d'instructions de la machine, ou encore, services offerts par la machine abstraite). Une opération a une en-tête qui a la forme générale suivante : Nom des paramètres de sortie <-- Nom de l'opération (Nom des paramètres d'entrée)

On a donc 4 cas possibles :

Dans cet exemple, nous n'avons que le premier cas. */

reserver =

PRE
0 < nb_sieges_dispos
THEN
nb_sieges_dispos := nb_sieges_dispos - 1
END;


/* Le symbole égal surmonté d'un chapeau se lit « se définit ainsi ». Il se différencie ainsi du symbole d'égalité. Ici, il est noté par « = » en notation ascii.

Vous voyez apparaître un PRE...THEN... . A quoi cela sert-il ? Supposons qu'on ait écrit seulement nb_sieges_dispos := nb_sieges_dispos - 1 On doit avoir : (voir l'exemple précédent)

[nb_sieges_dispos := nb_sieges_dispos - 1] (nb_sieges_dispos : 0..max-sieges) et donc
nb_sieges_dispos - 1 : 0..max-sieges,

prédicat qui ne peut être vérifié si nb_sieges_dispos vaut 0. Or on veut que l'invariant soit respecté par les opérations. On utilise pour ça une précondition d'emploi de l'opération.

Si P est un prédicat et S une substitution, P | S, qui se lit : le prédicat P qui préconditionne la substitution S, est défini par :

[P | S] I <=> P & [S] I qui se lit :

La substitution conditionnée [P | S] établit I si et seulement si P et ("et" logique) la substitution S établit que I est vrai. Du fait du &, si la précondition P est fausse, P & [S] I est faux. Ce cas est celui de l'avortement (on dit aussi du crash). Il modélise un programme dont on n'est jamais garanti qu'il se termine et même quand il se termine, il peut faire n'importe quoi. P | S a une forme « littéraire » : PRE P THEN S END */


annuler =

PRE
nb_sieges_dispos < max_sieges
THEN
nb_sieges_dispos := nb_sieges_dispos + 1
END;

/* Annuler une réservation consiste à additionner 1 au nombre de sièges disponibles. On a mis une précondition pour s'assurer qu'on ne dépassera pas sa limite. */


END

/* cela montre la fin de la spécification de cette machine. */

Une autre machine abstraite B

MACHINE

maPetiteEntreprise

/* rédige par Dudule le 06-04-2005 */

SETS

PROJET; SERVICE; EMPLOYE

VARIABLES

employe, service, projet, est_affecte, est_responsable_de_projet, est_responsable_de_service

INVARIANT /* Voici les contraintes à satisfaire :

employe <: EMPLOYE &
service <: SERVICE &
projet <: PROJET &
est_affecte : employe --> service &

/* employe --> service est l'ensemble des fonctions totales d'employe vers service */

est_responsable_de_service : employe >+> service &

/* +-> est mis pour l'ensemble des fonctions partielles. La partialité est exprimée par le trait vertical coupant la flèche de totalité. Comme l'ensemble des relations quelconques est exprimé par <-->, l'on ne pouvait utiliser < pour exprimer une fonction de la partie droite vers la partie gauche, d'où l'utilisation de >. Ainsi >+> représente une fonction partielle de la gauche vers la droite et une fonction de ma droite vers la gauche. */

est_responsable_de_service <: est_affecte &
est_responsable_de_projet : employe >+> projet &
dom(est_responsable_de_projet) /\

/* /\ est le symbole Ascii de l'intersection ensembliste */

dom(est_responsable_de_service)={} 

INITIALISATION
    employe, service, projet, est_affecte, est_responsable_de_service,est_responsable_de_projet := {},{},{},{},{},{}
 OPERATIONS
    ajout_employe(ss)=
       PRE
          ss : SERVICE &
          ss : service &
          (EMPLOYE - employe) /= {}
       THEN
          ANY ee WHERE
             ee : (EMPLOYE - employe)
          THEN
             employe := employe \/ { ee } ||
             est_affecte := est_affecte \/ { ee|->ss }
          END
       END;

    ajout_service=
       PRE
          (SERVICE-service) /= {}
       THEN
          ANY ss WHERE
             ss : (SERVICE-service)
          THEN
             service:=service \/ {ss}
          END
       END;

    ajout_responsable_service(ee,ss)=

       PRE
          ss : SERVICE &
          ss : service &
          ee : EMPLOYE &
          ee : employe &
          ee /: dom (est_responsable_de_service) &
          ee /: dom(est_responsable_de_projet) &
          ss /: ran (est_responsable_de_service) &
          ee|->ss: est_affecte
       THEN
          est_responsable_de_service:=est_responsable_de_service \/ {ee|->ss}
       END;

    ajout_projet=
       PRE
          (PROJET - projet) /: { }
       THEN
          ANY pp WHERE 
             pp : (PROJET - projet)
          THEN
             projet:=projet \/ {pp}
          END
       END;

    ajout_responsable_projet(pp, ee)=
       PRE
          pp : PROJET &
          pp : projet &
          ee : EMPLOYE &
          ee : employe &
          ee /: dom (est_responsable_de_service) &
          ee /: dom (est_responsable_de_projet) &
          pp /: ran (est_responsable_de_projet)
       THEN
          est_responsable_de_projet := est_responsable_de_projet \/ { ee|->pp }
       END;

    suppression_employe(ee)=
       PRE
          ee : EMPLOYE &
          ee : employe &
          ee : dom (est_affecte) &
          ee /: dom (est_responsable_de_service) &
          ee /: dom(est_responsable_de_projet)
       THEN
          employe := employe - {ee} ||
          est_affecte := {ee} <<| est_affecte
       END;

    suppression_responsable_service(ss)=
       PRE
          ss : SERVICE &
          ss : service &
          ss : ran (est_responsable_de_service) &
          est_responsable_de_service~(ss) |-> ss: est_affecte
       THEN
          est_responsable_de_service:= {est_responsable_de_service~(ss)} <<|est_responsable_de_service
       END;

    suppression_service(ss)=
       PRE
          ss : SERVICE &
          ss : service &
          ss /: ran (est_responsable_de_service)
       THEN
          service := service - {ss}
       END;

    suppression_responsable_projet(pp)=
       PRE
          pp : PROJET &
          pp : projet &
          pp : ran (est_responsable_de_projet)
       THEN
          est_responsable_de_projet := {est_responsable_de_projet~(pp)}<<|est_responsable_de_projet
       END;

    suppression_projet(pp)=
       PRE
          pp : PROJET &
          pp : projet &
          pp /: ran (est_responsable_de_projet)
       THEN
          projet := projet - {pp}
       END

 END

Le concept de précondition

Soit la machine suivante : 

MACHINE
    Calculette
 ...
 OPERATIONS
    cc <-- plus (aa, bb) =
    /* avec l'Atelier B, les noms des variables
       et des constantes doivent faire au moins 
       deux caractères */
       PRE
          a : NAT &
          b : NAT &
          a + b : NAT
       THEN
          cc := aa + bb
       END;
 ...
 END

Exemple de la calculette :

Le concepteur du logiciel démontrera, une fois pour toute, que si la précondition est remplie, la calculette fonctionnera correctement.

ATTENTION : 

   Bien différencier l'approche B (programmation offensive) de la programmation défensive !

Exemple de mon enrouleur de câble électrique :

J'ai un enrouleur de câble électrique qui porte l'étiquette suivante : « Puissance maximale sous 200 V = 2000 W avec le câble déroulé, 1000 W avec le câble enroulé. » J'ai utilisé ma tondeuse électrique de 12000 W avec le câble enroulé.

Cette démonstration a été faite une fois pour toute en utilisant les lois de la physique. Le vendeur ne m'a pas remboursé l'enrouleur.

C'est alors à l'utilisateur à ne faire appel à l'enrouleur qu'en respectant les conditions d'emploi. Ces conditions d'emploi ne peuvent être vérifiées dans le « code » de l'opération.

B et spécifications algébriques 

MACHINE 
    VARIABLE (VALEUR)
 VARIABLES
       vrb
 INVARIANT
       vrb : VALEUR
 OPERATIONS

    v <-- valeur =
       BEGIN
          v:= vrb
       END ;

    changer (v) =
       PRE
          v : VALEUR
       THEN
          vrb := v
       END

 END

En spécification algébrique, on écrit des AXIOMES :

valeur (changer (v)) = v

Différence fondamentale entre Z et B

nota : nous avons utilisé aussi bien pour Z que pour B la notation ASCII B.

[NOM, ADRESSE] 

_____CarnetDAdresses___________________
   NomConnu : F NOM
   APourAdresse : NOM -+> ADRESSE
 __________
   dom (APourAdresse) = NomConnu
 ____________________________________
 
 
 _____AjoutDAdresse_______________________
   Δ CarnetDAdresses
   nom? : NOM
   adr? : ADRESSE
  ___________
   nom? :  NomConnu ?
   APourAdresse' = APourAdresse <+ {(nom? |-> adr?)}
 
  _________________________________________

A-t-on besoin, en Z, de spécifier que : NomConnu' = NomConnu \/ {nom?}

Réfléchissez bien à cette question.

Et lisez ensuite ce qui suit : 

MACHINE
    CarnetDAdresses

 SETS
    NOM; ADRESSE

 VARIABLES
    NomConnu, APourAdresse

 INVARIANT
    NomConnu <: NOM &
    ApourAdresse: NomConnu +->ADRESSE

 INITIALISATION
    NomConnu := {} ||
    APour Adresse := {}

 OPERATIONS
    AjoutDAdresse(nom, adr) =
       PRE
          nom : NOM - NomConnu &
          adr : ADRESSE
       THEN
          APourAdresse := APourAdresse <+ {nom |-> adr} ||
          NomConnu := NomConnu \/{nom}
       END

 END

Partie de la notation ASCII utilisée en B (vocabulaire français)


Bien pratique pour les échanges sur Internet et pour saisir une machine B avec un clavier de monsieur tout le monde !

Logique

Code Libellé Notation Mathématique
P & Q Conjonction P\and Q
P or Q Disjonction P\vee Q
P => Q Implication P\Rightarrow Q
P <=> Q Equivalence P\Leftrightarrow Q
not P Négation \neg P
!(x).(P=>Q) Quantification universelle \forall(x)\cdot (P\Rightarrow Q)
#(x).(P) Quantification existentielle \exists(x)\cdot (P)


Egalité-Inégalité

Code Libellé Notation Mathématique
E = F Egalité E = F
E /= F Inégalité E\neq F
M <= N Inférieur ou égal M\le N
M < N Strictement inférieur M < N
M >= N Supérieur ou égal M\ge N
M > N Strictement supérieur M > N


Prédicats sur les ensembles
Code Libellé
E : S Appartenance
E /: S N'appartient pas
S <: T Sous-ensemble (inclusion)
S /< T non inclus
S <<: T sous ensemble strict ⊂


Ensembles
Code Libellé
E |-> F Couple
S * T Produit cartésien
pow (S) Ensemble des parties de S
S \/ T Union ∪
S /\ T Intersection ∩
S - T Différence
{ } Ensemble vide


Nombres
Code Libellé
NAT Les nombres naturels implantables
card (S)Cardinal de S

Relations
Code Libellé
S <-> T Relations quelconques
dom (r) Domaine de r
ran (r) Codomaine de r
id (r) Identité de r
S <| r Restriction de domaine
S <<| r Corestriction de domaine
r |> T Restriction de codomaine
r ~ Relation inverse de r
r [S] Image de S par r (on dit aussi image relationnelle)
r1 +> r2 Ecrasement de r2 par r1

Fonctions
Code Libellé
S +-> T ensemble des Fonctions partielles de S vers T
S --> T ensemble des Fonctions totales de S vers T
S >+> T ensemble des Injections
S >-> T ensemble des Injections totales
S +->> T ensemble des Surjections
S -->> T ensemble des Surjections totales
S >->> T ensemble des Bijections
f(E) Application de fonction


Suites (séquences en anglais)
Code Libellé
<> Suite vide
seq (S) Ensemble des Suites de S
iseq (S) Ensemble des Suites injectives
j ^k Concaténation
E -> J Ajout en début
J <- E Ajout en fin
[E] Suite singleton
size (J) Taille de la suite J
first (J) Premier élément de la suite J
last (J) Dernier élément de la suite J

Substitutions
Code Libellé
x := E Substitution simple
x,y := E,F Substitution multiple
G;H Séquence
skip Skip
x :: S Choix indéterministe de x parmi les éléments de S
x : P Choix par prédicat

Bibliographie

[1]

Qui enseigne B dans le monde ?

voir : [2]

Liens externes

Les conférences internationales B

See also: Méthode B, Ada (langage), B (langage), C (langage), Développement de logiciel, Méthode formelle (informatique)