Abstract Diagnosis Meta-Interpreters
Marco Comini
Dipartimento di Informatica, Università di Pisa,
Corso Italia 40, 56125 Pisa, Italy
comini-at-di.unipi.it
Abstract:
We show how declarative diagnosis techniques can be extended to cope
with verification of operational properties, such as computed and
correct answers, and of abstract properties, such as depth(k)
answers and groundness dependencies. The extension is achieved by
using a simple semantic framework, based on abstract interpretation.
The resulting technique (abstract
diagnosis) leads to elegant bottom-up and top-down
verification methods, which do not require to determine the symptoms in
advance, and which are effective in the case of
abstract properties described by finite domains.
Keywords: Logic Programming, Declarative
diagnosis, Verification, Semantics, Debugging.
Marco Comini <comini-at-di.unipi.it>