Velo - Vérification pour l'Environnement et le LOgiciel

Cette page est en lecture seule. Vous pouvez afficher le texte source, mais ne pourrez pas le modifier. Contactez votre administrateur si vous pensez qu'il s'agit d'une erreur.
Ce que je dois à Jean-Raymond Abrial
July 24, 2025
[[https://jean-raymond-abrial.blogspot.com/2025/07/ce-que-je-dois-jean-raymond-abrial.html|source ]]

====== Quand ai-je découvert Jean-Raymond Abrial ? ======

Peut-être bien que c'est quand j'ai fait acheter les actes de la conférence de Cargèse et que j'ai lu son article **//Data Semantics//**. Ou est-ce lors de la lecture des publications de la DER-IMA d'EDF (située à Clamart) ?

Ce qui est sûr c'est que j'ai découvert Z dans le Meyer Baudoin, Méthodes de Programmation chez Eyrolles, puis dans le Delobel Adiba, Bases de données chez Dunod.

Quand j'ai débuté en "informatique de gestion" (en I.U.T "Informatique") je trouvais que ce que je lisais était bien peu "scientifique". "Information" "donnée" "rubrique" etc. 

Pour "donnée" j'ai appris les théorèmes de Jean-Louis Rigal qui était prof à l'Université Dauphine. Facile : Th1, "Une donnée n'est pas donnée" car c'est le résultat d'une abstraction, Th 2. "Une donnée n'est pas donnée" car une fois donnée, ce n'est plus une donnée (elle ne change plus l'état de vos connaissances. Oh ! je viens d'introduire un autre terme !). Ce n'est plus un scoop. Les journalistes l'ont bien compris. Th. 3 "Une donnée n'est pas donnée", ça coûte", ce n'est pas donné ! même avec le Oueb. Y a quelqu'un qui paye.

En 1970, j'ai lu et relu "//La science informatique//" de Jacques Arsac. J'avais au moins la différence "information"/ "connaissance" (selon les définitions de J. Arsac).  

Paul Namian du Cnam avait écrit un article dans la revue Automatisme tome  XI, n°10, octobre 1966 "//Approche théorique du traitement des informations administratives//" essayant lui aussi d'y voir clair. J'avais la chance d'être dans les mêmes locaux que l'ENSM (devenu École Centrale) ! Claude Pair "//Les structures de l'information//" (Alès, 1971)

On parlait de "méthodologie" (alors qu'on n'étudiait pas des méthodes, aujourd'hui méthodologie c'est plus chic que "méthode" ! qui oserait publier une revue "Travail et Méthodes" (où j'ai pas mal publié). On parlait d'"analyse", puis ce fut "conception", analyse conceptuelle, le mot "structure" était partout, modèle aussi. Mais c'est Michel Serres invité à Nantes par Jean-Louis Gardies qui nous a éclairé par l'exemple de la fable Le loup et l'agneau, sur Structure et Modèle. 

Ce qui m'avait rappelé l'école primaire aux casernes (bé oui, je suis allé très jeune aux casernes - on utilisait le pluriel - à Saint-Yrieix-la-Perche !). Un instit (on dit maintenant "professeur des écoles") nous avait demandé "que voulez-vous faire plus tard ?" Un élève a répondu "expert comptable" (son père était comptable). Un autre a alors répondu "expert coiffeur". Dans les années 80, il aurait répondu "coiffeur concepteur" et de nos jours je vois des enseignes avec "Coiffure Concept" et autres variations.

Puisque je parle d'instit, parlons aussi de profs. C'est le prof de philo qui nous a parlé des tables de vérité, et des ensembles. Certes ce n'est pas allé loin ! Il avait expliqué l'ensemble vide par le symbole du panneau interdisant le stationnement.

J'ai parlé de Z. Mais il y a eu aussi le SGBD (je fais un anachronisme, on n'utilisait pas encore le terme) Socrate de J.R. Abrial, **Socrate** aussi découvert dans le Delobel Adiba. Socrate qui était utilisé sous ce nom puis sous celui de Clio à l'arsenal d'Indret pas loin de Nantes. 

A mon arrivée à Nantes en 1971 j'ai enseigné la méthode Cantor. Elle n'avait rien à voir avec Cantor. Mais allait de l'étude de l'existant jusqu'à la génération de code Cobol. Je l'avais apprise en étant en stage chez ICL qui l'utilisait. 

En 1982, dans la bibliographie de "//Présentation du  projet Thérèse//" de J.M. Pendibidu, TSI, Vol. 1, N°3, mai-juin 1982, pp. 253-257, on trouvait "Yaka, Fer, Setou, Bon et Yapad Bug, A metatheory of extented alfa-romero calculus : Very private communicatiob (1979). On reparlera de TSI plus loin. Rappelons que Georges Perec a publié 1974 en Experimental Demonstration of the tomatotopic organization in the Soprano (Cantatrix sopranica L.). Tout le monde y a noté la longue bibliographie. Jean-Raymond n'en faisait que de toutes petites ! Mais il lisait les textes mis dans ses bibliographie.

Suite à mes lectures sur Z, j'ai acheté le premier tome de **Bourbaki** avec sa reliure cartonnée  toilée, faite pour durer. Je n'ai pas réussi à aller bien loin (mais j'ai dû aller plus loin que dans Ulysse du gars de Dublin ! car cet Ulysse c'est pas la joyce !). Mais il y a à la fin, la Note historique et le petit fascicule de résultats. Et ça j'ai pu le lire. C'est bien plus lisible malheureusement que certains livres de classes qui ont été diffusés quand on a lancé la réforme des maths dans l'enseignement. Jean-Raymond  parle de ce fascicule dans sa conférence au Collège de France.

Peut-être est-ce à cette époque que je me suis intéressé au langage **SETL** qui a été développé à l'université de New-York. Ma mémoire me dit que c'est par des Français. Wikipedia (anglais, traduit en français) ne me le dit pas. J'ai dû faire un TD aux étudiants en SETL.

Je ne sais plus si j'ai enseigné Z (le Z d'Oxford), avant ou après avoir découvert NIAM (Nijssen Information Analysis Method) de Control Data en Europe. NIAM c'est l'utilisation du modèle relationnel binaire. J'ai publié le premier livre au monde (!) sur NIAM (mais traitait aussi du modèle relationnel n-aire et autres) en 1988. J'avais fait un an de délégation au CMILACO (Crédit Mutuel Informatique Loire Atlantique Centre Ouest) où NIAM était utilisé. En 1985, Jean-Pierre Giraudin et Monique Chabre-Peccoud avaient publié dans Bigre+Globule "P//our une réhabilitation du modèle relationnel binaire//". C'est Jean-Pierre qui sauvera la conférence de 2025 en nous préparant un exposé sur Z, Socrate à Grenoble.

**1984** J.Raymond publie dans la revue TSI, "//Spécifier ou comment maîtriser l'abstrait//", Vol. 3, N°3, pp.201-219. L'article débute avec un encadré d'une citation de Proust. Normal pour celui qui avait appelé un SGBD Socrate. Mais ça ne se fait pas ! Il faut lire l'encadré de présentation de l'article par un universitaire !  L'article est introuvable de nos jours. Appel à tous ! Mais j'ai gardé l'encadré de présentation sur un transparent. 

**1985** Jean-Raymond fait un cours au CEPIA à Rocquencourt. Guy Laffitte de l'INSEE l'écoute. Et fréquentera alors la rue des plantes à Paris où habite Jean-Raymond. On aurait pu se croiser à l'un de ces deux endroits. C'est sans doute en 1985 que j'ai visité Jean-Raymond rue des plantes. Je me souviens qu'avant le dîner il m'avait montré son booster de preuve. Je me souviens aussi qu'il faisait de longs séjours à Oxford à l'époque, suffisamment longs m'avait-il dit pour s'imprégner de l'accent anglais. Dans le B-Book, Jean-Raymond a écrit : "//G. Laffitte influenced this work by his careful reviews, his accurate criticisms, and the sometimes very serious rearrangements he proposed for some of the mathematical developments of this book//"

1986 Je lis dans la bibliographie de mon //Introduction à la spécification// (Masson), 1993, A small case study in program design, Nov., non publié. Ce doit donc être la première année des échanges avec Jean-Raymond.

En 1987 Je lis "Le cas des élections à la proportionnelle en LCP, Programmation déductive, Méthode de J.R. Abrial", IUT de Nantes. C'est Claude Pair qui avait traité le cas en programmation déductive. Pour LCP c'était Alain Coulon et M. Koutchouk de Bull.  Et aussi "A formal introduction to abstract machines", 4 May 87, publié par l'auteur

Si je ne me trompe ce sera en **1987** qu'un diplôme d'ingénieur Cnam sera passé avec comme sujet Quatre méthodes de spécification, SADT, Merise, Formalisme F1, Spécification mathématique d'Abrial, Application à un exemple, le réveil électronique. Jean-Raymond fournissait ses rédactions. Un jour, peut-être celui de la soutenance, il est venu avec ses outils nous faire une démonstration. Il devait alors être en poste au CNAM à Paris.

En **1988**, B User manual, Tech. Report, Programming Research Group Oxford University 

En **1989**, en septembre, je crois me souvenir que c'est Guy Laffitte qui est venu de pas loin lors de mes troisièmes journées MOACSI pour exposer le texte de Jean-Raymond "//Une approche formelle de la construction des logiciels//". 

**1996** (ou 95 ?) Le livre dont je parle plus loin a été publié en 96. Je suis allé faire un cours sur NIAM à l’École Polytechnique Fédérale de Lausanne. Et je me souviens que J.R. Abrial avait reçu une demande pour aller y enseigner B. Une collègue y était allé à sa place. Le cours a été publié dans un livre, Génie logiciel : principes, méthodes et techniques, Presses polytechniques et universitaires romandes. et un collègue de l'EPFL m'avait envoyé mon cours réécrit avec la notation mathématique. Ce qui m'a rappelé un cours que j'avais fait à des profs de maths sur la méthode Merise. A la pause, un est venu me réécrire les MCD (Modèles Conceptuels de Données) en notation mathématique. Je lui ai confirmé qu'il avait tout compris ! 

En NIAM on utilise une notation graphique avec deux symboles pour exprimer les 16 cas de relations binaires, le V qui coupant une ligne donne le quantificateur universel (le "pour tout") pour la contrainte de totalité, et la ligne pour la contrainte d'unicité (comme dans les relations n-aires à la Codd on souligne la clé), et quelques autres pour les contraintes d'égalité, inclusion entre relations, domaines, codomaines. Ce qui est important c'est qu'on doit écrire au mieux deux phrases sujet verbe complément pour la relation et son inverse. Il est ensuite facile de passer à un "modèle relationnel n-aire" qu'on n'appelle pas en NIAM, un "modèle logique" (pourquoi "logique" ! !), mais un "modèle regroupé". 

Je vois que dans mon livre de 88 je cite //Data Semantics// 1974 et "//La preuve dans les spécifications//" in "//Prototypage et spécifications de logiciels//", Journées Afcet, Insa Lyon, janvier 1987. Je note que Nijssen était un des organisateurs de la conférence de Cargèse.

En 1993 avec un collègue philatéliste nous faisions la spécification du Catalogue Yvert et Tellier en Merise, Niam et Z.

Un jour un collègue de l'université de Teesside à Middlesbrough (la ville qui a gardé son pont transbordeur alors que Nantes l'a perdu) a fait le tour des universités où on enseignait Z. Il est allé à Grenoble et est venu à Nantes. Z était la lingua franca de plusieurs enseignants. Via Erasmus il y a eu plusieurs réunions d'enseignants et d'étudiants de différents pays où on a fait des schémas Niam et ensuite du Z. Et au U.K du CCS de Robin Milner. Ensuite les collègues de Teesside (Bill Stoddart, Steve Dunne, Andy Galloway) ont enseigné B et ont publié sur B. Et sont allé voir Jean-Raymond à Marseille.

En **1994**, on est à deux ans de la publication du B-Book. Jean-Raymond Abrial vient à Nantes pour faire cours aux étudiants d'APPC (est-ce que là encore je fais un anachronisme ? Année Post Premier Cycle a fait suite à "Année Spéciale"), cours qui sera enregistré en vidéo à l'IUFM (Institut Universitaire de Formation des Maîtres) de Nantes qui disposait d'un studio et diffusé par l'IUT de Nantes et par l'éditeur Teknea de Toulouse. Il y a 6 cassettes VHS d'introduction à B et 8 d'études de cas, accompagnées de la copie des transparents. Un cours très pédagogique. Jean-Raymond a utilisé les papygrammes. A ce sujet je me souviens que quand fournissais aux étudiants la notation Merise, je leur disais de demander à leurs interlocuteurs en entreprise de leur fournir les papygrammes. Et qu'ils se rendraient compte que .... Quand je les retrouvais dans le train, ils me rappelaient mon conseil. Et que j'avais raison. Ils l'avaient testé. J. Raymond a aussi très bien expliqué le théorème du raffinement. J'ai pu alors faire un cours B.

Je me souviens que je lui avais parlé de la notation simple de Niam. Mais la notation Z était alors largement diffusée et même avait fait l'objet d'une norme. Lors de la conférence de Nantes de 2025, je l'ai présentée. Elle n'utilise que le trait -------- , le V et les pointes > ou <. Moins une relation est contrainte, moins on a de symbole. Une relation quelconque est représentée par ------. La plus contrainte par <-V---V->. Nous l'avons  appelée Oc, en référence à Occam et son rasoir ... et à l'occitan. 

**1995** J'avais prévu avec Jean-Raymond la première conférence internationale sur B à Nantes. Mais la publication du B-Book était en retard. Alors j'ai changé le nom de la conférence. Ce fut en court Z2B (c'était la mode de l'utilisation des 2 pour faire du to), en long "//Z Twenty Years On - What is its Future ?//" ISBN 2-906082-19-8 

A l'occasion j'ai de cette conférence j'ai créé l'association APCB, Association de
Pilotages des Conférence internationales B.

**1996** En novembre c'est la **1st Conference on the B Method** à Nantes, actes ISBN 2-906082-25-2

**1995-1996**, c'est aussi les années du **BUG**, B User Group fréquenté par les utilisateurs de l'Atelier B. Je me souviens de Ranan Fraer qui dépannait beaucoup de personnes. J'ai retrouvé Ranan à l'Ecole d'été EDF, CEA, INRIA au château de Bréau-Sans-Nappe du 12 au 23 juin 1995 où Fernando Mejia a distribué un document La Méthode et le Langage B. Ranan était sur l'Atelier B, jour et nuit. Et j'ai appris de lui que c'était la première fois qu'il avait l'atelier B entre les mains ! Sur sa [[https://www-sop.inria.fr/croap/personnel/Ranan.Fraer.html|page]] (toujours disponible : c'est rare !) je lis :

"//Ranan Fraer Formal development in B of a Minimum Spanning Tree Algorithm distinguished with the "Best Paper Award" at the First B Conference, Nantes(France), November 1996.//"

Il a donc dû repartir avec le B-Book ! 

et "//I'm also an enthusiastic supporter of Jean-Raymond Abrial's B method. There's a growing interest in B, as it has been already successfully applied on several large-scale industrial projects in France and UK//" 

**1996** C'est l'année du //Steam Boiler Control Specification//, au château de Dagsthul au nord de la Sarre. Et de la **première conférence internationale B à Nantes**. Jean-Raymond y annoncera ce qui deviendra le B événementiel avec son exposé intitulé : "//Extending B without changing it (for developing distributed systems)//".

En **1997**, à l'AFADL Toulouse, J.L. Lanet intervient suite à l'exposé de Jean-Raymond.  Gem+ va utiliser B pour la carte à puce. Et plus tard, j'irai passer un week-end à Marseille chez Jean-Raymond après la soutenance de stage d'un étudiant de l'IUT à **Gem+**. Je n'ai pas oublié. Lors de la soutenance il y avait des thésards qui ont découvert que l'autre étudiant... était en IUT !  J'ai aussi découvert les calanques en suivant Jean-Raymond. On est allé jusqu'à la fac de Luminy et on a pris le bus pour revenir. Quand on est arrivé au Vieux port, j'ai eu bien des difficultés à marcher. Le lendemain je l'ai passé allongé. Et Jean-Raymond est reparti dans les calanques le matin. Il venait de faire une expédition dans le désert. Etait-ce la  méharée Tamanrasset-Djanet particulièrement éprouvante où dès le premier jour un des membres du groupe est mort et dont le corps a dû être transporté pendant toute l'expédition ?

En **1997**, le département informatique de l'IUT de Nantes a publié le livre "//La Méthode B, Concepts, Démarche, Exemples d'applications//" de Karl Emeriau, ISBN 2-906082-26-0, rédigé suite à son mémoire d'ingénieur CNAM. Karl a été autodidacte en B grâce au B-Book. Toutes les applications sont des applications dites "de **gestion**" réalisées avec l'Atelier B jusqu'au code C généré automatiquement.

**1997** c'est aussi l'année de la 1st IEEE International Conference on Formal Engineering Methods qui a eu lieu à Hiroshima (M.G. Hinchey, Shaoying Liu, Eds).  J'avais envoyé un papier rédigé avec un collègue "//Formal Specification of Dynamic Constraints with the B Method//". Je savais que nous avions un point qui posait problème (un théorème à prouver il me semble). Un jour j'ai reçu un appel de Jean-Raymond. J'étais honteux. Je savais qu'il était membre du comité de programme. Immédiatement je lui ai dit, je n'aurais pas dû envoyer le papier. Il a un problème. Mais Jean-Raymond m'a dit "//je t'appelle pour te dire qu'il suffit de ...//" , une toute petite correction, mais essentielle ! J'ai remercié un "reviewer" dans l'article en tout anonymat. J'ai dû annuler mon déplacement à la "dernière minute". J'aurais retrouvé au Japon, plusieurs amis anglais que je me suis fait via Z puis B.

En **1998**, Claude Boksenbaum organisera la deuxième conférence B à Montpellier en avril.  Didier Bert sera l'éditeur des actes, les premiers dans les LNCS de Springer-Verlag.

En **2000** ce sera la première conférence des utilisateurs de B et Z à York en septembre. Les éditeurs seront Jonathan Bowen, Andy Galloway et Steve King. 

En **2001**, je publierai "//Spécification formelle avec B//", Hermes Lavoisier,  ISBN 2-7463-0302-2, avec la collaboration de Jean-Yves Lafaye et Marie-Laure Potet, avec un Avant-propos de Fernando Mejia (Responsable Méthodes et Outils de Développement Logiciel, Alstom Transport Signalisation) qui commence ainsi :

"//Je faisais depuis quelques temps des expériences d'utilisation de méthodes algébriques de spécification, dans ce qui s'appelait à l'époque Bull Systèmes, lorsque j'ai découvert en 1985 ou 1986, à l'occasion d'une formation données par Jean-Raymond Abrial, ce quelques années plus tard deviendrait le langage et la méthode B. Et ce fut un véritable coup de foudre !//" 

Il nous raconte l'histoire de B qu'il a vécue. 

En **2003** ce sera la 3e conférence des utilisateurs de Z et B à Turku en Finlande. Turku où exerçait  Ralph-Johan Back à Abo University qui est souvent cité dans les articles de Jean-Raymond. C'était en juin, époque où les nuits ne sont pas sombres.A noter que c'est une université de langue suédoise. Bien sûr nous y avons retrouvé Jean-Raymond et bien d'autres.


J'ai conservé les échanges sur le B Forum piloté par l'INRETS forum B de 2004 à 2008. Voici les noms des participants dont j'ai conservé les messages :  Michael Leuschel (HH Univ. Dusseldorf, Samuel Colin (Loria), Simão Melo de Sousa (Universidade da Beira Interior), Guy Vidal-Naquet (Supelec), Georges Mariano (INRETS), Marc Guyomard (Enssatt, Lannion), Steve Dunne (Univ. Teesside), Dominique Cansell (Loria), Daniel Zingaro (McMaster Univ.), Ken Robinson (UNSW Australia), Ib Holm Sorensen (BB-Core), Elisabeth Ball (Cse Sotton), Jeremy L. Jacob (Univ. York), Yann Zimmermann (Keesda), 

**2004** Début du projet Rodin avec Laurent Voisin. Jean-Raymond est prof à l’ETH Zurich jusqu'en 2009 où il travaillera sur Rodin avec Laurent Voisin et d'autres. Il en parle dans sa conférence au Collège de France.

**2008** En octobre je partirai en retraite. Et organiserai la conférence  The B method, from research to teaching où sera Jean-Raymond.

En 2008 ce sera la première conférence ABZ à la British Computing Society à Londres 

En **2009**, aura lieu la deuxième conférence  The B method, from research to teaching.

**2014 ** J'irai à la conférence de Toulouse ABZ et j'y retrouverai Jean-Raymond qui rentrait de Chine. Il y avait aussi bien sûr Egon Börger (il n'a pas dû en rater une) - qui fut prof invité à Nantes pour quelques mois - Leslie Lamport et Tony Hoare. Quand je suis allé visiter avec les petits-enfants le musée de l'aviation de Toulouse j'ai reconnu le restaurant du dîner de gala. 

**2015 ** Conférence de Jean-Raymond au Collège de France. Je me souviens qu'il m'avait raconté qu'on lui avait volé son ordinateur portable avant la conférence.

**2022** Ce sont mes derniers échanges par courriels avec Jean-Raymond. Il venait de m'apprendre qu'il était en fauteuil roulant et était dans un établissement adéquat. Il lisait les Essais de Montaigne et s'intéressait à la civilisation japonaise. Je lui ai proposé d'aller le voir mais il m'a répondu qu'il n'était pas bien. Dans son exposé à ABZ 2025, Dominique Cansell termine par deux photos prises lors de ses deux dernières visites de Jean-Raymond. C'était en 2022. Mais Dominique a communiqué avec Jean-Raymond les années suivantes.

Le **25 mai 2025** Ce sera la conférence //J.R. Abrial, a pioneer in the scientific development of computer languages and formal methods and their large-scale application in industry// dans le cadre des Journées Scientifiques de l'université de Nantes. Nous apprendrons le 3 juin le décès de Jean-Raymond la veille des journées.

et du 10 au 13 juin 2025 a eu lieu la  conférence ABZ où Dominique Cansell a présenté un travail fait avec Jean-Raymond il y a quelques années . C'était **30 ans après la première conférence sur  Z et B de Nantes** ! 

Et je ne m'imaginais pas il y a un an que je publierais à presque 79 ans un article sur B dans une conférence ! "//Formal Modelling of Information System Evolution using B//" Un article retrouvé quand j'ai préparé la conférence sur Jean-Raymond. Le collègue a dû se remettre à l'Atelier B car il ne restait que des bouts de specs B. Et les outils ont évolués depuis 2008 ! L'article traite d'applications où les règles changent selon des phases. C'est par exemple le cas de l'année universitaire. C'est aussi le cas d'évolutions de la loi. 

**Merci Jean-Raymond pour tout ce que tu m'as appris de Socrate, à Z, à B, à Event-B, à Rodin, pour ta pédagogie, pour avoir adressé tes travaux à tant de personnes, pour ton accueil que ce soit à Paris ou à Marseille. Grace à toi, j'ai eu des relations avec de nombreuses personnes qui elles aussi disaient à quel point tu leur as apporté. Grace à toi, je n'ai pas travaillé, j'ai pris du plaisir.** 

Henri Habrias
Velo - Vérification pour l'Environnement et le LOgiciel

Outils pour utilisateurs

Outils du site

Outils de la page
