Positive And Negative Diagnosis for Constraint Logic Programs in Terms of Proof Skeletons
Gérard Ferrand, Alexandre Tessier · 1997
The paper is motivated by the declarative debugging of constraint logic programs. It deals with the theoretical basis of declarative incorrectness diagnosis. It starts with a reformulation of the program semantics in terms of proof tree skeletons, which is suitable for declarative diagnosis study. The program semantics is explained in terms of positive semantics and negative semantics. The problem of wrong answer is treated as an incorrectness of the positive semantics while the problem of missing answer is treated as an incorrectness of the negative semantics. Incorrectness diagnosis is based on a well-founded relation over computation states. 1 Introduction The first motivation for a work on debugging is a computation producing a result which is considered as incorrect. Since there is a result, it is not an infinite computation. An incorrect result is called a symptom. This notion of symptom depends on some expected properties of the program, so a symptom is a result which is not ex...