Algorithmic program debugging

Algorithmic debugging is a debugging technique that has been extended to practically all programming paradigms. Roughly speaking, the technique constructs an internal representation of all (sub)computations performed during the execution of a buggy program; and then, it asks the programmer about the correctness of such computations.

During his PhD research at Yale University Ehud Shapiro developed the first systematic and principled approach to program debugging, a craft practiced by every programmer but till then without any theoretical foundation. 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. In case of logic programs, the intended behavior of the program is a model (a set of simple true statements) and bugs are manifested as program incompleteness (inability to prove a true statement) or incorrectness (ability to prove a false statement). The algorithm would identify a false statement in the program and provide a counter-example to it or a missing true statement that it or its generalization should be added to the program. A method to handle non-termination was also developed. Shapiro implemented the method of algorithmic debugging in Prolog for the debugging of logic programs and his PhD thesis describing this work was selected as a 1982 ACM Distinguished Dissertation. Since then the method of algorithmic debugging has been applied to many programming languages and systems. Three decades later, algorithmic debugging, also known as declarative debugging, is still an active field of computer science research and will probably remain so for decades as no panacea is in sight.