A note on Jean-Raymond Abrial (1938–2025) by Jonathan Bowen, An appreciation of Jean-Raymond Abrial by Henri Habrias

 A note on Jean-Raymond Abrial (1938–2025)
by Jonathan Bowen

We have the sad news to report that Jean-Raymond Abrial passed away on 26 May
2025. Jean-Raymond was the progenitor and inspiration for not just one, but two
major formal methods, namely the Z notation and the B-Method. He was a modest
and independent researcher, admirably spanning theory and practice. He deserves
much greater appreciation of his achievement than he has perhaps received during
his lifetme. As a small tribute, I have updated Jean-Raymond’s Wikipedia page
and created a new page [7] for his 1996 magnum opus, The B-Book [1], after
realising that I reviewed the book in 1997 [3].
We include an appreciation and biographical summary of Jean-Raymond’s
achievements below. For the future, we intend to have a longer set of memories
about Jean-Raymond by his colleagues in the next issue of FACS FACTS, along
the lines of the celebratory set of contributions for Tony Hoare’s 90th birthday in
2024 [5]. Please contact the FACS FACTS editors if you would like to contribute.

 

An appreciation of Jean-Raymond Abrial
by Henri Habrias
Jean-Raymond Abrial died on 26 May 2025, the day before a conference held as
part of the Journ´ees Scientifiques at the University of Nantes, which focused on
his work and its implementation in various fields.
1
J.-R Abrial was born in Versailles, France, in 1938. After studying at the Prytan
´ee Militaire de la Fl`eche, he attended the Ecole Polytechnique. In 1960, he
became a marine engineer. He was awarded a French government scholarship to
Stanford University, then to the Centre de Programmation de la Marine, where he
worked on a version of the LTR language (Real Time Language). It was there
that G´erard 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!”
Not inclined to embrace the “fashions” that more or less regularly agitate scientific
communities. In Grenoble, at a university that was to be 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, starting
in 1969. He applied the same approach to his subsequent work, specifying before
programming. His efficiency was demonstrated by his rapid implementation.
In 1970–71, he gave an original course on “Data and program structure, existential
point of view”. At the Carg`ese symposium in 1974, he published “Data Semantics”,
an article that would top bibliogaphies for decades. It was in Grenoble
that he published the first papers on the Z formal specification method and notation.
Z is the ultimate language and the first letter of Zermelo. He used set theory,
its notation and the language of predicates. Z from Grenoble was distributed first
by Meyer Baudoin (programming methods) and then by Delobel Adiba (databases
and relational systems). Socrate was immediately put to use in Grenoble in the
IT sector and professionally via the Eca-Automation company, then in the army,
gendarmerie, EDF and SNCF. This was followed by a new version, Clio, developed
by Syseca, and many others such as CLIO/SQL, ORCHIS-Base, open to new
query languages.
Tony Hoare, who had attended an Abrial course in the Alps, brought him to
the Oxford Programming Research Group in 1979 for two years. It was here that
he and others developed the well-known version of Z. The implementation of Z
at IBM led to the restructuring and rewriting of parts of their CICS (Customer
Information Control System) software. This earned 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 named
Ada, in memory of Ada Lovelace, the daughter of Lord Byron, known as “the first
programmer in history”.
In his 2015 lecture at the Coll`ege de France – which is still available online on
the Coll`ege de France website – Jean-Raymond recounts how he worked and what
would become the B-Method. In a 1984 article for the Royal Society, “Programming
as a Mathematical Exercise”, he presents his method: “One consequence of
2
this viewpoint is that the activity of program construction becomes that of proof
construction.” He would remain an “independent consultant” for most of his career.
He was also a professor at the CNAM (Conservatoire National des Arts et
M´etiers) in Paris. He shared his ongoing work with many lecturers and individuals
preparing for an engineering degree at CNAM.
Abrial had also developed a tool to assist in development – the B-Tool – an
aid for interactive theorem proving. I remember that he addressed the case of
the 1986 proportional elections, using the approach presented in his article titled
“To Specify, or How to Master the Abstract”, which included a long quotation
from Proust – quite unusual in academic circles. It was a very pedagogical article.
The B-Method was in gestation: B because it came “before C” (the B-Toolkit
generated ADA and C code).
During the 1980s, the RATP (Paris’s public transport operator) called on Abrial
for line A of the RER, where the first safety-critical control-command software in
France was to be implemented. In his 2015 lecture at the Coll`ege de France, he
recalled:
“Claude Hennebert told me, ‘we would like to carry out a technical
audit.’ The audit lasted three weeks. I had to answer the question:
‘Do the means implemented guarantee that the final product matches
its original specification?’ I said I couldn’t answer because I hadn’t
seen a specification. I was told, ‘There was no specification, so give
us a course on specification.’ ”
In the mid-1980s, the RATP decided to embark on a driverless metro – Line
14 – whose critical components were developed using B. With Abrial’s support,
Alstom decided to develop its own toolset. In 1993, the first version of the BToolset
was created, comprising a type checker, a proof obligation generator, and
a theorem prover, suitable for industrial-scale software. Abrial then proposed
that the company Digilog – later Steria, and now Clearsy – industrialise these
tools. Today, Atelier B is freely available via the Clearsy website. Two companies
specialising in B were founded in Aix-en-Provence: Clearsy and Systerel.
In 1990, Abrial returned to Oxford, where BP (British Petroleum) developed
the B-Toolkit. In B, one works with abstract machines and proves that operations
preserve the invariant. For example, the invariant might specify that the generalised
intersection of the envelopes of underground trains is always empty. One
then needs to specify how these envelopes are computed, given that they evolve
due to factors such as speed and passenger load. The process involves moving
3
from a specification of abstract machines to machines that are closer to the software
implementation, through what is called refinement. In this stage, abstract
variables are linked to more concrete ones within the invariant. Refinement proof
is then required. At the end of the process, a program is generated that will remain
untouched. Proof is embedded in the construction of the program, rather
than being done after the program is written.
Also in 1990, Guy Laffitte used B and the B-Tool at INSEE (the French National
Institute of Statistics and Economic Studies) for the general population census.
In 1993, Alstom delivered to the metro systems of Calcutta and Cairo, as well
as to the SNCF and the RATP, the first train speed control systems incorporating
software developed using B. Today, many metro systems around the world use B
in their software. B was also used at the Gemplus research centre in G´emenos for
smart card development.
The B-Book, published in 1996 [1], was subtitled Assigning programs to meanings
– a nod to Robert Floyd’s 1967 paper Assigning meanings to programs [6],
which is one of the foundational sources of B. Also in 1996, at the first international
B conference in Nantes, Abrial gave a talk on extending B without altering
its foundations in order to develop distributed systems. This marked the beginning
of Event-B. In 2010, Modeling in Event-B: System and Software Engineering
[2] was published. In June 2025, the 18th conference on B has taken place in
D¨usseldorf as the combined ABZ 2025 conference, where the conference started
with a tribute to Jean-Raymond and an article written in 2019 with Abrial was
presented by his co-author, Dominique Cansell [4].
From 2004 to 2009, Abrial held a post at the Swiss Federal Institute of Technology
in Zurich (ETH Zurich), where he and a team developed the Rodin platform.
In 2006, he was inducted as a member of the Academia Europaea, and in
2008, awarded an honorary doctorate by the University of Sherbrooke. In 2017,
in the presence of Chinese President Xi Jinping, he received the International Scientific
and Technological Cooperation Award.
At the beginning of his Coll`ege de France lecture, Jean-Raymond stated:
“There are two types of researchers: the prolific and the monomaniacs.
I belong to the latter, as I have always pursued the same kind of
investigations – namely, the specification and verified construction of
computerised systems.”
Jean-Raymond was a researcher and a practitioner whose approach, pedagogy,
and publications inspired many academics and practitioners around the world. Z,
4
then B, became the lingua franca of many educators. Jean-Raymond Abrial was
also a mountaineer and a hiker, whether trekking from Marseille to Cassis via the
Calanques or across the Sahara.
Watercolour of Jean-Raymond Abrial, by Henri Habias (2025).
References
[1] Abrial, J.-R. (1996). The B-Book: Assigning Meanings to Programs. Cambridge
University Press. doi:10.1017/CBO9780511624162
[2] Abrial, J.-R. (2010). Modeling in Event-B: System and Software Engineering.
Cambridge University Press. doi:10.1017/CBO9781139195881
[3] Bowen, J.P. (1997). B-hold the Future of Software Development. The Times
Higher Education Supplement, 1267(30), 14 February. Multimedia computer
books.
[4] Cansell, D. and Jean-Raymond Abrial, J.-R. (2025). The Proved Construction
of a Protocol with an Example. ABZ 2025 – 11th International Conference on
5
Rigorous State Based Methods, D¨usseldorf, Germany, 11–13 June. https:
//abz-conf.org/site/2025/program/
[5] Denvir, T., He, J, Jones, C. B., Roscoe, A.W., Stoy, J., Sufrin, B., and Bowen,
J. P. (2024). Tony Hoare @ 90. FACS FACTS, 2024(2):5–42, July. BCS.
https://www.bcs.org/media/1wrosrpv/facs-jul24.pdf
[6] Floyd, R. W. (1967). Assigning meanings to programs. Republished in Colburn,
T. R., Fetzer, J. H., Rankin, T. L. (eds.) (1993), Program Verification.
Studies in Cognitive Systems, vol. 14. Springer. doi:10.1007/978-94-011-
1793-7 4
[7] Wikipedia (2025). The B-Book. Wikipedia: The Free Encyclopedia. https:
//en.wikipedia.org/wiki/The_B-Book
6