Theoretical and empirical studies on using program mutation to test the functional correctness of programs

Abstract

In testing for program correctness, the standard approaches [11,13,21,22,23,24,34] have centered on finding data D, a finite subset of all possible inputs to program P, such that 1) if for all x in D, P(x) = f(x), then P∗ = f where f is a partial recursive function that specifies the intended behavior of the program and P∗ is the function actually computed by program P. A major stumbling block in such formalizations has been that the conclusion of (1) is so strong that, except for trivial classes of programs, (1) is bound to be formally undecidable [23].