Design and implement a solution to the Naur text-processing problem using the language specified by your instructor. Execute it against test data and record the number of faults you find and the cause of each fault (e.g., logic fault, loop counter fault). Do not correct any of the faults you detect. So you goal is to just detect the faults, not to correct them.
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 refined stepwise, so is the invariant. Developing a product in this way gives the programmer confidence that the product is correct and tends to reduce the number of faults. Quoting Dijkstra again, "The only effective way to raise the confidence level of a program significantly 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 filled 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 correctness. The procedure consisted of approximately 25 lines of code. The paper then was reviewed by Leavenworth in Computing Reviews [Leavenworth, 1970]. The reviewer pointed out that, in the output of Naur's procedure, the first word of the first line is preceded by a blank unless the first word is exactly maxpos characters long.
Although this may seem a trivial fault, it is a fault that surely would have been detected 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 Good enough 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 difficulty. In fact, of the total of seven faults collectively detected by Leavenworth, London, and Good enough 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.