Now we are interested in whether the program gives the correct results for various sets of test data. If, for some set of data the program halts normally, but gives incorrect results, then the program is said to have a logical error. Even if the program does work properly for all sets of test data, this does not mean that all logical errors have been eliminated. It is normally impossible to test all possible data sets, and although by choosing good test data we can make the probability of error small, we can't be sure that the program is correct. (There are numerous examples of commercial software that have subtle, and sometimes serious, errors that are found by users.) In general, program verification requires the use of formal proof techniques like those we have studied.
A proof that a program is correct consists of two parts. The first part shows that the correct answer is obtained if the program terminates. This part establishes partial correctness of the program. The second part of the proof shows that the program always terminates.