We report on work in progress aiming to add blame features to property-based-testing in logic programming, in particular w.r.t. the mechanized meta-theory model checker Check. Once the latter reports a counterexample to a property stated in Prolog, a combination of abduction and proof explanation tries to help the user to locate the part of the program that is responsible for the unintended behavior. To evaluate whether these explanations are in fact useful, we need an unbiased collection of faulty programs, where the bugs location is unknown to us. We have thus implemented a mutation testing tool for Prolog that generates such a set. Preliminary experiments point to the usefulness of our blame allocator. The mutator is of independent interest, allowing us to gauge the e ectiveness of the various strategies of Check in nding bugs in Prolog speci cations.
Property-based testing [
PBT has also a pedagogical value and our students seem to enjoy using it during their functional programming coursework. After type-checking succeeds, the PBT message \Ok, passed 100 tests ", whereby the tool reports the failure to refute some property, gives the students a warm fuzzy feeling of having written correct code. This feeling comes to a sudden halt when a counterexample is reported, signaling a mismatch between code and speci cation. In our experience, the student freezes, disconnects the brain, typically uttering something like \Prof, there's a problem here", and refrains from taking any further action.
Now, no-one likes to be wrong, not only students, and this is why testers and programmers may be di erent entities in a software company. While a counterexample to a property is a more useful response than, say, the false of a failed logic programming query | or a core dump for that matter | we can do better and go beyond the mere reporting of that counterexample; namely, try to circumscribe the origin of the latter. After all, the program under test may be arbitrarily large and, arguably, even partial solutions pinpointing the slice of the program involved in an error can help pursuing the painful process of bug xing.
\Where do bugs come from?" is a crucial question that has sparked a huge
amount of research. In this short paper, we report on preliminary work on
addressing a much, much smaller sub-problem: rst, the domain is mechanized
meta-theory model-checking [
Secondly, and consequently, we restrict to (nominal) logic programming, that
is to encoding written in Prolog [
Our blame tool is written in Prolog, a choice taken mostly out of convenience, since it allows us the exibility to experiment with ideas by metainterpretation, rather then wiring them in for good in Prolog's OCAML implementation. In fact, meta-interpreters are forbidden by the interaction of the strongly-typed nature of Prolog, together with its being a rst order language.
We picture the architecture of the tool in Fig. 1: we write models and specs in Prolog and we pass them to Check for validation. If a counterexample is found, we translate the
Prolog code to standard Prolog and we feed it to our explanation tool together with the said counterexample.
The tool returns an explanation that can be hopefully used to debug the
Prolog model. And so on. This architecture, of course, applies only to Fig. 1. Flow of the blame game
Prolog code that can be faithfully executed in standard Prolog and therefore does not support natively nominal features. 2
Suppose that we wish to study the following grammar (adapted from [
pred ss(list(ab)). pred bb(list(ab)).
pred aa(list(ab)). pred count(ab,list(ab),nat). ss([]). ss([b|W]) :- ss(W). ss([a|W]) :- bb(W). bb([b|W]) :- ss(W). bb([a|VW]) :- bb(V), bb(W), append(V,W,VW). aa([a|W]) :- ss(W). aa([b|VW]) :- aa(V), aa(W), append(V,W,VW) However, our encoding is awed | we ask the reader to suspend her disbelief, since the bug is quite apparent. Still, it is easy to conjure an analogous scenario where the grammar has dozens of productions and the bugs harder to spot.
We shall use Check to debug it. We split the characterization of the grammar into soundness and completeness properties: #check "sound" 10 : ss(W), count(a,W,N1), count(b,W,N2) => N1 = N2. #check "compl" 10 : count(a,W,N), count(b,W,N) => ss(W).
The tool dutifully reports (at least) two counterexamples: Checking for counterexamples to sound: ss(W), count(a,W,N1), count(b,W,N2) => N1 = N2 Checking depth 1 2 3 Total: 0.000329 s: N1 = z, N2 = s(z), W = [b] compl: count(a,W,N), count(b,W,N) => ss(W) Checking depth 1 2 3 4 5 6 7 8 9 Total: 0.016407 s: N = s(z), W = [b,a] Now that we have the counterexamples, where is the bug? More precisely, which clause(s) shall we blame?
The #check pragma of Check corresponds to speci cation formulas of the form 8X: G
A where G is a goal and A an atomic formula (including equality and freshness constraints). A ( nite) counterexample is a grounding substitution providing values for X that satisfy the negation of (1): that is, such that (G) is derivable, but the conclusion (A) is not. In this paper, we identify negation with negationas-failure (NAF) and we will not make essential use of nominal features.
The tool synthesizes (trusted) type-based exhaustive generators for the free variables of the conclusion, so that NAF executes safely. A complete search strategy, here naive iterative deepening, searches for a proof of: 9X: : G ^ gen[[ ]](X1) ^ ^ gen[[ ]](Xn) ^ not(A) (1) (2) To wit, completeness will be the query:
9W. count(a,W,N), count(b,W,N), gen ablist(W), not(ss(W)).
The predicate gen ablist(W) corresponds to the generator formula gen[[list(ab)]](W ) for lists of a's and b's. In the soundness query we know by mode analysis that we do not need generators for numerals.
For a query such as the above and more in general such as (2) to unexpectedly succeed, two (possibly overlapping) things may have gone wrong [22]: MA: the atom A fails, whereas it belongs to the intended interpretation of its de nition (missing answer ); WA: a bug in G creates some erroneous bindings, which again make A fail (wrong answer ): some atom in G succeeds but it is not in the intended model.
Our \old-school" idea consists in coupling 1) abduction [
Of course, since we do not know, in principle, which is which and the two
phenomena can occur simultaneously, we are going to use some simple
heuristics to drive this process. What we would rather keep our distance from is full
declarative debugging (see e.g., [
Our notion of abduction is a simple-minded proof procedure that nds a set of assumptions such that ; ` G0, but 6` G0 for given and G0. In our limited setting here of rst-order logic programming, we, as expected, internalize as a xed program P and we see as a (additive) conjunction of atoms A. An abduction procedure depends on the selection of what the abducibles are. This choice is related to which part of the program we trust and which we want to investigate. The system will suggest abducibles based on the dependency graph of the conclusion of the property under investigation, but we give the nal say to the user, while trying to make it easy to change one's mind.
We now work through the above example. Our tool reads into standard Prolog the Prolog les, adding names to rules and treating type information as inactive predicates via appropriate operator declarations. For example, here is the ss predicate and related declarations: ab :: type. a :: ab. b :: ab. pred ss(list(ab)). ss([]) :- rule(s1). ss([b|W]) :- rule(s2), ss(W). ss([a|W]) :- rule(s3), bb(W).
To begin with, we need to decide what to investigate and what to trust. Consistently with our faith in properties, we will trust count and append: trusted(append(_,_,_)). trusted(count(_,_,_)).
The dependency graph suggests (quite unhelpfully here) to put all of aa,bb,ss as abducibles. assumable(ss(_)). assumable(bb(_)). assumable(aa(_)).
For exposition sake, let us investigate the completeness bug rst, that is the failure of ss([b,a]). This is a case of MA, since that string should be accepted. The tool returns this explanation: ss([b,a]) for rule s2, since: ss([a]) for rule s3, since:
bb([]) for assumed Once you get used to the fairly primitive verbalization, you see that if it were the case that bb([]) holds, then ss([b,a]) would have succeeded and the counterexample not found. However, there is no production for b accepting the empty string, so we should blame ss, namely either s2 or s3. By comparing the clauses to the productions they are supposed to encode we see that the body of s2 should be aa(W) and not ss(W).
For the soundness bug, it is obvious that it is a case of WA. We trust unication, the more since here it is just syntactic equality. Hence we need to understand what went wrong in the premise ss(W) | remember, we trust count. The tool answers: ss([b]) for rule s2, since:
ss([]) for fact s1.
Since s1 is OK, it is again s2's fault. Once we x that bug, Check does not report any more issues. 3
It is natural to split the de nitions of the program under test into builtin, which we assume to be non problematic, and those we want to look into (pred, for compatibility with Prolog type declarations). By default, every user-de ned predicate is under suspicion. However, once a pred overcomes our scrutiny, or we believe it, perhaps temporarily, to be well-behaved, we can graduate it to being trusted and let it o the hook. Builtins and trusted predicates are not meta-interpreted, that is we simply call them. Abducibles must be non-trusted pred de nitions.
The abduction/explanation mechanism can be formulated in terms of a
calculus AE (P ), based on the notion of proof-tree (see [
G r A A asm
G1 G2 G1 ^ G2 ^
Given a xed program P , rule r corresponds to a single SLD step with clause A :- rule(r),G in P . Rules >; ^; _ are self-explanatory. Rule asm closes a proof whenever A is declared as abducible. The last two rules are somewhat di erent (and hence the double bar): builtin and trusted both end the proof returning an answer substitution: in the rst case if there is an external computation of the builtin predicates. In the trusted case, we apply the rule only if there is a closed proof-tree, i.e. without assumptions returning . In fact, this is not technically a nitary rule, in the same sense that NAF is not; nevertheless, the way in which we use the calculus, namely by replaying already found counterexamples, will ensure that the rule is e ective. For example, the second clause for bb asks for a computation of append(V,W,VW) where VW is ground. This is simply executed as a Prolog query outside the calculus, returning the ground substitution .
The meta-interpreter computes over those proof-trees, simultaneously collecting abducible assumptions and Prolog terms encoding the proof-tree itself, to be later verbalized. The meta-interpreter enjoys, we claim, the following correctness property: a proof-tree computed by the meta-interpreter is a proof in the calculus above. Conversely, for all goals G, if there is proof in AE (P ) of G , the interpreter will produce a more general proof-tree for G with the same sequence of rules.
Proof verbalization Clearly, proof-trees of height 2 as the ones occurring in
Section 2 are not that di cult to interpret. However, we address the general case by
o ering various levels of explanation, from printing out the whole tree to instead
presenting a skeleton containing only the involved rule names. We currently do
this with di erent forms of printf, while it would be more exible to use a form
of proof distillation [
Heuristics Suppose you have a counterexample for property 8X: G A: how do you go about trying to decide whether it is a MA or a WA? We suggest the following steps with the blame tool: 1. if A is a builtin (including constraints) or a trusted predicate, it is clear that it is a case of WA and we directly verbalize the proof tree of the premise(s). 2. Otherwise, we use abduction to investigate the failure of A; start by adding A and its dependency graph as abducibles. 2.1 If the failure of A points to a case of MA, use the explanation mechanism to see if there is a clause missing in the program or which clause is otherwise involved. 2.2 If the set of assumptions found by abduction is \unreasonable", that is we have atoms that should not hold in the intended model, it is likely a case of WA and we turn to verbalizing the proof-tree for G. 4
Mutation analysis [
What is the connection with our endeavor? A killed mutant is a good
candidate for blame assignment, since it should simulate reasonable bugs that occur
in a program without being planted by ourselves. This is justi ed by the
\competent programmer assumption" [
Check with other PBT tools | but this is obviously biased, labor-intensive and very hard to scale.
We have thus developed a mutator for Prolog programs, with an emphasis
on trying to devise mutation operators for our intended domain, namely
models of programming languages artifacts. Those operators specify the mutations
that the tool will inject and therefore a mutator is as e ective as operators are
relevant. Mutation testing comes from imperative languages and the operators
thereby are pretty useless. Even operators proposed for declarative programs [
Keeping in mind that we strive to produce mutants that cannot be detected already by static analysis such as type checking in Prolog or singleton variable analysis in standard Prolog, we have converged on this initial set of operators: Clause mutations: deletion of a predicate in the body of a clause, deleting the whole clause if a fact. Replacement of disjunction by conjunction and vice versa.
Operator mutations: arithmetic and relational operator mutation, say < in .
Variable mutations: replacing a variable with an (anonymous) variable and vice versa.
Constant mutations: replacing a constant by a constant (of the same type), or by an (anonymous) variable and vice versa.
Prolog-speci c Removing freshness annotations (#), changing their scope or confusing them with equality.
In our implementation, a simple driver produces a given number of randomly generated mutants from an Prolog source P and a list LM of mutation operators. At every generation step we make a random choice of operator in LM and of clause in P such that the operator is applicable, in the spirit of [27]. If the mutant is new, i.e., it has not been produced before, it is passed to the next phase: here, we try to weed out semantically equivalent mutants following the proposal in [23] of comparing them with their ancestor on a nite portion of input. We achieve this by asking Check to try to refute their equivalence up to a given bound. Keeping the bound small makes this a fairly quick, if imperfect, lter. If the mutant survives, we pass it again to Check, this time under the property that the original model was supposed to satisfy. If it fails, we go back to the ow in Fig. 1.
We have been experimenting with the mutation and explanation of three
main case studies:
1. The preservation and progress property for the typed arithmetic language
in Chapter 8 of [25].
2. Non-interference for static ow information systems, which we had started
to address in [
We have given an \appetizer" of our approach to blame assignment for counterexamples found by PBT. We have used old-fashioned ideas in the literature, such as abduction and explanation trees, trying to strike a reasonable balance with declarative debugging: we only ask for the user's input when we let her decide if the answer given by abduction is sensible; this is quite di erent, we argue, from the the constant prodding that declarative debugging requires. Our approach is also much simpler (perhaps simple-minded) than previous work aiming to explain why a query is true or false in a model, typically under the answer set semantics, as in e.g. [26].
There is so much work that lies in front of us: we need to gather more experience using the tool, especially with a user who is di erent from the authors. This is particularly crucial for tuning the amount of details in proof verbalization.
Mutation testing for Prolog is of independent interest, besides the way we have used it here. It allows us to evaluate how well Check performs in spotting bugged models, similarly to the interaction of MuCheck [20] with QuickCheck. However, designing mutation operators that make sense in our intended domain is an open question, see [24] for the more general issue of mutations vs. real faults. The operators that we have proposed are a starting point, but it would be nice to provide the user with a basic DSL to encode her own.
Finally, the main drawback of the current setup is that we can play the blame game only for Prolog programs that are indeed Prolog code, i.e. that do not use the nominal features, since they cannot be faithfully replayed in standard Prolog. The new version, already under development, will instead handle the whole of
Prolog, by porting the blame tool to the latter, where Prolog's programs are
rei ed in object-level clauses following the two-level approach [