Abstract Correction of First-Order Functional Programs
Marı́a Alpuente, Demis Ballis, Santiago Escobar, Moreno Falaschi, Salvador Lucas · Electronic Notes in Theoretical Computer Science · 2003
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[6]. 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.