Jean-Raymond
Abrial (1938, 2025)
Jean-Raymond
Abrial est décédé les 26 mai 2025 la vieille de la conférence qui
a eu lieu dans le cadre des Journées Scientifiques de l'université
de Nantes et qui traitait de ses travaux et de leur mise en oeuvre
dans différents domaines.
J.-R
Abrial est né en 1938 à Versailles. Après des études au Prytanée
militaire de la Flèche, il fera l'Ecole Polytechnique. En 1960 il
sera ingénieur du génie maritime. Il sera boursier du gouvernement
français à Stanford University puis au Centre de Programmation de
la Marine où il travaillera sur une version du langage LTR (Langage
Temps Réel). C'est là que Gérard Le Lann, qui a fait partie de
l'équipe ayant conçu Internet, l'a connu. J.-R Abrial est pour lui
"l'un des plus grands informaticiens français ! Peu enclin à
épouser les « modes » qui agitent plus ou moins régulièrement
les communautés scientifiques. Liberté de penser, de créer, et
liberté d'essaimer !".A Grenoble, dans une université qui va
être une des premières en France à développer les enseignements
et recherches en informatique en France, il va à partir de 1969 avec
une équipe de trois personnes créer le système de gestion de base
de données Socrate en moins de deux ans. Il fera appliquer une
démarche qui sera la sienne dans la suite de ses travaux, spécifier
avant de programmer. Son efficacité s'est manifestée par une
réalisation rapide.
En
70-71 il fera à Grenoble un cours original "Structure de données et de
programme, point de vue existentiel".
Lors
du colloque de Cargèse de 1974, il publiera "Data Semantics",
un article qui se retrouvera en tête des bibliographies pendant des
décennies. C'est à Grenoble qu'il publiera les premiers écrits sur
la méthode et notation de spécification formelle Z. Z c'est le
langage ultime et la première lettre de Zermelo. Il utilisera la
théorie des ensembles, sa notation et le langage des prédicats. Z
de Grenoble fut diffusé tout d'abord via le "Meyer Baudoin"
(méthodes de programmation) puis par le "Delobel Adiba"
(bases de données et systèmes relationnels). Socrate fut
immédiatement utilisé à Grenoble dans les filières informatique
et professionnellement via la société Eca-Automation puis à
l'armée, gendarmerie, EDF, SNCF. Il y eut ensuite une nouvelle
version sous le nom de Clio réalisée au sein de la société
Syseca et beaucoup d’autres comme CLIO/SQL, ORCHIS-Base,
ouvertes sur les nouveaux langages d’interrogation. Tony Hoare qui
a assisté à un cours d'Abrial dans les Alpes, l'a fait venir au
Programming Research Group d'Oxford en 1979 pendant deux ans. C'est
là qu'avec d'autres sera réalisé la version connue de Z. La mise
en œuvre de Z chez IBM conduira à restructurer et réécrire des
parties de leur logiciel CICS (Customer Information Control System).
Ce qui vaudra au PRG son premier Queen's award for technology.
Abrial
fera partie de l'équipe Green de CII-Honeywell-Bull dirigée par
Jean Ichbiah qui sera sélectionnée pour définir le langage qui
s'appelera ensuite Ada en mémoire de Ada Lovelace, la fille de Lord
Byron, dite "la première programmeuse de l'histoire". Dans
sa conférence au Collège de France en 2015, conférence toujours en
ligne sur le site du Collège de France, Jean-Raymond raconte comment
il travaillait et ce qui deviendra la méthode B. Dans un article de
1984 de la Royal Society, "La programmation comme un exercice
mathématique", il présente sa méthode "Une conséquence
de ce point de vue est que l'activité de construction de programmes
se transforme en celle de construction de preuves." Il sera
presque tout le temps "consultant indépendant". Il sera
professeur au Cnam à Paris. Il adressait à de nombreux enseignants
et à des personnes préparant un diplôme d'ingénieur Cnam ses
travaux en cours. Et avait développé un outil d'aide au
développement, le B-Tool, d'aide à la démonstration de théorèmes
interactif. Je me souviens qu'il avait traité du cas des élections
à la proportionnelles de 1986, selon la démarche présentée dans
son article. intitulé "Spécifier ou comment maîtriser
l’abstrait", avec une longue citation de Proust qui dénotait
dans le milieu universitaire. Un article très pédagogique. La
méthode B était en gestation. B car "avant C" (l'atelier
B générait de l'ADA et du C), et "avancé".
En
1990, il sera de nouveau à Oxford où chez British Petroleum sera
réalisé le B-Toolkit. En B, on a des machines abstraites et on
prouve que les opérations respectent l'invariant. Par exemple,
l'invariant peut spécifier que l'intersection généralisée des
enveloppes des rames de métro est toujours vide. Il faudra ensuite
préciser comment on calcule ces enveloppes qui évoluent du fait de
la vitesse, du poids des voyageurs). On passe d'une spécification de
machines abstraites à des machines plus proches du logiciel en
faisant ce qui est appelé le raffinement. Dans l'invariant on relie
des variables abstraites aux variables plus concrètes. Il faut alors
faire de la preuve de raffinement. A la fin du processus, on génère
un programme qu'on ne touchera pas. On a fait de la preuve en
construisant le programme et non de la preuve une fois le programme
écrit. Le B-Book publié en 1996 sera sous-titré "Assigning
programs to meaning", un clin d'oeil à la publication de 1967
de Robert Floyd intitulée "Assigning meanings to programs",
article qui est une des sources de B.
En
1990, Guy Laffitte utilisera B et le Btool à l'INSEE pour le
recensement général de la population.
Dans
les années 80 la RATP fera appel à Abrial pour la ligne A du RER,
où doit être installé le premier logiciel de contrôle-commande
sécuritaire jamais mis en œuvre en France. Voici ce qu'il nous en
dit lors de sa conférence du Collège de France.
Claude
Hennebert m'a dit "on voudrait faire un audit technique".
L'audit a duré trois semaines. Je devais répondre à la question
"Les moyens mis en œuvre permettent-ils de garantir que le
produit final correspond bien à sa spécification initiale ? j'ai
dit, je ne peux pas répondre parce que je n’ai pas vu de spécification ". On m'a répondu "Il n'y avait pas de
spécification, alors faites nous un cours de spécification. Et à
la mi-80 la RATP a décidé
de se lancer dans un métro sans conducteur, la ligne 14 dont les
parties critiques ont été développés en B". Avec l'appui d'Abrial,
Alstom décide de développer son propre ensemble d'outils. Et en
1993 la première version du BToolset comprenant un vérificateur de
type, un générateur d'obligations de preuves et prouveur de
théorème pour des logiciels de taille industrielle est réalisée.
Abrial propose alors que la société Digilog, puis Steria et
aujourd'hui Clearsy industrialise ces outils. Aujourd'hui,
l'Atelier-B est disponible gratuitement via le site web de Clearsy.
Deux sociétés faisant du B ont été créées à Aix-en-Provence,
Clearsy et Systerel.
En
1993, Alstom livrera aux métros de Calcutta et du Caire, à la SNCF
et à la RATP les premiers systèmes de contrôle de vitesse de
trains intégrant des logiciels développés avec B. Aujourd'hui de
nombreux métros dans le monde ont du B dans leur logiciel.
B
sera utilisé au centre de recherche de Gemplus à Gemnos pour la
carte à puce.
En
1996 lors de la première conférence internationale sur B à Nantes,
Abrial fera un exposé sur l'extension de B sans le changer pour
développer des systèmes distribués. Ce sera le début du "B
événementiel". En 2010 sera publié Modeling in Event-B,
System and Software Engineering.
Cette
année aura lieu la dix-huitième conférence traitant de B à
Düsseldorf. Y sera présenté par son son co-auteur un article
rédigé en 2019 avec Abrial.
De
2004 à 2009, Abrial sera en poste à l'Ecole Polytechnique de Zûrich
et avec une équipe développera la plateforme Rodin.
En
2006 il sera reçu membre de l'Academia Europea et en 2008 docteur
pour l'honneur de l'Université de Sherbrooke.
En
2017 il recevra en présence du président chinois Xi Jinping
l'International Scientific and Technological Cooperation Award.
Lors
de l'introduction de sa conférence au Collège de France, il dira :
"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"
Jean-Raymond
aura été un chercheur, un praticien dont la démarche, la
pédagogie, les publications ont motivé bien des universitaires et
praticiens de par le monde.
Z puis B furent la "lingua franca" de beaucoup
d'enseignants. Jean-Raymond Abrial était aussi un alpiniste et un
marcheur aussi bien de Marseille à Cassis via les calanques qu'à
travers le Sahara.
Henri
Habrias
Articles
