@article {ABCF10,
	title = {An Integrated Framework for the Diagnosis and Correction of Rule-Based Programs},
	journal = {Theoretical Computer Science},
	volume = {411},
	year = {2010},
	note = {to appear},
	abstract = {We present a generic scheme for the declarative debugging of
programs that are written in rewriting-based languages that are equipped with narrowing.
Our aim is to provide an integrated development
environment in which it is possible to debug a program and
then correct it automatically.

Our methodology is based on the combination (in a single framework) of a semantics-based diagnoser that identifies those parts of the code that contain errors and an inductive learner that tries to repair them, once the bugs have been
located in the program. We develop our methodology in several steps. First, we associate with our programs a semantics
that is based on a (continuous) immediate consequence operator, T_R, which models the answers  computed by
narrowing  and is parametric w.r.t. the evaluation strategy,  which can be eager or lazy. Then, we show that, given the intended specification of a program R, it is possible to check the correctness of R by a single step of T_R.
In order to develop an effective debugging method,
we approximate the computed answers semantics of R
and derive a finitely terminating bottom-up abstract diagnosis method,
which can be used statically.

Finally, a bug-correction  program synthesis methodology attempts to correct the erroneous
components of the wrong code. We propose a hybrid, top-down (unfolding-based)
as well as bottom-up (induction-based), correction approach
that is driven by a set of evidence examples which are
automatically produced as an outcome by the diagnoser.
The resulting program is proven to be correct and complete w.r.t.
the considered example sets.

Our debugging framework does not require the user to  provide
error symptoms in advance or to answer difficult questions concerning
program correctness. An implementation of our debugging
system has been undertaken which
demonstrates the workability of our approach.},
	author = {Maria Alpuente and Demis Ballis and F. Correa and Moreno Falaschi}
}
