History : Z in U.K. with A. Hoare

" 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]. 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 anongoing 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. [...]

source :
J.P. Bowen
Oral History of Sir Antony Hoare
CHM Ref: X3698.2007 © 2006 Computer History Museum Page 18 of 25