Abstract debugging of logic programs is an extension of declarative debugging, where we deal with specifications of operational properties, which can be characterized as abstractions of SLD-trees (observables). We introduce a simple and efficient method to detect incompleteness errors, which is based on the application of the immediate consequences operator to the specification. The method is proved to be correct and complete whenever the immediate consequences operator has a unique fixpoint. We then prove that this property is always satisfied if the program belongs to a large class of programs (acceptable programs). We finally show that the same property can be proved for any program, if the observable belongs to a suitable class of observables.

AADEBUG'95 Program

AADEBUG'95 home page