Predicate calculus and program semantics

Logic in computer science (03B70) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

This is a self-contained and very non-traditional book on foundations of computing science. The book deals with predicate transformers - functions from boolean structures (called ``predicates, or ``conditions, or ``assertions) to boolean structures introduced by E. W. Dijkstra - as a means for defining programming language semantics ``in a way that would directly support the systematic development of programs from their formal specifications. The theory is an exercise in formal mathematics, and the author stresses that the resulting tool ``became an absolute delight to work with: formal (calculational) proofs are not long, tedious, and error-prone, but rather short, simple, and elegant. The author has been able to develop heuristic for the design of these proofs turning it ``into an eminently teachable discipline. This approach has more profound consequences than ``just teaching programming language semantics: doing and teaching mathematics by means of the formalisms used in the book leads to much better (and shorter) mathematical texts, with arguments presented in a clear, precise, and explicit manner. The author does not - for several reasons - consider his book as a textbook, although the material has been successfully used in graduate courses on both sides of the Atlantik. The intended audience is ``to whom it may concern; mathematical and programming maturity is a much more relevant prerequisite than knowledge of some particular material. The author is very careful throughout his presentation, and, in particular, warns against allegedly improving it by means of complications exemplified by ``hybrid arguments, partly conducted in terms of a formal system, and partly conducted in terms of a specific model for that formal system. As the proof are calculational the first several chapters introduce notation and justify it as a very precise and explicit - and therefore convenient - manipulative tool. In most cases, the author's notation is close to the familiar one, and the differences are clearly explained, beginning with consistent and systematic use of boolean expressions. The grammar for parsing the formulae is very simple. Throughout the book, the author took substantial efforts to show the development (and patterns) of non-trivial proofs and to present proofs in a manner perfectly fit for human consumption rather than pull mathematical rabbits out of a hat. The reader often sees how formal manipulation suggests the only possible next step in proof development, since clairvoyance is considered unwelcome. This treatment agrees with E. W. Dijkstra's observations on mathematics education: a new and better proof of a well-known theorem often has a greater value than a new theorem. After the chapters on notation, the calculus of boolean structures is developed in an algebraic fashion. This largest chapter (51 pages) introduces well-known (and occasionally less well-known) material in an unconventional manner, and as a result the reader familiarizes himself with the author's approach. They often investigate, possibly transitively, what can be derived from postulates with explicit rules of manipulation (``truth tables are never used). The underlying decision (evidently, in-the-small, and after some reflection, in-the-large) are clearly justified. The author notes that this chapter is very detailed due to at least three reasons that make it unconventional: rules of manipulation are made explicit, expressions with equivalence - having clean manipulation rules - can often not be adequately worded in a natural language, and no (set-theoretic) models are used. The next chapter is the second largest one (40 pages) and deals, again calculationally, with predicate transformers. Programming language semantics is defined in the following chapters using these constructs. In particular, it is shown that language design decisions may have deep underlying mathematical reasons. The author moves to grounds more familiar to the programmer at the end of the predicate transfer chapter where he introduces predicates on state spaces, i.e., more specific ones than the general theory requires. The ``programming chapters, starting with semantics of straight-line programs, are very consistent in their calculational approach and heavily rely on the ``mathematical ones; at times the author explicitly extracts ``mathematical contents from their programming considerations. The author admits that certain theorem formulations and at times even definitions may be appreciated only with some foresight (``in view of what follows, p. 175, or ``in view of later applications, p. 165). This is especially true for Chapter 8 ``Equations in predicates and their extreme solutions - a basis for semantics of repetitions. In the same manner, the author suggests to accept very important definitions of predicate transformers for repetition ``without wondering from where they come or what has inspired them: this information is provided in the next chapter frankly titled ``Operational considerations. A possible explanation of this not entirely satisfactory approach may lie in the intrinsic difficulty of repetition: its termination cannot be explained using only predicate calculus, and the author introduces here the notion of well-founded sets (for which they proof the validity of mathematical induction and finiteness of all decreasing chains). the same somewhat foresight-based approach is encountered in (very short) Chapters 11 and 12 on converse predicate transformers as the mathematical basis of strongest postconditions. Therefore it may be advisable to read (and re- read) the book in a manner that is not always linear. The heuristics for proof development is often made explicit, but the reader should note the author's warning: ``Our texts have a tendency of being misleadingly smooth and unusually compact. The explanations and remarks clearly show the author's mastery of English - to rephrase E. W. Dijkstra, one of the prerequisites for success in programming (the other one being mathematical maturity). The author's excellent narratives on programming language semantics and on comparative merits of different notations clearly show that programming cannot be reduced to calculations - the subject matter of the book - despite the necessity and significance of the latter.

Recommendations

Cited in

(only showing first 100 items - show all)

This page was built for publication: Predicate calculus and program semantics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4692630)