samedi 20 février 2016

B Method, Méthode B, Machine abstraite, Spécification formelle

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)}
R2= R ; R = {(1, 3), (3, 4)}
Le symbole ; est celui de la composition "en avant".
R3 = R2; R = {(1, 4)}
R4= 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

mercredi 17 juin 2015

Exposé de J.R. Abrial au Collège de France, avril 2015

Je vous signale l'exposé au Collège de France de JR Abrial

http://www.college-de-france.fr/site/gerard-berry/seminar-2015-04-01-17h30.htm

Cette présentation est celle d’un chercheur vieillissant qui porte un
regard historique sur les trente dernières années de son travail.

Il y a deux sortes de chercheurs : les prolifiques et les monomaniaques.
Je fais partie de la seconde catégorie, car j'ai toujours pratiqué le même
genre d’investigations, à savoir la spécification et la construction
vérifiée de systèmes informatisés.

Ce travail, autant théorique que pratique, s’est concrétisé au cours de
toutes ces années dans trois formalismes voisins : Z, B et Event-B (dont
je ne suis pas, loin de là, le seul contributeur). Je vais tenter
d’expliciter comment les idées que contiennent ces formalismes et les
outils correspondants ont lentement émergés de façon parfois erratique.

Je tenterai aussi de préciser les multiples influences qui ont participé à
cette évolution. En particulier, je montrerai comment plusieurs
réalisations industrielles ont permis de progresser dans ce domaine. Mais
je soulignerai aussi les échecs et parfois les rejets de la part de
communautés tant universitaires qu’industrielles.

Pour finir, je proposerai quelques réflexions et approches pour le
financement de recherches telles que celle-ci.

-- 


mercredi 27 mars 2013

Le langage de prototypage me to

H. Habrias

Voir chapitre XI, VDM et me too de H. Habrias, Introduction à la spécification, Masson,1993

EVALUATION D'UNE EXPRESSION

3 * 4;= 12;
{(a, b) | a <- b="" font="">
=  {(1,3), (1,4), (2,3), (2,4)};

OBJET ET OPERATIONS

n == e;

affecte le résultat de l'évaluation de e au nom n.
mise à jour de l'environnement en liant n à l'évaluation de e.

aime == { ("Dudule, "Paulette"), ("Paulette", "Dutonf"), ("Dutonf", "Logique")};=  AIME;
aime;
= {(Dudule, Paulette), (Paulette, Dutonf), (Dutonf, Logique)};
nouveauaime == {("Dutonf", "Bouffe"), ("Dutonf", "Logique")};
= NOUVEAUAIME;
nouveauaime;
= {(Dutonf, Bouffe), (Dutonf, Logique)};
aime == aime union nouveauaime;
= AIME;
aime;
 
= {("Dudule, "Paulette"), ("Paulette", "Dutonf"), (Dutonf, Bouffe), (Dutonf, Logique)};

Vous voulez observer les noms des objets en cours de stockage dans l'environnement

obs;= {NOUVEAUAIME,AIME};

Avons-nous défini des opérations ?

ops;= {};
non !

Les opérations sont définies comme des fonctions

sq(x) = x * x;= SQ;
ops;
= {SQ};

Vous voulez sauver votre environnement dans un fichier.

save("nomfichier");

et recharger ce fichier
 
load("nomfichier");
Nombres, chaînes, etc.
 
obj1 == 1;
= OBJ1;obj1;
= 1;
10;
= 10;
-10.421;
= -10.421;
x == 31;
=X;
-X;
= -31;
is_numer(5);
= TRUE;
is_number("Dudule");
= FALSE;
"Hello";
= Hello;
salut(n) == ["Hello", n];
= SALUT;
salut("Dudule");
= [Salut, Dudule];
is_string("Dudule");
= TRUE;
is_string(["Dudule", "Dutonf"]);
= FALSE;
"Dudule" = "Dutonf";
= FALSE;
"Dudule" > "Dudule";
= FALSE;

6 + 7;
= 13;
23 - 8;
= 15;
7 * 8;
= 56;
40.0 / 3;
= 13.3333333;
13 truncate 3;
= 4;
37 mod 10;
= 7;
true;
= TRUE;
true and false;
= FALSE;
true and true;
= TRUE;
true or false;
= TRUE;
false or (false and false);
= FALSE;
not(false);
= TRUE;
true => true;
= TRUE;

true => false;
= FALSE;
false = false;
TRUE;
true = false;
= FALSE;
["a", {"longue", "complexe"}, "expression"] =
["a", {"longue", "complexe"}, "expression"] ;
= TRUE;
3 /= (2 * 2);
= TRUE;
{1,2,3} /= {3,2,1};
= FALSE;

Conditionnelle

sum(x,y) == if x = 0 then y else 1 + sum(x - 1, y);
= SUM;sum(15,4);
= 19;

Enfin, voici la définition de fonctions !
 
sq(x) == {i*i | i <- font="" x="">
=SQ;sq({3,4,5,6});
= {9,16,25,36);
cp(x, y) == {(p,q) | p <-x font="" q="" y="">
CP;

cpsq(x) == cp(sq(x),sq(x));
= CPSQ;
cpsq({1,2,3});
= {(1,1), (1,4), (1,9), (4, 1), (4,4), (4,9), (9,1), (9,4), (9,9)};

Application de fonction

double(x) == {i * 2 | i<- font="" x="">
= DOUBLE;double({3,4});
= {6, 8);
double(double({3,4}));
= {12, 16};

Lambda expressions
 
(lambda(x,y). (x * x) + (y * y))(2,3)
= 13;

Définitions locales
 
 let n1 == e1,...,nk == ek in e
retourne le valeur de e, évaluée dans un contexte enrichi par la liaison des noms ni aux valeurs ei
La portée des noms n1 à nk est e. Donc l'expression ei ne peut utiliser un de snoms n1 à nk.let x == 3, y == 4 in x + y;
= 7;
a == 2;
= A;
let a == 3, b == a * a in b;
= 4;
mais
let a == 3
in   let b == a * a
      in  b;
= 9;

Et voici les ensembles
 
{"Dudule", "Paulette"};
= {Dudule, Paulette);{};
= {};
a == { "pommes", "poires", "scoubidou"};
= A;
{ x * x | x <- font="">
= {4,16,36};

Avec filtre ?
 
{ x * x | x <- 3="" font="" x="">= {1,4,9};

On a bien sûr toutes les opérations ensemblistes :
union,
intersection
member
difference
subset
card
quantificateur universel :

all n in s . b

quantificateur existentiel

exists n in s .b

Et les relations

bouffe == {("bouillie", "pomme de terre"), ("purée", "pomme de terre")};
= BOUFFE;is_relation (bouffe);
= TRUE;
is_relation (10);
= FALSE;
dom(bouffe);
= {bouillie, purée};
rng(bouffe);
= {pomme de terre);

et le reste , voir feuille Quick Reference Guide
Les Maps

prix == { "radio" ->20, "cassette" ->110, "couteau" ->20};
= PRIX;prix["couteau"];
= 20;

et bien sûr la surcharge (plus exactement, l'écrasement)

m1 overwr m2

Bibliographie :
Software Design and Prototyping using me too (1990)
 by H Alexander, V Jones 

jeudi 11 février 2010

samedi 21 juin 2008

Retraite ...mais ça continue !

L'auteur de ce bloc-notes part en retraite...mais continuera à alimenter ce bloc-notes.