Algorithmic Debugging with Assertions

Algorithmic debugging, as presented by Shapiro, is an interactive process where the debugging system acquires knowledge about the expected meaning of a program being debugged and uses it to localize errors. This paper suggests a generalization of the language used to communicate with the debugger. In addition to the usual "yes" and "no" answers, formal specifications of some properties of the intended model are allowed. The specifications are logic programs. They employ library procedures and are developed interactively in the debugging process. An experimental debugging system incorporating this idea has been implemented. In contrast to some other systems, its diagnosis algorithms do not require instantiation of unsolved goals by the oracle. This is achieved by generalization of the oracle in the incorrectness algorithm, and by adopting a new approach in the insufficiency algorithm. A formal proof of correctness and completeness of the new insufficiency algorithm is presented. Extensi..