Abstract Correction of first-order Functional Programs

DEBUSSY is an (abstract) declarative diagnosis tool for functional programs which are written in OBJ style. The tool does not require the user to either provide error symptoms in advance or answer any question concerning program correctness. In this paper, we formalize an inductive learning methodology for repairing program bugs in OBJ-like programs, which is based on the so-called example-guided unfolding (Bostrom and Idestam-Alquist, 1999). Correct programs are synthesized by unfolding and removing rules of the faulty program. Rules to be unfolded (deleted) are selected according to the examples, which can be automatically generated as an outcome by the DEBUSSY diagnoser. © 2003 Published by Elsevier Science B.V. Abstract Correction; Abstract Interpretation; First Order Functional Programs; Inductive Learning; Program Transformation