Declarative Diagnosis Revisited
Marco Comini, G Levi, G. Vitiello · The MIT Press eBooks · 1995
Abstract We extend the declarative diagnosis methods to the diagnosis w.r.t. com-puted answers. We show that absence of uncovered atoms implies complete-ness for a large class of programs. We then define a top-down diagnoser,which uses one oracle only, does not require to determine in advance thesymptoms and is driven by a (finite) set of goals. Finally we tackle the prob-lem of effectivity, by introducing (finite) partial specifications. We obtain aneffective diagnosis method, which is weaker than the general one in the caseof correctness, yet can efficiently be implemented in both a top-down and ina bottom-up style.Keywords: Declarative diagnosis, Verification, Semantics, Debugging 1 Introduction The diagnosis problem can formally be defined as follows. Let P be a pro-gram, [[P]] be the behavior of P w.r.t. the observable property α, and I bethe specification of the intended behavior of P w.r.t. α. The diagnosis con-sists of comparing [[P]] and I and determining the “errors” and the programcomponents which are sources of errors, when [[P]] 6= I. The formulationis parametric w.r.t. the property considered in the specification I and inthe actual behavior [[P]]. Declarative diagnosis [15, 14, 11, 8] is concernedwith model-theoretic properties. The specification is the intended declara-tive semantics (the least Herbrand model in [15] and the set of atomic logicalconsequences in [8]).Abstract diagnosis [4, 5] is a generalization of declarative diagnosis, wherewe consider operational properties, i.e., observables (an observable is anyproperty which can be extracted from a goal computation, i.e., observablesare abstractions of SLD-trees). An example of a useful observable is com-puted answers. The diagnosis w.r.t. computed answers is expected to bemore precise than the declarative diagnoses in [15] and [8], which can bereconstructed in terms of the observables ground instances of computed an-swers and correct answers respectively [5]. The semantics involved in the