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. --

Mes livres

http://saintyrieixlaperche.wordpress.com/2014/12/02/moi-aussi-jai-publie-des-livres/

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 

Structures de données et méthodes formelles (génie logiciel, méthodes formelles, programmation, algorithmes, mathématiques discrètes, logique, méthode B)

Structures de données et méthodes formelles
Marc Guyomard
Springer, 2011


http://www.springer.com/computer/book/978-2-8178-0199-5

Mes livres chez Teknea

Suite à une demande

http://www.teknea.com/Informatique.HTM

Retraite ...mais ça continue !

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

Les notes de TD et de "DS" sont affichées

J'ai noté largement (j'ai considéré parfois que la réponse, bien qu'ayant aucun sens, était forcément une étourderie comme tout le monde en fait. Et j'ai mis la note max à la question. Bof ! on ne donne pas un diplôme de médecin, n'est-ce pas. Et il faut être productif.)

Il se peut qu'il y ait des erreurs de recopie de notes. Vous pouvez venir vérifier vos copies et dossiers. M'adresser un courriel pour un rdv.

Il me reste à refaire ce cours en Bac+4 dans deux mois. Et ce sera fini pour moi de ce cours au moins dans notre bonne université.

Peut-être une autre vie professionnelle ailleurs ...

Heureusement, les écrits servent à d'autres. Ce courriel semble le dire :

"
Bonjour,

Juste un petit mot de félicitations pour
votre excellent livre sur la 
mesure du logiciel. Je l'avais lu il y a
7 ou 8 ans mais je l'ai 
redécouvert cette semaine durant le calme
d'août... Il est simple et 
agréable à lire. J'ai eu votre email via
google et suis arrivé sur IUT 
de Nantes. Vos élèves ont de la chance.
Bravo.

XXXXXXX
Direction du Pilotage des Systèmes 
d'Information
Groupe XXXXXX

Je n'ai donc pas perdu tout mon temps
et volé ma paye.

Il s'agit d'un très grand groupe qui
vient de signer un très très
gros contrat dont nous a parlé la presse.

Si j'ai des notes de 0,1 en TD j'ai mis
un 19,9 à un étudiant.


Pour clore ce bloc-notes, cette citation
extraite de

Erik Orsenna, Voyage au pays du coton,
Petit précis 
de mondialisation, Le livre de poche

"- Comment vois-tu l'avenir de la Chine ?
- Pas différent de son passé. Mon pays
a toujours été la première puissance du monde. 
Sauf durant les deux derniers siècles.
Dans vingt ans,
elle aura recouvré son rang.
- Et vous ne craignez pas la concurrence
indienne ?
- L'Inde est trop démocratique. Elle y
perd beaucoup d'énergie.
Bo nous parle souvent de Paris , où il
est resté 6 ans [...]
Une question le préoccupe :
- Pourquoi, en France, n'aimez-vous pas
les enfants ?
Je m'étonne, me récrie, le prie de développer.
- En France, vous ne travaillez pas
assez. Donc vous préparez mal
l'avenir de vos enfants.
Et il enfonce le clou :
- Chaque année, la dette de la France
augmente. Seuls ceux qui
ne travaillent pas assez s'endettent.
Et qui doit rembourser ? 
Les enfants.
Que répondre? "

page 275-276