Jean-Raymond Abrial (1938, 2025) English

 

 Jean-Raymond Abrial (1938, 2025)

Jean-Raymond Abrial died on May 26, 2025, the day before the conference held as part of the Scientific Days of the University of Nantes, which discussed his work and its application in various fields. 

 

J.-R. Abrial was born in 1938 in Versailles. After studying at the Prytanée militaire de la Flèche, he attended the École Polytechnique. 

 

In 1960, he became a marine engineer. He received a French government scholarship at Stanford University and then at the French Navy Programming Center, where he worked on a version of the LTR (Real-Time Language) language. It was there that Gérard Le Lann, who was part of the team that designed the Internet, met him. For him, J.-R. Abrial is "one of the greatest French computer scientists! He is reluctant to embrace the "fashions" that more or less regularly shake up scientific communities. Freedom to think, to create, and freedom to spread! " 

 

In Grenoble, at a university that would become one of the first in France to develop computer science teaching and research, he and a team of three created the Socrate database management system in less than two years in 1969. He would apply an approach that would be his own in his subsequent work: specify before program. Its effectiveness was demonstrated by the short time taken to complete the project quickly. François Peccoud, initiator of the Socrate project, wrote that J.R. Abrial "set himself a deadline of one month to write a specification, imagining that it would consist of 100 procedures contained in a 100-page document. Then, three months were needed for the team to understand and appropriate the specification, and only then would we move on to programming" (Jean Ricodeau's thesis).

In 1970-71, he gave an original course, "Data and Program Structure, an Existential Point of View."
At the 1974 Cargèse conference, he published "Data Semantics," an article that would be at the top of bibliographies for decades. It was in Grenoble that he published the first writings on the method and notation of formal specification Z. Z is the ultimate language and the first letter of Zermelo. He would use set theory, its notation, and the language of predicates. Z de Grenoble was first disseminated via "Meyer Baudoin" (programming methods) and then by "Delobel Adiba" (databases and relational systems). Socrate was immediately used in Grenoble in the IT sectors and professionally via the company Eca-Automation and then in the army, gendarmerie, EDF, SNCF. There was then a new version under the name Clio produced within the company Syseca. As Christian Jullien writes, "even in SQL, the Socrates databases could be used, along with many others like CLIO/SQL and ORCHIS-Base, which were open to new query languages." 

 

Tony Hoare, who attended a lecture by Abrial in the Alps, brought him to the Programming Research Group in Oxford in 1979 for two years. It was there that, along with others, the well-known version of Z was developed. IBM's implementation of Z led to the restructuring and rewriting of parts of their CICS (Customer Information Control System) software. This earned the PRG its first Queen's Award for Technology. 

 

Abrial was part of the CII-Honeywell-Bull Green team led by Jean Ichbiah, which was selected to define the language that would later be called Ada in memory of Ada Lovelace, Lord Byron's daughter, known as "the first female programmer in history." In his lecture at the Collège de France in 2015, a lecture still in online on the Collège de France website, Jean-Raymond describes how he worked and what would become the B method. In a 1984 Royal Society article, "Programming as a Mathematical Exercise," he presents his method: "A consequence of this point of view is that the activity of building programs is transformed into that of building proofs." He was almost always an "independent consultant." 

 

He was a professor at the Cnam in Paris. He sent his work in progress to many teachers and people preparing for a Cnam engineering degree. And he had developed a development aid tool, the B-Tool, to help with interactive theorem demonstration. I remember that he had dealt with the case of the 1986 proportional elections, according to the approach presented in his article entitled "Specifying or how to master the abstract," with a long quote from Proust that stood out in the academic world. A very educational article. The B method was in the making. B because "before C" (the B workshop generated ADA and C), and "advanced."

In 1990, he returned to Oxford, where the B-Toolkit was developed at British Petroleum. In B, we have abstract machines and we prove that operations respect the invariant. For example, the invariant can specify that the generalized intersection of envelops 4,307 / 5,000
of subway trains is always empty. We will then need to specify how we calculate these envelopes, which change due to speed and passenger weight. We move from a specification of abstract machines to machines closer to software by performing what is called refinement. In the invariant, we link abstract variables to more concrete variables. We then need to prove the refinement. At the end of the process, we generate a program that will not be touched. We performed the proof while building the program, not the proof once the program was written. The B-Book published in 1996 will be subtitled "Assigning programs to meaning," a nod to Robert Floyd's 1967 publication "Assigning meanings to programs," an article that is one of the sources for B.

In 1990, Guy Laffitte used B and the Btool at INSEE for the general population census. 

 

In the 1980s, the RATP called on Abrial for RER Line A, where the first safety-related instrumentation and control software ever implemented in France was to be installed. Here's what he told us about it during his lecture at the Collège de France.
Claude Hennebert told me, "We'd like to conduct a technical audit." The audit lasted three weeks. I had to answer the question, "Do the resources implemented ensure that the final product corresponds to its initial specifications?" I said, "I can't answer because I haven't seen any specifications." I was told, "There was no specification, so give us a specification course." And in the mid-1980s, RATP decided to embark on a driverless metro, line 14, whose critical parts were developed in B. With Abrial's support, Alstom decided to develop its own toolset. And in 1993, the first version of the BToolset, including a type checker, a proof obligation generator, and a theorem prover for industrial-scale software, was released. Abrial then proposed that Digilog, then Steria, and now Clearsy, industrialize these tools. Today, Atelier-B is available free of charge via the Clearsy website. Two B companies were created in Aix-en-Provence: Clearsy and Systerel.

In 1993, Alstom delivered the first speed control systems to the Calcutta and Cairo metros, the SNCF, and the RATP. of trains integrating software developed with B. Today, many metros around the world have B in their software.

B will be used at the Gemplus research center at Gemnos for smart cards.

In 1996, at the first international conference on B in Nantes, Abrial gave a presentation on extending B without changing it to develop distributed systems. This marked the beginning of "event-based B." In 2010, Modeling in Event-B, System and Software Engineering was published.

This year, the eighteenth conference on B was held in Düsseldorf. Dominique Cansell presented a paper written in 2019 with Abrial.

From 2004 to 2009, Abrial worked at the Zurich Polytechnic School and, with a team, developed the Rodin platform.

In 2006, he was awarded a membership in the Academia Europea and in 2008, he received an honorary doctorate from the University of Sherbrooke.

In 2017 In the presence of Chinese President Xi Jinping, he will receive the International Scientific and Technological Cooperation Award.

 
In the introduction to his lecture at the Collège de France, he will say: "There are two kinds of researchers: the prolific and the monomaniacal. I belong to the second category because I have always practiced the same kind of investigation, namely the specification and verified construction of computerized systems."

Jean-Raymond was a researcher, a practitioner whose approach, pedagogy, and publications have motivated many academics and practitioners around the world. Jonathan Bowen wrote that Ib Holm Sorensen, who worked with J.R. Abrial at Oxford, was a "doer." Two "doers" shared the same office at Oxford.
Z and then B were the "lingua franca" for many teachers. Jean-Raymond Abrial was also a mountaineer and hiker, from Marseille to Cassis via the calanques, as well as across the Sahara and other regions of the world.

 

Henri Habrias