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.