Tentative steps toward a development method for interfering programs

Reviewer: Randal P. Leavitt

C. B. Jones has produced a very interesting report. It summarizes the work done during his two year stay at Oxford, and illustrates the extension of his rigorous software development method to include the programming of concurrent processes. These programs are referred to as interfering because the concurrent tasks can interfere with each other's operation either by means of shared variables or with message passing. For this type of complicated software, the proposed development method, based on formal rules, will reduce design errors and, consequently, incrase productivity. Readers of Jones's other work will find this theme familiar. Rigorous software development, according to Jones, must be supported by formal theory without getting bogged down in excessive detail. It encompasses top-down analysis with active decomposition, ensuring at each stage of refinement that the design satisfies the specifications. Other approaches for verifying concurrent programs are characterized by proofs for isolated components, followed by a final proof that all these component proofs do not conflict. Consequently, the design cannot be validated until the decomposition is complete. For Jones, considering a formally supported development strategy for very large programs, these approches are not acceptable. He has, instead, proposed an extension of his rigorous method for isolated program development, and illustrated how it can be applied to develop interfering programs. The basic idea is to include precise interference statements in the program specification. These include “rely-conditions” defining the assumptions used during development, and “guarantee-conditions” restricting the interferences an implementation can generate. To illustrate the technique, Jones includes a step-by-step refinement for two Ada programs—one to find the minimum index of an array element having a specified property, and the other to record equivalence relationships. These are first developed as isolated programs without concurrency, and then redeveloped to show an equivalent concurrent implementation. The non-interfering versions are shown to be a special case of the more general interfering development method. There are, however, some deficiencies in Jones's report. Anyone unfamiliar with his earlier work will find the notation particularly difficult to follow. It is very clearly defined in Software development: a rigorous approach [1]. The book and the article together constitute some very rewarding reading. Jones's development method does not deal with some important problems, such as deadlock, Ada exceptions, total correctness, and some aspects of how global variables are shared by tasks. The Ada examples are not syntactically correct, though they are understandable. Proper syntax does make examples easier to read, however. Jones does not claim to have defined a complete proof system. The given proof rules are not stable and further examples need to be worked out. This report essentially demonstrates that some useful results can be derived by extending Jones's rigorous methods, but many avenues still remain to be explored. Jones makes several almost indirect observations in this report that deserve notice. One is that program specifications will have to include some comment about performance if they are to be properly understood as requiring concurrency. (Non-concurrent implementations can always satisfy the requirements if performance is not a factor.) Another is that very strong pressure exists to adopt language features that make the degree of interference controllable. The Ada rendezvous concept is particularly useful in this way.