Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Formal development programs and proofs
Dijkstra E. (ed), Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990. Type: Book (9780201172379)
Date Reviewed: Sep 1 1990

“Good programming is the art and science of keeping things simple” (p. viii). The Year of Programming (1987) at the University of Texas at Austin, which originated from this conviction, resulted in a series of somewhat unusual proceedings. This volume deals with general aspects of programming as a discipline. It shows a methodology for writing correct programs and knowing that they are correct. The “streamlining of the mathematical argument” is the focus of all the contributions, whether they deal with formal mathematics, the derivation of particular algorithms, or the presentation of this derivation. The reader is encouraged to share the authors’ enthusiasm.

The prerequisite for understanding most of the 18 papers is mathematical maturity; familiarity with ideas expressed in the references below, although not strictly necessary, would be helpful. The papers vary in complexity, and for some papers familiarity with the basics of some aspects of formal mathematics (such as “constructive” logic and number theory) and of systolic computations is desirable. The book might challenge its reader because of the “drastic difference from what [the reader] was used to and familiar with” due to “the shortcomings of our various educational systems.” The material is well worth the effort.

R. C. Backhouse’s paper on constructive type theory is one of the most demanding in the book. Its goal is to show how program quality can be improved by using types at the development rather than the implementation stage (“static” and “dynamic” type checking belong to the implementation stage). The author succeeds in presenting the main features of Martin-Löf’s theory in a manner understandable to at least some readers; many examples provide additional help. A realistic nontrivial proof of the program (Boyer-Moore majority vote) is developed in the framework of this theory, although the ideas underlying this development can be presented within a more conventional framework, such as Dijkstra and Feijen’s [1,2].

Several short papers (by E. W. Dijkstra, D. Gries, J. L. A. van de Snepscheut, and M. Rem and T. Verhoeff) show the formal development of sequential and parallel algorithms using techniques that are now standard. Programs and their proofs are developed together using simple formal manipulation techniques combined with some invention. The methodology and techniques for parallel program design resemble those used for sequential programming, and complex design problems can indeed be mastered in this manner. Some of these parallel programs “lend themselves very well to silicon compilation.” The expositions are clear, concise, and elegant (Rem’s exposition of systolic algorithms may even be too concise). Van de Snepscheut’s presentation of a distributed implementation of Warshall’s transitive closure algorithm is the only paper that uses figures, and it uses them only for visualization. Some papers successfully simulate “hands-in-the-pocket” oral presentations. After studying several program derivations in this manner, the reader will become accustomed to the technique and may use it successfully in the future.

Other short papers deal with “streamlining of the mathematical argument.” As Dijkstra has noted in his book [3], the experience gained from developing programs in a precise, explicit, and elegant manner should improve general mathematical reasoning; in particular, design decisions are isolated and recorded explicitly. The authors show that programming paradigms make a mathematical argument extremely elegant. They also successfully advocate the use of classical logic as a daily calculational tool. Some authors convincingly demonstrate how formal (nearly uninterpreted) symbol manipulation can do the work both in program construction and in mathematics; if this looks unusual, recall that “computing science is intrinsically concerned with the boundary between human and mechanical symbol manipulation” (p. xi). This manipulation is done in small steps because of the “limited scope of our minds.” It is shown that conventional mathematical definitions, even for such simple notions as “maximum,” are often inconvenient for manipulations and should therefore be reconsidered. Still, design decisions should be justified heuristically rather than pulled out of a hat. The closest approximation to a “hands-in-the-pocket” presentation seems preferable for both computing and general mathematical argument, if appropriate. Some convincing examples of such presentations are provided in the book (and Feijen and Bijlsma conclude their paper about formula manipulation with the advice to postpone the use of pencil and paper as long as possible).

A. J. Martin presents the crucial steps in the solution of a real-world problem: design of delay-insensitive VLSI circuits based on formal program transformations. The design is proven to meet its specifications, rather than “checked” using exhaustive and expensive test systems. The paper shows how, by applying rules for manipulating uninterpreted formulae, a sequential description of a program is transformed into a semantically equivalent description with the same ordering of actions but without explicit sequencing. The application semantics, however, are presented too concisely, and the paper may be difficult for nonexperts.

Two contributions by J. M. Morris present mathematical laws underlying the stepwise transformation of a formal specification into a program. A program is defined as a specification without nonalgorithmic components. A programming language is an implementable subset of the specification language. The stepwise refinement rules are formal, unlike the “semiformal” rules in several other papers in the book. Design decisions for theorems and their occasionally lengthy proofs are frequently omitted. Some definitions are motivated, but Morris’s papers, again unlike the semiformal presentations, consciously do not study the “very effective heuristics” crucial for “the success of the game…of deriving elegant programs.” The author considers both the benefits of his approach and its serious limitations. It is interesting to compare Morris’s approach with Gries and Volpano’s recent “semiformal” paper [4].

The last paper, “Influences (or Lack Thereof) of Formalism in Teaching Programming in Software Engineering” by D. Gries, deals with more widespread use of the ideas presented in the book. Gries stresses that all the contributors to the book except himself are from Europe and notes the reason: “We are so busy doing the next thing that we don’t have time to reflect on the last thing.” A drastic change in approach is needed, and only proper computing education, with an emphasis on formal methods and syntactic proofs, may help. The goal is to use formalism judiciously because “the game is to formalize only as much as necessary--no more and no less--to make an argument as clear, simple, and elegant as possible. It is a game of economy of thought, concept, and pen.” This problem has recently been hotly debated in Communications of the ACM, and this debate shows the need to educate the programmer. The critical mass of appropriate texts is slowly accumulating and, in the trenches of commercial software, the demand for object-oriented design and development may mean that the need for formalism will soon be acknowledged.

Reviewer:  H. I. Kilov Review #: CR123375
1) Dijkstra, E. W. A discipline of programming. Prentice-Hall, Englewood Cliffs, NJ, 1976. See <CR> 17, 11 (Nov. 1976), Revs. 30,461 and 30,462.
2) Dijkstra, E. W. and Feijen, W. H. J. A method of programming. Addison-Wesley, Reading, MA, 1988.
3) Dijkstra, E. W. Selected writings on computing: a personal perspective. Springer-Verlag, New York, 1982. See <CR>, Rev. 8407-0518.
4) Gries, D. and Volpano, D. The transform--a new language construct. Struct. Program. 11, 1 (1990), 1–10.
Bookmark and Share
  Featured Reviewer  
 
Specification Techniques (F.3.1 ... )
 
 
Assertions (F.3.1 ... )
 
 
Computer Science Education (K.3.2 ... )
 
 
Invariants (F.3.1 ... )
 
 
Languages (D.2.1 ... )
 
 
Methodologies (D.2.1 ... )
 
  more  
Would you recommend this review?
yes
no
Other reviews under "Specification Techniques": Date
Compatibility problems in the development of algebraic module specifications
Ehrig H., Fey W., Hansen H., Löwe M., Jacobs D., Parisi-Presicce F. Theoretical Computer Science 77(1-2): 27-71, 1990. Type: Article
Oct 1 1991
Transformations of sequential specifications into concurrent specifications by synchronization guards
Janicki R., Müldner T. Theoretical Computer Science 77(1-2): 97-129, 1990. Type: Article
Jul 1 1991
Regularity of relations
Jaoua A., Mili A., Boudriga N., Durieux J. Theoretical Computer Science 79(2): 323-339, 1991. Type: Article
Apr 1 1992
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy