Algorithmic program debugging

Algorithmic debugging (also called declarative debugging) is a debugging technique that compares the results of sub-computations with what the programmer intended. The technique constructs an internal representation of all computations and sub-computations performed during the execution of a buggy program and then asks the programmer about the correctness of such computations. By asking the programmer questions or using a formal specification, the system can identify precisely where in a program a bug is located. Debugging techniques can dramatically reduce the time and effort spent on debugging.

Program debugging is an extremely common part of software development. Until the 1980s the craft of program debugging, practiced by every programmer, was without any theoretical foundation. In the early 1980s, systematic and principled approaches to program debugging were developed. In general, a bug occurs when a programmer has a specific intention regarding what the program should do, yet the program actually written exhibits a different behavior than intended in a particular case. One way of organizing the debugging process is to automate it (at least partially) via an algorithmic debugging technique. The idea of algorithmic debugging is to have a tool that guides the programmer along the debugging process interactively: It does so by asking the programmer about possible bug sources. The algorithmic debugging technique constructs an internal representation of all computations and sub-computations performed during the execution of a buggy program (an execution tree). Then, it asks the programmer about the correctness of such computations. The programmer answers "YES" when the result is correct or "NO" when the result is wrong. Some algorithmic debuggers also accept the answer "I don't know" when the programmer cannot give an answer (e.g., because the question is too complex). Thus, the answers of the programmer guide the search for the bug until it is isolated by discarding correct parts of the program. The algorithmic debugging process finds one bug at a time. In order to find different bugs, the process should be restarted again for each different bug.

...
Wikipedia