Determining correctness by testing
Martin Fraser Brooks · 1980
This report presents a mathematical theory of program testing which describes how testing can be used to show a program's correctness. We study the situation where the programmer has written a program P which is either correct or which differs from the correct program by one or more errors in a specified class E of errors. The theory relates: (1) The combinatorics of how errors in E could have led to P being written. (2) The type of program behavior that the programmer will observe when testing; for example the program's output or a trace. (3) The characteristics of test data which is guaranteed to reveal the presence of errors in P. The theory is developed at a general level and is then specialized to the case of recursive programs having only certain types of simple errors, where the programmer observes a trace of each test run. We derive a method for generating test data for recursive programs. The generated test data is complete, meaning that if the only errors in the recursive program are of the specified simple types, then the test data will reveal the errors through at least one incorrect trace. Viewed contrapositively, if one assumes that the program differs from the correct program at most by errors of the specified simple types, then if the trace of each test run is as the programmer intended, then the program must be correct. The test data generation method has been implemented and examples of its operation are given.