This proposal seeks to develop mathematical methods of computer science for the purpose of testing program correctness. The simpler but nevertheless nontrivial problem of deciding whether or not a given program on a given input outputs the correct answer will be investigated. Consider a program P that, while having been written to solve general instances of a certain problem, is actually run on just one or a few select instances. In this case, instead of proving the correctness of program P on all inputs, it suffices to prove that the output of P on the given few instances is correct (or to exhibit a bug in P). For example, suppose program P is supposed to decide if two graphs G and H are isomorphic. If P supplies the isomorphism, then it is easy to check that the isomorphism really works. Interestingly, the interactive proof for graph nonisomorphism serves to test the correctness of a program that asserts that G and H are not isomorphic. Given any program for graph isomorphism, this test procedure either gives quantifiable mathematical evidence that the program's answer is correct, or else it proves that the program has a bug. This raises the question: which computational problems (such as graph isomorphism) have the property that a program for the problem on any given input can be efficiently tested for correctness? Initial studies show that a large collection of programming problems drawn from block designs, graphs, codes, matrices over GF(q), latin squares, etc., can be tested by similar techniques. A useful natural (group theoretic) description of a broad class of computational problems, including those mentioned above, whose programs can be tested by such schemes is sought.
