" From Z to B and then Event-B : Assigning Proofs to Meaningful Programs " (2013), text in English of part of the 2015 JRA conference at the Collège de France
2013 From Z to B and then Event-B : Assigning Proofs to Mea-
ningful Programs, J.-R. Abrial. E.B.Johnsen, L. Petre (eds) Integrated Formal Me-
thods. IFM 2013. Lecture Notes in Computer Science, vol 7940, pp. 1-15
https://doi.org/10.1007/978-3-642-38613-8_1
Cet article est très proche de l'exposé que fera en français Jean-Raymond Abrial au Collège de France le 1e avril 2015
From Z to B and then Event-B:
Assigning Proofs to Meaningful Programs
Jean-Raymond Abrial
Marseille, France
jrabrial@neuf.fr
The very first paper on Z [1] was published in 1980 (at the time, the name Z was
not “invented”), then the book on the B method [2] was published in 1996, and,
finally, the book on Event-B [3] was published in 2010. So, 30 years separate
Z from Event-B. It is thus clear that I spent a significant time of my scientific
professional life working with the same kind of subject in mind, roughly speaking
specification languages. I do not know whether this kind of addiction is good or
bad, but what I know is that I enjoyed it a lot.
So, I was very pleased when the organizers of iFM 2013, Luigia Petre and
Einar Broch Johnsen, invited me to give a talk at the conference and at the
same time suggested that I can give a presentation on “Z to Event-B”.
Since I am the main contributor (at least initially) of these three topics (Z,
B, and Event-B), there are certainly some common features that are interesting
to put forward in the three of them. But at the same time, during these thirty
years, it was also possible to gradually envisage some evolution from the first to
the last.
The main purpose of this presentation is thus to clarify this. This paper does
not contain a description of Z, B, or Event-B, as well as that of the corresponding
tools that have been developed over the years. Readers interested by this can
access the literature.
In the main part of the paper, I will rather present a historical account. The
idea is to explain how all this has slowly emerged as an intellectual evolution.
I will also try to make clear what are the external ideas and events (there are
many) that influenced this evolution. Then I will try to make a synthesis and
present what is common in these three topics and also what makes them different
from each other. This will take place in two Appendices.
The Way It All Started: Green
In the seventies, I was a member to the “Green” team developing the programming
language that later became ADA. During that time, I was probably one
of the first persons to write programs in “Green”: this is because I thought it
was necessary to try some proposed programming features in some significant
programs before incorporating them into a language. I must say that I was a bit
frustrated at the time, and this was for two reasons.
My first frustration came from my colleagues of the “Green” team: they did not
understand why I was so busy with this “programming” activity of mine. [...]
Comments
Post a Comment