Declarative Incorrectness Diagnosis in Constraint Logic Programming.
F. Le Berre, Alexandre Tessier · 1996
Our concern in this paper is the declarative incorrectness diagnosis of constraint logic programs. Many techniques have been developed for LP but cannot be merely adapted to CLP. Constraint logic program semantics is redefined, using a reject criterion, in term of skeletons. Skeletons give an intrinsic definition to the answers provided by a program. The reject criterion can take into account the behaviour of an incomplete constraint solver. The main contribution of this paper is to prove that: if there exists a wrong answer then there is an incorrect clause in the program, and this clause occurs in the answer skeleton. Moreover, we give an algorithm which, given an incorrectness symptom, localizes a faulty clause and the circumstances of its incorrectness. Above all, there are new notions adapted to CLP framework.