6.5.2 6.5.2 Mini ase Study
Correctness Proof Mini Case Study
An important aspect of correctness proofs is that they should be done in conjunction with design and coding. As Dijkstra put it, “The programmer should let the program proof and program grow hand in hand” [Dijkstra, 1972]. For example, when a loop is incorporated into the design, a loop invariant is put forward; and as the design is refi ned stepwise, so is the invariant. Developing a product in this way gives the pro-grammer confi dence that the product is correct and tends to reduce the number of faults. Quoting Dijkstra again, “The only effective way to raise the confi dence level of a program signifi cantly is to give a convincing proof of its correctness” [Dijkstra, 1972]. But even if a product is proven to be correct, it must be thoroughly tested as well. To illustrate the necessity for testing in conjunction with correctness proving, consider the following.
In 1969, Naur reported on a technique for constructing and proving a product correct [Naur, 1969]. The technique was illustrated by what Naur termed a line-editing problem ; today this would be considered a text-processing problem. It may be stated as follows:
Given a text consisting of words separated by blank characters or by newline (new line) characters, convert it to line-by-line form in accordance with the following rules:
1. Line breaks must be made only where the given text contains a blank or newline;
2. Each line is fi lled as far as possible, as long as 3. No line will contain more than maxpos characters.
Naur constructed a procedure using his technique and informally proved its cor-rectness. The procedure consisted of approximately 25 lines of code. The paper then was reviewed by Leavenworth in Computing Reviews [Leavenworth, 1970]. The re-viewer pointed out that, in the output of Naur’s procedure, the fi rst word of the fi rst line is preceded by a blank unless the fi rst word is exactly maxpos characters long.
Although this may seem a trivial fault, it is a fault that surely would have been de-tected had the procedure been tested, that is, executed with test data rather than only proven correct. But worse was to come. London [1971] detected three additional faults in Naur’s procedure. One is that the procedure does not terminate unless a word longer than maxpos characters is encountered. Again, this fault is likely to have been detected if the procedure had been tested. London then presented a corrected version of the procedure and proved formally that the resulting procedure was correct; recall that Naur had used only informal proof techniques.
The next episode in this saga is that Goodenough and Gerhart [1975] found three faults that London had not detected, despite his formal “proof.” These included the fact that the last word is not output unless it is followed by a blank or newline. Yet again, a reasonable choice of test data would have detected this fault without much diffi culty. In fact, of the total of seven faults collectively detected by Leavenworth, London, and Goodenough and Gerhart, four could have been detected simply by running the procedure on test data, such as the illustrations given in Naur’s original paper. The lesson from this saga is clear. Even if a product has been proven correct, it still must be tested thoroughly.
172 Part A Software Engineering Concepts
The example in Section 6.5.1 showed that proving the correctness of even a small code fragment can be a lengthy process. Furthermore, the mini case study of this section showed that it is a diffi cult, error-prone process, even for a 25-line procedure. The following issue therefore must be put forward: Is correctness proving just an interesting research idea or is it a powerful software engineering technique whose time has come? This is answered in Section 6.5.3.
6.5.3 Correctness Proofs and Software Engineering
A number of software engineering practitioners have put forward reasons why correctness proving should not be viewed as a standard software engineering technique. First, it is claimed that software engineers lack adequate mathematical training. Second, it is sug-gested that proving is too expensive to be practical; and third, proving is too hard. Each of these reasons will be shown to be an oversimplifi cation:
1. Although the proof given in Section 6.5.1 can be understood with hardly more than high school algebra, nontrivial proofs require that input specifi cations, output specifi ca-tions, and loop invariants be expressed in fi rst- or second-order predicate calculus or its equivalent. Not only does this make the proof process simpler for a mathematician, it allows correctness proving to be done by a computer. To complicate matters further, predicate calculus now is somewhat outdated. To prove the correctness of concurrent products, techniques using temporal or other modal logics are required [Manna and Pnueli, 1992]. There is no doubt that correctness proving requires training in mathemati-cal logic. Fortunately, most computer science majors today either take courses in the requisite material or have the background to learn correctness-proving techniques on the job. Therefore, colleges now are turning out computer science graduates with suf-fi cient mathematical skills for correctness proving. The claim that practicing software engineers lack the necessary mathematical training may have been true in the past, but it no longer applies in the light of the thousands of computer science majors joining the industry each year.
2. The claim that proving is too expensive for use in software development also is false.
On the contrary, the economic viability of correctness proving can be determined on a project-by-project basis using cost–benefi t analysis (Section 5.2). For example, con-sider the software for the international space station. Human lives are at stake, and if something goes wrong, a space shuttle rescue mission may not arrive in time. The cost of proving life-critical space station software correct is large. But the potential cost of a software fault that might be overlooked if correctness proving is not performed is even larger.
3. Despite the claim that correctness proving is too hard, many nontrivial products have successfully been proven correct, including operating system kernels, compilers, and communications systems [Landwehr, 1983], [Berry and Wing, 1985]. Furthermore, many tools such as theorem provers assist in correctness proving. A theorem prover takes as input a product, its input and output specifi cations, and loop invariants. The theorem prover then attempts to prove mathematically that the product, when given input data satisfying the input specifi cations, produces output data satisfying the output specifi cations.
sch76183_ch06_154-182.indd 172
sch76183_ch06_154-182.indd 172 04/06/10 1:28 PM04/06/10 1:28 PM
At the same time, there are some diffi culties with correctness proving:
• For example, how can we be sure that a theorem prover is correct? If the theorem prover prints out This product is correct, can we believe it? To take an extreme case, consider the so-called theorem prover shown in Figure 6.7 . No matter what code is submitted to this theorem prover, it will print out This product is correct. In other words, what reliability can be placed on the output of a theorem prover? One suggestion is to submit a theorem prover to itself and see whether it is correct. Apart from the philosophical implications, a simple way of seeing that this will not work is to consider what would happen if the theorem prover of Figure 6.7 were submitted to itself for proving. As always, it would print out This product is correct, thereby “proving” its own correctness.
• A further diffi culty is fi nding the input and output specifi cations, and especially the loop invariants or their equivalents in other logics such as modal logic. Suppose a product is correct. Unless a suitable invariant for each loop can be found, there is no way of prov-ing the product correct. Yes, tools do exist to assist in this task. But even with state-of-the-art tools, a software engineer simply may not be able to come up with a correctness proof. One solution to this problem is to develop the product and proof in parallel, as ad-vocated in Section 6.5.2. When a loop is designed, an invariant for that loop is specifi ed at the same time. With this approach, it is somewhat easier to prove that a code artifact is correct.
• Worse than not being able to fi nd loop invariants, what if the specifi cations themselves are incorrect? An example of this is method trickSort ( Figure 6.2 ). A good theorem prover, when given the incorrect specifi cations of Figure 6.1 , undoubtedly will declare that the method shown in Figure 6.2 is correct.
Manna and Waldinger [1978] stated that, “We can never be sure that the specifi ca-tions are correct” and “We can never be certain that a verifi cation system is correct.”
These statements from two leading experts in the fi eld encapsulate the various points made previously.
Does all this mean that there is no place for correctness proofs in software engineering?
Quite the contrary. Proving products correct is an important, and sometimes vital, software engineering tool. Proofs are appropriate where human lives are at stake or where other-wise indicated by cost–benefi t analysis. If the cost of proving software correct is less than the probable cost if the product fails, then the product should be proven. However, as the text-processing mini case study shows, proving alone is not enough. Instead, correctness proving should be viewed as an important component of the set of techniques that must be utilized together to check that a product is correct. Because the aim of software engineering is the production of quality software, correctness proving is indeed an important software engineering technique.
Even when a full formal proof is not justifi ed, the quality of software can be mark-edly improved through the use of informal proofs. For example, a proof similar to that FIGURE 6.7
“Theorem prover.”
void theoremProver ( ) {
print “This product is correct”;
}
of Section 6.5.1 assists in checking that a loop is executed the correct number of times.
A second way of improving software quality is to insert assertions such as those of Figure 6.6 into the code. Then, if at execution time an assertion does not hold, the product is halted and the software team can investigate whether the assertion that terminated execution is incorrect or whether indeed a fault in the code was detected by triggering the assertion.
Languages such as Java (from version 1.4 onward) support assertions directly by means of an assert statement. Suppose that an informal proof requires that the value of variable xxx be positive at a particular point in the code. Even though the members of the design team may be convinced that there is no way for xxx to be negative, for additional reliability they may specify that the statement
assert (xxx > 0)
must appear at that point in the code. If xxx is less than or equal to 0, execution terminates, and the situation can be investigated by the software team. Unfortunately, Assert in C++ is a debugging statement, similar to assert in C; it is not part of the language itself.
Once the users are confi dent that the product works correctly, they have the option of switching off assertion checking. This speeds up execution, but any fault that would have been detected by an assertion may not be found if assertion checking is switched off. There-fore, there is a trade-off between run-time effi ciency and continuing assertion checking even after the product has been installed on the client’s computer. (Just in Case You Wanted to Know Box 6.3 gives an interesting insight on this issue.)
Model checking is a new technology that may eventually take the place of correctness proving of software. Model checking is outlined in Section 18.11.
A fundamental issue in execution-based testing is which members of the software devel-opment team should be responsible for carrying it out. This is discussed in Section 6.6.