The quest to prove the “correctness” of software before it is released to users is one of the prime activities of software engineering; there is a long history of research and development in this area. However, the quest has not been successful so far, except possibly in some isolated cases. One approach used in this quest, where the source code of the program is available, is for the programmer, analyst, or tester wishing to check the correctness of a program to add what are known as assertions or conditions at appropriate points in the program, which will be tested when the execution reaches those points. This requires the tester to understand the meanings of the variables in the program, and other components of the “program state,” and be able to formulate conditions in a way that can cause their execution when the control flow reaches that point. This may be termed an “empirical” approach. It is typically impossible to completely test any reasonably sized program using this approach. However, it is intended that most critical conditions be defined and tested this way. There are approaches to developing testing tools that create very large collections of data to test programs this way as exhaustively as possible.
The other primary approach to proving the correctness of programs has been to formalize the semantics of programming languages and data structures, in a way that makes them amenable to formal analysis by the compiler, and by programmers. The collection of methods used in this approach is often called the formal methods approach. This approach has not been very successful so far, due to hard problems in the above characterization and analysis tasks. For a recent compilation of papers in this area, see Dershowitz [1].
Given the inherent difficulties of being successful in the latter approach, much work is being done to use the empirical approach as effectively as possible. Ploesch correctly identifies program correctness as an important part of software quality, and, accordingly, evaluates the techniques he uses in proving correctness in terms of their contribution to software quality.
This book consists of ten chapters and two appendices. In the first chapter, the author surveys ways in which software quality has been defined and approached in the literature. He concentrates on the software assurance technology center (SATC) model, which can be viewed as a part of the factor-criteria-metrics (FCM) approach. This approach divides software quality into four parts: requirements quality, product code quality, implementation effectiveness, and testing effectiveness. Each of these is then broken down into a number of criteria, and then broken down into a set of metrics, which may be evaluated by studying and testing the code. Ploesch emphasizes in the preface that simplicity, generality, and expressiveness are some of his requirements, so that “average software engineers” can use the techniques he develops. Yet, these terms do not appear directly in his list of criteria. Perhaps they should. Another point I would like to make, with regard to the author’s evaluation of the contributions of his techniques to his list of criteria, is that, while he identifies where positive effects are possible, he does not indicate possible negative effects in other criteria. If, for instance, simplicity were one of his criteria, some of the techniques proposed would probably have to be indicated as having a negative effect on that criterion.
The body of the book addresses the formulation of contracts, consisting of pre-conditions, post-conditions, and the so-called invariants in the block of code being analyzed; scenarios, which are use cases describing entity behavior; and prototyping software using these.
A contract is viewed as an agreement between a piece of code and the user of the code. The user, which is often another piece of code calling or preceding the first piece code, promises that the pre-conditions and the invariants will be satisfied when the code in question is entered. The responsibility of the code is that, if the above are satisfied, then the post-conditions and the invariants will also be satisfied when the code is exited. This type of contract is said to be at the behavioral level, as distinct from other types of contracts at the quality of service (QoS), synchronization, and syntactic levels.
Ploesch cites previous work by Parnas, Hoare, and Dijkstra. In discussing the work by Parnas, however, he should clarify Parnas’ notation, without requiring the reader to go back to the original paper; otherwise, it is very possible for the “average software engineer” to misunderstand the code fragment that is presented. The formulation used by the author in his work follows the Hoare triple, namely, “{P} Q {R},” which means: “If the assertion {P} is true before initialization of a program Q, then the assertion R will be true on its completion.” This is the general structure of a contract as used in this book.
The author uses two sub-languages to formulate contracts: simple contract language (SCL), to express contracts in Java, and object constraint language (OCL), to express contracts that would be associated with unified modeling language (UML) diagrams. This is already an indication of complications to come, in the area of expressing contracts when using different languages and platforms.
A point worth making here is that, although pre- and post-conditions are usually presented as a pair of brackets (a matching pair), a single pre-condition may be matched with one or more post-conditions, as in a block of code having multiple exit points. Indeed, when a pre-condition has been specified, there may be any number of intermediate and post-conditions placed in the body of the code to check for various errors.
The author then makes a nice classification of the contract support available in various languages. This is a useful overview, prompting those interested to further study this feature in various languages.
Ploesch goes on to describe his formulation of scenarios, which serve the same function as use cases in UML. Time-line notations (as in UML) and two-dimensional object models, similar to class diagrams, are discussed. The need for additional text descriptions, to express information that cannot be expressed in the diagrams, is pointed out. This is the role of OCL: to be able to add text to UML diagrams, to capture information that cannot be captured otherwise. Since OCL has a formal syntax and semantics, it can be used to provide further information about scenarios. While there is no evaluation of whether or not this is sufficient, it seems to be a step in the right direction. Clearly, much work is needed in this area.
A chapter is devoted to prototyping with contracts and scenarios. This too appears to be a useful approach to formal development, especially in incremental development, since it will reduce the need for regression testing, thus improving quality, reducing cost, and speeding up delivery. However, further work is needed to evaluate whether, and to what extent, these benefits are being realized, and how this can be improved.
The main part of the book winds up with a discussion of contracts in the context of type systems, illustrating their use with axioms, assertions, and subtyping.
In the first appendix, there is an extensive description of a monitoring and control application, and the use of scenarios and contracts. The application is a fairly complicated one. The style of scenario description is tabular, with natural language descriptions in the tables. This does not make this example a very convincing one. Use of a more formal style might have been more satisfactory.
The final appendix is a Backus Naur Form (BNF) description of SCL syntax, the contract language used in some of the examples.
On the whole, the book presents a consistent and well-organized approach to the area of proving program “correctness” as much as possible, through information provided by the programmer, analyst, or tester. While it misses its goal of being simple enough for the “average practicing software engineer,” it does point to a direction in which progress is made and work should go on.
I recommend the book highly both to researchers and practitioners working in this area, especially those using UML.
