2. Program Checking

A$\lambda$goVista can be seen as a novel application of program checking, an idea popularized by Manuel Blum and his students. The idea behind program checking is simply this. Suppose we are concerned about the correctness of a procedure P in a program we're writing. We intend for P to compute a function f, but we're not convinced it does so. We have three choices:

1.

We can attempt to prove that $P\equiv f$ over the entire domain of P. Unfortunately, in spite of decades of research into program verification, it is still only feasible to prove the correctness of trivial programs.

2.

We can test that P(x) = f(x), where x is drawn from a reasonable domain of test data. The problem with testing is that the actual distribution of input data to the program is often either unknown or prohibitively large.

3.

We can include a result checker C^P_f with the program. For every actual input x given to P, the result checker checks that P(x)=f(x).

We normally require C^P_f and P to be independent of each other; i.e. they should be programmed using very different algorithms. We also want the checker to be efficient. To ensure that these conditions are met, it is generally expected that a result checker C^P_f should be asymptotically faster than the program P that it checks. That is, we expect that if P runs in time T then C^P_f should run in time o(T).

Much theoretical research has gone into the search for efficient result checkers for many classes of problems. In some cases, efficient result checkers are easy to construct. For example, let P(x) return a factor of the composite integer x. This is generally thought to be a computationally difficult problem. However, checking the correctness of a result returned by P is trivial; it only requires one division. On the other hand, let P(x) return a least-cost traveling salesman tour of the weighted graph x. Checking that a given tour is actually a minimum-cost tour seems to be as expensive as finding the tour itself.