Tony Hoare nous parle de Jean-Raymond Abrial à Oxford/Tony Hoare tells us about Jean-Raymond Abrial at Oxford
Merci Jonathan Bowen
Bowen: This led up to your CSP book in your own red and white book series in 1985, but you were also
working
on other things. You were very much promoting a new formal notation
that became known as Z at Oxford, although maybe you weren’t directly
working on it. I understand you were involved in inviting
Jean-Raymond Abrial for instance, who very much promoted Z and defined
Z. Would you like to say something about how that started?
Hoare: Yes, it’d be a pleasure. I met Jean-Raymond Abrial at a summer school organized by Electricite
de France in a lovely little village in France called Labrae sonnalp [sp] (1). I
was very impressed by his research, and indeed his lecturing. He was a
brilliant lecturer. I invited him to spend some research time at Oxford,
and got a research grant for him from the Research Council. He did
marvelous work in the development of Z. This is a sort of
specialization of the techniques of logic and set theory, which were
originally thought of as the foundation of mathematics in the earlier
part of the last century, and now being suggested as a suitable notation
and conceptual framework for specifying the desired properties of
computer systems. The formal theory was adapted for this purpose and
tried out in a number of small and other realistic and large sized
examples, and found to be surprisingly effective at describing what a
program is intended to do, rather than how the program works, how the
program actually does it.
Bowen: I think you were involved with encouraging IBM to actually take up the ideas. How did that
come about?
Hoare:
Again, it was very much a matter of chance. I was invited to give a
keynote address at the British Computer Society Symposium on
professionalism, I think it was, in programming. I talked a bit about
formalization and verification, and put forward a conjecture, fairly
tentatively, that maybe the time was right to scale these things up by
trial use in industry. In the audience there happened to be quite a
senior director from IBM at Hursley. He came up to me after the lecture,
and invited me to put my commitment where my mouth was, and actually do
something in collaboration with IBM. That made me gulp a bit, because I
knew that -- well, I had the impression -- that IBM had produced some
pretty complicated software, and this really would be a challenge, and
there was a good chance that we would fall flat on our faces. But you
can’t turn down an opportunity like that. So Abrial and Ib Sorensen and
other colleagues set to work, and actually produced some very useful
analyses for them, using Z, to help them with an ongoing project for
restructuring and rewriting parts of their software system, a software
system called CICS, C-I-C-S. It stands for Customer Information Control
System. It was one of the most profitable and influential software
products in those days, so it was an important project.
Bowen: That led to a Queen’s award for technology. Another strand of your work led to another
Queen’s award, which was the work on Occam and the transputer, which came out of your CSP work.
How did that connect ? "
(1) Ce nom de village n'existe pas. Certainement un problème de prononciation du français.
Lisez l'interview de Jonathan Bowen,
CHM Ref: X3698.2007 © 2006 Computer History Museum Page 6 of 25, Jonathan Bowen
Merci Jonathan pour tout ce que tu fais encore aujourd'hui du U.K. jusqu'en Chine !
Comments
Post a Comment