Three-valued declarative debugging

A general scheme for declarative debugging using three truth values is described in [NaishNaish2000a]; it is based on a more traditional two-valued scheme [NaishNaish1997]. Computations are represented as trees and debuggers search the tree for a buggy node. For diagnosing wrong answers in definite clause programs, the tree is a proof tree (see [LloydLloyd1984]): each node contains an atom $A$ which was proved in the computation and the children of the node contain the atoms in the body of the clause instance which was used at the top level of the proof of $A$. Each node has a truth value associated with it: correct, if the atom is true in the intended interpretation, erroneous, if the atom is false, or inadmissible, the third truth value. The truth value is determined by an ``oracle''. The user is asked questions and typically these are stored in a database to avoid repeated questions. The user may also be able to supply more general assertions or even runnable specifications [Drabent and MaluszynskiDrabent and Maluszynski1988].

If a node is erroneous but all its children are correct, it corresponds to an incorrect clause instance: the body is true but the head is false. This class of bugs was identified in the first work on declarative debugging [ShapiroShapiro1983]. Another class of bugs, related to inadmissibility, was identified in [PereiraPereira1986] and formalised more in [NaishNaish2000a]: nodes which are erroneous with no erroneous children but at least one inadmissible child. In a top-down execution this corresponds to a clause instance which causes a transition from admissible atoms to inadmissible atoms. It allows an inadmissible atom to be used in the (dubious) ``proof'' of a false atom. For such a bug to be manifest, the inadmissible call must succeed (if the inadmissible call fails the top level false atom would also fail, so there would be no bug symptom to diagnose). However, the diagnosis algorithm does not consider how or why the inadmissible call succeeds. The fact it succeeds is not considered an error -- the error is that it is called at all.

Several different instances of the three-valued declarative debugging scheme were identified, using different definitions of inadmissibility. Although our previous work on types and debugging provides the intuition for this paper, we do not rely on any particular definition of inadmissibility here. We simply assume that the programmer has some notion of (in)admissibility for ground atoms. If inadmissibility is identified with ill-typedness (as suggested in [PereiraPereira1986]) then the second class of bugs correspond to a form of type error discussed in [NaishNaish1992b]. However, this definition of inadmissibility does not lead to ideal behaviour of debuggers [NaishNaish2000a] and does not quite capture the intentions of programmers.

As well as considering types, programmers consider modes. A successful call to merge/3 in which just the last argument is not a sorted list is very different from a successful call where the second argument is not a sorted list. For merge([2,3], [1,2], [2,1,2,3]) we would consider that the output is wrong and there is a bug in merge/3 whereas for merge([2,3], [2,1], [2,1,2,3]) we would consider that the input is wrong and the bug is elsewhere. A more natural definition of inadmissibility for ground atoms is that the ``input'' arguments of the atom are ill-typed (or violate some condition). In [NaishNaish2000a] this definition of inadmissibility is related to a declarative view of modes [NaishNaish1996], which gives a more technical definition that captures the intuitive idea of input arguments being ill-typed.