use of correctness assertions in declarative diagnosis
We use assertions to reduce the quantity of queries in declarative diagnosis of logic programs. We first present a declarative diagnoser for normal logic programs. Given a bug symptom, the diagnoser first constructs a tree that models the execution of the bug symptom and then searches the tree for the bug that causes the bug symptom. We then incorporate into the diagnoser three tree transformations that prune the tree before it is searched. These transformations make use of two kinds of assertion about the correctness of the program and maintain the soundness and completeness of the diagnoser. These transformations reduce the size of the tree and thus reduce the quantity of queries imposed on the oracle.
correctness assertions declarative diagnosis logic programs