Une galante introduction à la notion de machine abstraite en B

En rangeant des papiers, je suis tombé sur "Le journal secret, n° 7 de mai 1938, Revue d'éducation sexuelle. J'en ai hérité de ma mère sage-femme. Le premier article s'intitule "Donneuses" de Lait. Comment on "trait" les femmes.

 Je vais en scanner les pages. Que d'évolutions depuis 38 !
Cherchant sur la Toile, je n'ai pas trouvé l'histoire de cette revue, mais je suis tombé sur un de mes cours ! je le reproduit ici.
A ce sujet, la conférence 2014 sur la Méthode B a lieu en France, à Toulouse. Nous l'avions initialisée à Nantes.
http://www.irit.fr/ABZ2014/
http://www.methode-b.com/2014/04/abz-2014-toulouse-du-2-au-5-juin/

Une galante introduction à la notion de machine abstraite en B
(c) Henri Habrias
Département informatique
I.U.T. de Nantes
7- 01- 2001

«Le baron Warseberg, malgré qu’il entretenait la demoiselle Laforest voyait encore les filles de la Varenne. Il puisa dans le flanc de Mlle Dorville ce poison destructeur, qu’il procura à Mlle Laforest, qui de son côté en fit présent à M. Saimson, mousquetaire, avec qui elle greluchonait, lequelle par la même voie en fit cadeau à Mlle Ricourt, de la Comédie Italienne, qui, sans façon la voitura à M. de la Ferté, intendant des Menus Plaisirs, qui en gratifia Mlle Rozetti, qui, de même, me la souffla… »

Mémoires du chevalier de Fontainieu qui raconte les origines d’une galanterie (entendez une blennorragie) qu’il attrapa, in Le Journal Secret, Revue d’éducation sexuelle, 1et Mai 1938
NOTA 1 :
Cette spécification est écrite en utilisant la notation ASCII de B. Son avantage : disponible sur tout clavier et utilisable en HTML. Vous trouverez ici les tableaux de correspondance entre le notation dite "mathématique" de B et la notation ASCII.
NOTA 2 :
Cette spécification n'a pas été vérifiée avec l'Atelier B. Nous vous proposons de vous en servir lors du premier td d'Atelier B.
MACHINE

Galanterie

SETS

PERSONNE ; SEXE = {masc, fem}; NOM ;

METIER
/* Les SETS sont des ensembles qui n’ont aucun élément en commun. On les appelle aussi « ensembles de base ». Ce sont des ensembles finis et non vides (comme on construit tous les autres ensembles à partir d’eux, si ils étaient vides on obtiendrait des ensembles vides !) . On ne peut écrire des énoncés comme PERSONNE \/ SEXE ou encore PERSONNE := PERSONNE – {pp}. Les SETS sont en quelque sorte des constantes.
On construit des ensembles à l’aide du produit cartésien et de l’opérateur ensemble des parties (ou encore ensemble des sous-ensembles d’un ensemble).
Ici, le set SEXE est défini en extension. */
VARIABLES

APourSexe, AdonnéGalanterieA, ApourMétier, Personnes

DEFINITIONS

Homme == APourSexe~ [{masc}] ;
Femme == APourSexe~ [{fem}] ;

/* APourSexe~ [{masc}]
dénote l’image relationnelle de l’ensemble singleton {masc} par l’inverse de la fonction APourSexe.
Le symbole ~ dénote la relation inverse (on dit aussi réciproque). Ces définitions utilisent la spécification de la fonction APourSexe qui est donnée dans l'invariant (voir ci-dessous).
Le symbole == dénote en ASCI une définition. A ne pas confondre avec le symbole = dénotant le prédicat d’égalité. */
/* Les définitions sont ce que les informaticiens appellent des « macro » (macro-instructions). Ce ne sont pas des variables. Une variable peut se trouver en partie gauche d’une substitution ( :=). Ce n’est pas le cas d’une définition. Une définition est un nom de morceau de texte de spécifications. */
INVARIANT

Personnes < : PERSONNE &
APourSexe : Personnes --> SEXE &
ADonnéGalanterieA : Homme <-> Femme &
ADonnéGalanterieA /\ ADonnéGalanterieA~ = {} &
APourMétier : Personnes +-> METIER

/* L’invariant est un prédicat. Tout état du système doit respecter l’invariant. */
/* : est la notation ASCII pour l’appartenance.
& est la notation ASCII pour le « et » logique.
  A < : B est le prédicat d’inclusion de l’ensemble A dans l’ensemble B
A --> B est l’ensemble des fonctions totales (on dit en français, applications) de l’ensemble A vers l’ensemble B)
A <-> B est l’ensemble des relations quelconques de A vers B. Voir exemple de relation avec des diagrammes sagittaux, avec des "tables relationnelles" (pour causer comme les gens des "bases de données")
A +-> B est l’ensemble des fonctions partielles de l’ensemble A vers l’ensemble B. */
/* L’invariant est un prédicat. Ici il s’agit d’une conjonction de prédicats élémentaires.
Personnes < : PERSONNE se paraphrase ainsi : « Personnes est une variable qui prend comme valeurs un sous-ensemble de l’ensemble PERSONNE. »
APourSexe : Personnes --> SEXE se paraphrase ainsi : «  APourSexe est une variable qui prend comme valeur un élément de l’ensemble de toutes les fonctions totales (on dit dans les livres de mathématiques français, application) de l’ensemble Personnes vers l’ensembleSEXE. En d’autres termes, ApourSexe est une variable qui est une fonction totale (le verbe être est ici utilisé dans le sens de l’appartenance ensembliste) »
ADonnéGalanterieA : Homme <-> Femme se paraphrase ainsi « AdonnéGalanterieA est une variable qui prend comme valeur un élément de l’ensemble de toutes les relations quelconques de l’ensemble Homme vers Femme »
ADonnéGalanterieA /\ ADonnéGalanterieA~ = {} se paraphrase ainsi « si une personne p1 donne galanterie à une personne p2 alors p2 ne donne pas galanterie à p1. Ceci permet aussi d'exprimer que l'on ne se donne pas galanterie à soi-même.»
APourMétier : Personnes +-> METIER se paraphrase ainsi « ApourMétier est une variable qui prend comme valeur un élément de l’ensemble de toutes les fonctions partielles de Personne vers METIER »
*/
INITIALISATION

ApourSexe, AdonnéGalanterieA, ApourMétier, Personnes := {},{},{}, {}

/* := est le symbole de la substitution simple. Ici on fait quatre substitutions en parallèle.
On pouvait aussi écrire en B, ainsi :
ApourSexe := {} ||
AdonnéGalanterieA := {} ||
ApourMétier := {} ||
Personnes := {}
Notons que dans une machine abstraite B, on n’a pas le droit d’utiliser le séquencement (noté par ;), lequel est réservé aux étapes suivantes du raffinage. */
/* On doit s’assurer qu’il y a au moins un état qui satisfait l’invariant. */
/* Voici un état du système décrit par le texte fourni */

Personnes = {Warseberg, Dorville, Lafores, Saimson, Ricourt, de la Ferté, Rozetti, Fontainieu}ApourSexe = {(Warseberg, masc), (Dorville, fem), (Laforest, fem), (Saimson, masc), (Ricourt, fem), (de la Ferté, masc), (Rozetti, fem), (Fontainieu, masc)}
AdonnéGalanterieA = { Dorville, Warseberg), (Warseberg, Laforest), (Laforest, Saimson), (Saimson, Ricourt), (Ricourt, de la Ferté), (de la Ferté, Rozetti), (Rozetti, Fontainieu)}
ApourMétier = { (Saimson, mousquetaire), (Ricourt, comédienne), (de la Ferté, intendant des Menus Plaisirs), (Fontainieu, chevalier)}

*/
OPERATIONS

NouvellePersonne (Sexe) =
PRE

Sexe : SEXE &
PERSONNE – Personnes /= {}

/* Le signe = ici ne dénote pas le prédicat d’égalité mais une définition. */
/* La précondition est la plus faible précondition pour que l’opération respecte l’invariant.
Par exemple, si l’invariant est x < 10, la plus faible précondition pour que l’opération x := x + 1 respecte cet invariant (ce qui s’écrit [x := x + 1] (x < 10) ) est : x + 1 < 10 soit x < 9. C’est bien la plus faible (x = 0 par exemple sera bien plus forte (serait plus exigeante que ce qui est suffisant)).*/
/* Si l’on respecte la précondition, l’opération conduira à un état respectant l’invariant. On a « typé » le paramètre d’entrée de l’opération et on s’assure qu’il reste des personnes qui ne sont pas encore « nées » */

THEN

ANY pp WHERE pp : PERSONNE – Personnes THEN
Personnes := Personnes \/ {pp} ||
ApourSexe := ApourSexe \/ {pp |-> Sexe}

/* Le symbole ASCII \/ dénote l’union ensembliste. pp |-> Sexe est un couple. Le symbole ASCII |-> sert à exprimer un couple (maplet). */
/* On fait un choix indéterministe (ANY pp WHERE) dans l’ensemble des personnes non encore « nées ». On spécifie deux substitutions en parallèle. Si on ne faisait pas la substitution ApourSexe := ApourSexe \/ {pp |-> Sexe}, on ne respecterait pas l’invariant (pour toute personne, on doit avoir enregistré de quel sexe est cette personne). */

END ;

END ;

NouvelleGalanterie (Pers1, Pers2) =

PRE

Pers1 : Personnes &
Pers2 : Personnes &
Pers2 |-> Pers1 /: AdonnéGalanterieA

THEN

AdonnéGalanterieA : = AdonnéGalanterieA \/ {Pers1 |-> Pers2}

END ;

SupressionPersonne (Pers) =

PRE

Pers : Personnes &
Pers / : dom (APourMétier) &
Pers /: (dom (AdonnéGalanterieA) \/ ran (AdonnéGalanterieA))

/* / :  est le symbole ASCII pour la négation de l’appartenance ensembliste
dom (APourMétier) désigne le domaine de la relation APourMétier */
/* Si on n’avait pas la contrainte Pers / : dom (ApourMétier), il faudrait « enlever » le couple (Pers |-> ApourSexe (Pers)) de l’ensembleApourSexe.
Attention ! Nous venons de faire un abus de langage. On n’enlève pas un élément d’un ensemble. L’ensemble {1, 2, 3} est l’ensemble {1, 2, 3} ad vitam aeternam. Ce n’est pas une variable.
Il aurait fallu dire « substituer à la variable ApourSexe, l’ensemble égal à la valeur actuelle de cette variable moins l’ensemble singleton {(Pers |-> ApourSexe (Pers))}. */

THEN

Personnes := Personnes – {Pers} ||
APourSexe := {Pers} <|| ApourSexe

/* Le symbole ASCII <|| est celui de l’antirestriction de domaine. */

END ;

Galants <- font="" quiaattrap="">

BEGIN

Galants := dom (AdonnéGalanterieA) \/ ran (AdonnéGalanterieA)

END

END

/* dom (R) représente le domaine de la relation RA. ran (R) représente le codomaine de la relation R . Le symble ASCII \/ est celui de l'union ensembliste.  */
.
Nouvelle spécification
Si nous modifions la liste des variables et l’invariant en supprimant la variable Personnes, et en ajoutant Personnes dans les définitions :
Personnes == dom (ApourSexe), nous devons modifier les opérations :

OPERATIONS

NouvellePersonne (Sexe) =

PRE

Sexe : SEXE &
PERSONNE – Personnes /= {}

THEN

ANY pp WHERE pp : PERSONNE – Personnes THEN
ApourSexe := ApourSexe \/ {pp |-> Sexe}

END ;

END ;

NouvelleGalanterie (Pers1, Pers2) =

PRE

Pers1 : Personnes &
Pers2 : Personnes &
Pers2  |-> Pers1 :/ AdonnéGalanterieA

THEN

AdonnéGalanterieA : = AdonnéGalanterieA \/ {Pers1  |-> Pers2}

SupressionPersonne (Pers) =

 PRE

Pers : Personnes &
Pers / : dom ((AdonnéGalanterieA) \/ ran (AdonnéGalanterieA))

THEN

ApourMétier := {Pers} <|| ApourMétier

 END

END

Quelques opérations supplémentaires :
Opération donnant l'ensemble des personnes à l'origine de la "galanterie" d'une personne donnée
/* Voici une opération ayant paramètre d'entrée et paramètre de sortie.*/
/* ADonnéGalanterieA+ est la fermeture transitive et non réflexive d'une relation.
Exemple :
soit la relation R = {(1,2), (2, 3), (3, 4)}
R²= R ; R = {(1, 3), (3, 4)}
Le symbole ; est celui de la composition "en avant".
R³ = R²; R = {(1, 4)}
R⁴= R³ ; R = {(1, 4)}. On a obtenu la fermeture transitive. Ici elle n'est pas réflexive : on n'a pas de couple dont la partie gauche est égale à la partie droite. */
/* Remarquons que les paramètres d'entrée sont typés dans la précondition. Mais que ce n'est pas le cas des paramètres de sortie. On ne peut vérifier leur type lors de l'appel de l'opération. Leur typage est fourni après le THEN. */

ALOrigine <-- font="" pers="" quialorgine="">

PRE

pers : ran (ADonnéGalanterie)

THEN

ALOrigine :=  (ADonnéGalanterieA+)~ [{pers}]

END

Opération donnant l'ensemble des femmes ayant transmis la "galanterie"
/* Le symbole ASCII <| est celui de la restriction du domaine d'une relation. */

Fem <-- atransmis="</font">

BEGIN

Fem := dom (Femme <| ADonnéGalanterieA)

END

Nous n'avons pas vérifié cette spécification. Il doit certainement y avoir des erreurs !Exercice :
- Vérifiez cette spécification avec l'atelier B, à savoir :
1) Vérifier  la syntaxe, le typage des variables
2) Générer les obligations de preuve
3) Prouver chacune...mais il se peut que certaines spécifications d'opération ne respectent pas l'invariant. En conséquence, vous ne pourrez prouver que :
Précondition &  invariant implique que la substitution établit l'invariant

Et la suite ?
Avant d'aller plus loin, remarquons que :
Dans une spécification abstraite :
- on peut avoir de l'indéterminisme. Nous en avons eu un exemple ici avec le choix indéterministe dans un ensemble.

Normal ! on ne veut pas tout dire dès le début. On laisse des décisions pour la suite de la conception.

- on a des préconditions

Normal ! quand on spécifie par exemple une opération de division, on veut que ce soit une fonction. Et la fonction division ne donne pas comme résultat : "je ne peux pas diviser" ! Propos étonnant ?! Non, voyez vos livres de mathématiques.
Mais vous savez qu'une fonction a un "domaine de définition". La précondition s'assure que l'on est bien dans le domaine de définition.

- on n'a pas de séquencement

Normal ! on veut être abstrait et ne pas être contraint par le séquencement (qui va nous être imposé par la suite par l'ordinateur). Si on veut rester proche de l'expression du besoin par le client, il ne faut pas être obligé de choisir, dès la spécification, un séquencement là où c'est hors de propos.

Par la suite :

On raffine une machine abstraite. Le raffinage consiste à se rapprocher d'une implantation. Le raffinage se fait "à signature" identique. C'est-à-dire que l'on ne change pas les paramètres des opérations.
Quand on écrit une machine qui raffine une autre machine, dans l'invariant de la nouvelle machine, on relie les variables de la machine abstraite aux variables de la machine concrète (on appelle cet invariant, invariant de collage (gluing invariant).
On introduit :

- le séquencement
- on diminue l'indéterminisme
- on affaiblit les préconditions

On a des machines dites REFINEMENT
jusqu'à arriver à des machines dites IMPLEMENTATION
dans lesquelles :

- il n'y aura plus de parallèlisme (on ne trouvera plus le symbole ||)
- on trouvera la séquence (;) et la boucle
- il n'y aura plus de préconditions dans le code des opérations

A chaque étape, il faudra prouver que le raffinage est correct.
Donc, en B, on distingue deux ensembles de preuves :

- les preuves d'opération (qui sont faites à un niveau d'abstraction)
- les preuves de raffinage (qui portent sur la relation de raffinage entre une opération abstraite et une opération plus concrète).

Bibliographie
J.R. Abrial, The B-Book, Assigning programs to meanings, Cambridge University Press, 1996
ISBN : 0 521 49619 5