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.