## REVIEW OF J.-R. ABRIAL: SPECIFICATION OR HOW TO GIVE REALITY TO ABSTRACTION (1986)

Computing Reviews 26(6): 335, 1985. The article under review
appeared in Tech. Sci. Inf. 3(3): 183-197, 1984.

This is a piece of propaganda for the notation for specification
of input-output characteristics of programs, as introduced and
advertised in books and articles by Jones and Bjørner. The
author delivers his message in terms of an example, namely a simple
set of operations for a certain type of storage allocation. This
example is worked out in great detail, by several stages of
implementation, and in terms of formulas and proofs.

The presentation is one among several others in recent years that
argue for the use of so-called formal specifications, a matter
sufficiently fashionable to appear on the programs of international
conferences. The question repeatedly asked by the adherents of this
fashion is: why do formal specifications not catch on and why are
they not used widely in practice?

Part of the answer is given indirectly by this article. The
author talks about 'the gap ... between those who believe it
is necessary to specify a program before writing it and those who
believe specification has no value'. This is a
misrepresentation of the situation. The point is that what is called
specification by the author is characterized not by its contribution
to the design and construction of the program, but by the use of a
particular logical-mathematical notation. A specification, in the
author's manner of speaking, is a description of parts of the logic
of the program and certain proofs of their consistency expressed in
such special terms. The so-called gap arises primarily from the
author's peculiar notion of specification.

There is probably a need for more careful argumentation in much
software development. Most likely, the notation advocated by this
author will sometimes be helpful in this. But presenting it
dogmatically, as the essential issue in this context, makes for a
distorted view of the problems.