J.-R. Abrial, Foreword of the book "SPECIFICATION CASE STUDIEs" edited by Ian Hayes

 Foreword of the book "SPECIFICATION CASE STUDIEs" edited by Ian Hayes

Reading formal texts is like meeting people. Sometimes, you understand them
straightaway like good friends who take to each other immediately. At other times,
it is more difficult. You may parse what you read, but find it impossible to work
out any meaning. With the latter, you have to be patient, ask questions, explore
the surroundings; in other words, it is better for you to be introduced through some
common good friends who volunteer to help you prepare for the first meeting.
Large computer programs, to say the least, pertain to the category of formal texts
whose meanings are not immediately obvious! For that reason, people have been
trying – for some time – to find out what kind of intermediate text would be best
suited to play the role of go-between.
This book reports on experiments made at Oxford University within this frame-
work: it shows how one may communicate ideas and meanings about existing (or
even not-yet-written) computer programs, and this by using conventional mathemat-
ical notations of ordinary logic and elementary set theory.
The choice of a “standard” mathematical notation offers many advantages: it is
easy for a scientifically trained reader to understand; it is rigorous; it denotes rich
concepts (e.g., functions and their usual attributes: partiality vs. totality, domain,
range, etc.); and it is an open notation, because you may enlarge it at will.
Liberated from the burden of obeying the idiosyncracies of a particular language,
the authors of the various papers forming this book were free to experiment with
various styles depending on the problem at hand (but also on their personal taste).
In reading the book, I found it very exciting to discover how each situation was
formalised in a way different from that of others (or from what I had in mind). This
variety of style is reassuring: it indicates, if at all necessary, that there does not exist
any “normal” way of describing things rigorously.
However, despite this variety, all authors seem to have encountered at some point
or another a difficulty of the same nature—namely that of structuring the formal
text. To this common problem they decided to give a common answer in the form of
what is called a Schema, together with a corresponding Schema Calculus.
Roughly speaking, a Schema is a box within which certain variables of interest are
together declared, given types, and mutually constrained. The Schema Calculus gives
rules by which these boxes can be transformed or combined to produce other boxes.
The main advantages of this mechanism are its simplicity and immediate “visibility”.
In this book, the main emphasis has been put on using ordinary mathematical
notations in order to describe (specify) computer programs. Another important out-
come of any mathematical approach is that of performing proofs: this will be vital, of
course, in the process of software design by which specifications are gradually trans-
formed in order to obtain concrete programs. Here is the subject of another book.

J.-R. Abrial
Paris, February 1986