BUGGY 2.0

System Description

Buggy is a tool being able to detect and automatically repair eager as well as lazy functional logic programs w.r.t. a specification of a given intended semantics. Such a specification is formalized by means of a functional logic program.

The system makes use of abstract interpretation to statically recognize faulty program rules w.r.t. a given specification. Then, programs are automatically repaired using a top-down, example-guided synthesis technique -based on unfolding transformations- which purifies wrong programs from incorrect answers. The synthesis is driven by automatically generated, positive and negative examples which respecitvely model expected and unexpected program behaviors. Since this approach is not always sufficient to come up with satisfactory corrections when faulty programs are not overly general (that is, faulty programs not able to derive all the positive examples generated), the system has been coupled with FLIP, a bottom-up synthesis tools developed by Ferri, Hernandez and Ramirez, which allows one to transform programs into overly general programs to which we can subsequently apply our top-down correction process.

Rougly speaking, given a program and the specification of its itended semantics, the debugging process proceeds as follows:

  1. Buggy locates faulty rules (if any).
  2. Then, it automatically generates positive and negative example sets using the outcome of the previous verification phase.
  3. If the program to be debugged is not overly-general, the bottom-up learner FLIP is executed to get an overly general program.
  4. Finally, the obtained overly general program is repaired by using the Buggy's correcton facilities.

For a thorough description of our debugging methodology, please refer to our paper.

Examples

Here you can find several experiments which we carried out with our debugging tool. For each experiment we provide several tables containing

  • the debugger inputs (program and specification);
  • the example sets automatically generated by Buggy ;
  • the set of examples and the background knowledge taken in input by FLIP along with the resulting overly general program, whenever program generalization is needed;
  • the final corrected program along with some comments about the entire code revision process.
Assumptions

In what follows...

  • Programs and specifications are Conditional Term Rewriting Systems (CTRS) expressed using the Buggy functional logic syntax.
  • Examples sets consist of equations of ground terms such that the lhs of each equation is a pattern and the rhs is a constructed term.
  • Rules which are detected as faulty by Buggy are marked in light purple. Rules computed by FLIP are marked in blue. Corrections are marked in dark green.
  • Value k is the natural number used to calculate the underapproximation I-, it influences the search for the wrong rules and the automatic generation of the example sets.
  • C is an input parameter representing a list of ground constructor terms which are used to generate ground examples.
  • For each experiment the k and C values we used are shown in the Comments column of the tables containing the corrected programs.

Wrong program Specification

 even(0) = true 
 even(s(X)) = even(X) 
 fib(0) = 0 
 fib(s(0)) = s(0) 
 fib(s(s(X))) = sum(fib(s(X)),fib(X)) 
 sum(X,0) = X 
 sum(X,s(Y)) = s(sum(X,Y)) 
 even(0) = true 
 even(s(s(X))) = even(X) 
 fib(0) = s(0) 
 fib(s(0)) = s(0) 
 fib(s(s(X))) = sum(fib(s(X)),fib(X)) 
 sum(X,0) = X 
 sum(X,s(Y)) = s(sum(X,Y)) 

Positive example set Negative example set

 even(s(s(0))) = true. 
 even(s(s(s(s(0))))) = true. 
 even(s(s(s(s(s(s(0))))))) = true. 
 even(s(s(s(s(s(s(s(s(0))))))))) = true. 
 fib(0) = s(0). 

 even(s(0)) = true. 
 fib(0) = 0.  

FLIP input Overly general program

 Examples

 fib(0) = s(0) 

 Background theory

 fib(s(0)) = s(0)
 fib(s(s(X))) = sum(fib(s(X)),fib(X))
 sum(X,0) = X
 sum(X,s(Y)) = s(sum(X,Y))


 fib(0) = s(0) 
 fib(s(0)) = s(0) 
 fib(s(s(X))) = sum(fib(s(X)),fib(X)) 
 sum(X,0) = X 
 sum(X,s(Y)) = s(sum(X,Y)) 
 even(0) = true
 even(s(X)) = even(X)


Corrected program Comments

 even(0) = true
 even(s(s(X))) = even(X)
  fib(0) = s(0)
 fib(s(0)) = s(0)
 fib(s(s(X))) = sum(fib(s(X)),fib(X))
 sum(X,0) = X
 sum(X,s(Y)) = s(sum(X,Y))
 k=3; 
 C=[0,s(0)] 

 View the outcome 
Wrong program Specification

 odd(0) = true 
 odd(s(X)) = odd(X) 
 even(0) = true 
 even(s(s(X))) = even(X) 
 odd(s(X)) = true :- even(X) = true 

Positive example set Negative example set

 odd(s(0)) = true. 
 odd(s(s(s(0)))) = true. 
 odd(s(s(s(s(s(0)))))) = true. 
 odd(s(s(s(s(s(s(s(0)))))))) = true. 

 odd(0) = true. 
 odd(s(s(0))) = true. 

Corrected program Comments

 odd(s(0)) = true 
 odd(s(s(X))) = odd(X) 

 k=3; 
 C=[0,s(0)] 

 View the outcome 
Wrong program Specification

 spanishdiet(X,Y) = diet(X,Y). 
 diet(X,Y) = and(food(X),drink(Y)). 
 and(true,X) = X. 
 food(X) = otherfood(X). 
 food(X) = spanishfood(X). 
 drink(X) = otherdrink(X). 
 drink(X) = spanishdrink(X). 
 spanishfood(paella) = true. 
 spanishfood(gazpacho) = true. 
 spanishfood(tapas) = true. 
 spanishfood(fideua) = true. 
 otherfood(lasagne) = true. 
 otherfood(sushi) = true. 
 otherfood(kebab) = true. 
 otherfood(bigmac) = true. 
 spanishdrink(sangria) = true. 
 spanishdrink(rioja) = true. 
 spanishdrink(aguadevalencia) = true. 
 otherdrink(cola) = true. 
 otherdrink(beer) = true. 
 otherdrink(sake) = true. 
 otherdrink(grappa) = true. 
 spanishdiet(fideua,sangria) = true. 
 spanishdiet(fideua,rioja) = true. 
 spanishdiet(fideua,aguadevalencia) = true. 
 spanishdiet(paella,sangria) = true. 
 spanishdiet(paella,rioja) = true. 
 spanishdiet(paella,aguadevalencia) = true. 
 spanishdiet(gazpacho,sangria) = true. 
 spanishdiet(gazpacho,rioja) = true. 
 spanishdiet(gazpacho,aguadevalencia) = true. 
 spanishdiet(tapas,sangria) = true. 
 spanishdiet(tapas,rioja) = true. 
 spanishdiet(tapas,aguadevalencia) = true. 

Positive example set Negative example set

 spanishdiet(fideua,sangria) = true. 
 spanishdiet(fideua,rioja) = true. 
 spanishdiet(fideua,aguadevalencia) = true. 
 spanishdiet(paella,sangria) = true. 
 spanishdiet(paella,rioja) = true. 
 spanishdiet(paella,aguadevalencia) = true. 
 spanishdiet(gazpacho,sangria) = true. 
 spanishdiet(gazpacho,rioja) = true. 
 spanishdiet(gazpacho,aguadevalencia) = true. 
 spanishdiet(tapas,sangria) = true. 
 spanishdiet(tapas,rioja) = true. 
 spanishdiet(tapas,aguadevalencia) = true. 

 spanishdiet(kebab,grappa) = true. 
 spanishdiet(sushi,grappa) = true. 
 spanishdiet(kebab,rioja) = true. 
 spanishdiet(sushi,rioja) = true. 

Corrected program Comments

 spanishdiet(X,Y) = diet(X,Y). 
 diet(X,Y) = and(food(X),drink(Y)). 
 and(true,X) = X. 
 food(X) = spanishfood(X). 
 drink(X) = spanishdrink(X). 
 spanishdrink(aguadevalencia) = true. 
 spanishdrink(rioja) = true. 
 spanishdrink(sangria) = true. 
 spanishfood(fideua) = true. 
 spanishfood(tapas) = true. 
 spanishfood(gazpacho) = true. 
 spanishfood(paella) = true. 
 otherdrink(sake) = true. 
 otherdrink(beer) = true. 
 otherdrink(cola) = true. 
 otherfood(bigmac) = true. 
 otherfood(lasagne) = true. 

 k=3; 
 C=[grappa,rioja,sushi,kebab]. 

 No rules have been changed.
 Only a rule deletion has been
 performed.

 View the outcome 
Wrong program Specification

 noemptyapp([],[X1|Y1]) = [X1|Y1]. 
 noemptyapp([X1|Z1],[X2|Y2]) = [X1|noemptyapp(Z1,[X2|Y2])]. 
 noemptyapp([X1|Y1],[X2|Y2]) = append([X1|Y1],[X2|Y2]). 
 append([],W) = W. 
 append([X1|Z1],W1) = [X1|append(Z1,W1)]. 

Positive example set Negative example set

 noemptyapp([[a,a],a],[[a,a],a,a]) = [[a,a],a,[a,a],a,a]. 
 noemptyapp([[a,a],a],[[a,a],a]) = [[a,a],a,[a,a],a]. 
 noemptyapp([[a,a],a],[[a],a,a]) = [[a,a],a,[a],a,a]. 
 noemptyapp([[a,a],a],[[a],a]) = [[a,a],a,[a],a]. 
 noemptyapp([[a],a],[[a,a],a,a]) = [[a],a,[a,a],a,a]. 
 noemptyapp([[a],a],[[a,a],a]) = [[a],a,[a,a],a]. 
 noemptyapp([[a],a],[[a],a,a]) = [[a],a,[a],a,a]. 
 noemptyapp([[a],a],[[a],a]) = [[a],a,[a],a]. 
 noemptyapp([[a],a,a],[[a],a]) = [[a],a,a,[a],a]. 
 noemptyapp([[a],a,a],[[a],a,a]) = [[a],a,a,[a],a,a]. 
 noemptyapp([[a],a,a],[[a,a],a]) = [[a],a,a,[a,a],a]. 
 noemptyapp([[a],a,a],[[a,a],a,a]) = [[a],a,a,[a,a],a,a]. 
 noemptyapp([[a,a],a,a],[[a],a]) = [[a,a],a,a,[a],a]. 
 noemptyapp([[a,a],a,a],[[a],a,a]) = [[a,a],a,a,[a],a,a]. 
 noemptyapp([[a,a],a,a],[[a,a],a]) = [[a,a],a,a,[a,a],a]. 
 noemptyapp([[a,a],a,a],[[a,a],a,a]) = [[a,a],a,a,[a,a],a,a]. 

 noemptyapp([],[[a],a]) = [[a],a]. 
 noemptyapp([],[[a],a,a]) = [[a],a,a]. 
 noemptyapp([],[[a,a],a]) = [[a,a],a]. 
 noemptyapp([],[[a,a],a,a]) = [[a,a],a,a]. 

Corrected program Comments

 noemptyapp([X1,X2],[X3|Y3]) = [X1,X2,X3|Y3]. 
 noemptyapp([X1,X2,X3,X4|Y1],[X5|Y2]) = [X1,X2,X3,X4|noemptyapp(Y1,[X5|Y2])]. 
 noemptyapp([X1,X2,X3],[X4|Y5]) = [X1,X2,X3,X4|Y5]. 
 noemptyapp([X1],[X2|Y2]) = [X1,X2|Y2]. 

 k=1; 
 C=[[a],[a,a]] 

Outcome correct w.r.t. the example sets, but not w.r.t. the intended
semantics

View the outcome 
Wrong program Specification

 oddapp([],X) = X. 
 oddapp([X1|Z1],W1) = [X1|oddapp(Z1,W1)]. 

 oddapp([X1],[X2|Y2]) = [X1,X2|Y2]. 
 oddapp([X1,Y1|Z1],W1) = Z:- Z = [X1,Y1|oddapp(Z1,W1)]. 

Positive example set Negative example set

 oddapp([[a]],[[a],a]) = [[a],[a],a]. 
 oddapp([[a]],[[a],a,a]) = [[a],[a],a,a]. 
 oddapp([[a]],[[a,a],a]) = [[a],[a,a],a]. 
 oddapp([[a]],[[a,a],a,a]) = [[a],[a,a],a,a]. 
 oddapp([[a,a]],[[a],a]) = [[a,a],[a],a]. 
 oddapp([[a,a]],[[a],a,a]) = [[a,a],[a],a,a]. 
 oddapp([[a,a]],[[a,a],a]) = [[a,a],[a,a],a]. 
 oddapp([[a,a]],[[a,a],a,a]) = [[a,a],[a,a],a,a]. 
 oddapp([[a,a],[a,a],a],[a,a]) = [[a,a],[a,a],a,a,a]. 
 oddapp([[a,a],[a,a],a],[a]) = [[a,a],[a,a],a,a]. 
 oddapp([[a,a],[a],a],[a,a]) = [[a,a],[a],a,a,a]. 
 oddapp([[a,a],[a],a],[a]) = [[a,a],[a],a,a]. 
 oddapp([[a],[a,a],a],[a,a]) = [[a],[a,a],a,a,a]. 
 oddapp([[a],[a,a],a],[a]) = [[a],[a,a],a,a]. 
 oddapp([[a],[a],a],[a,a]) = [[a],[a],a,a,a]. 
 oddapp([[a],[a],a],[a]) = [[a],[a],a,a]. 
 oddapp([a],[a,a]) = [a,a,a]. 
 oddapp([a],[a]) = [a,a]. 

 oddapp([],[a]) = [a]. 
 oddapp([],[a,a]) = [a,a]. 
 oddapp([[a],a],[a]) = [[a],a,a]. 
 oddapp([[a],a],[a,a]) = [[a],a,a,a]. 
 oddapp([[a,a],a],[a]) = [[a,a],a,a]. 
 oddapp([[a,a],a],[a,a]) = [[a,a],a,a,a]. 

Corrected program Comments

 oddapp([X1],Y1) = [X1|Y1]. 
 oddapp([X1,X2|Y1],Y2) = [X1,X2|oddapp(Y1,Y2)]. 

 k=1; 
 C=[[a],[a,a]] 

 View the outcome 
Wrong program Specification

 sum(X,0) = 0 
 sum(X,s(Y)) = s(sum(0,Y)) 

 sum(0,Y) = Y 
 sum(s(X),Y) = s(sum(X,Y)) 

Positive example set Negative example set

 sum(s(s(s(s(s(0))))),0) = s(s(s(s(s(0))))).
 sum(s(s(s(s(s(0))))),s(0)) = s(s(s(s(s(s(0)))))).
 sum(s(s(s(s(s(0))))),s(s(0))) = s(s(s(s(s(s(s(0))))))).
 sum(s(s(s(s(0)))),s(s(0))) = s(s(s(s(s(s(0)))))).
 sum(s(s(s(s(0)))),s(0)) = s(s(s(s(s(0))))).
 sum(s(s(s(s(0)))),0) = s(s(s(s(0)))).
 sum(s(s(s(0))),0) = s(s(s(0))).
 sum(s(s(s(0))),s(0)) = s(s(s(s(0)))).
 sum(s(s(s(0))),s(s(0))) = s(s(s(s(s(0))))).
 sum(s(s(0)),s(s(0))) = s(s(s(s(0)))).
 sum(s(s(0)),s(0)) = s(s(s(0))).
 sum(s(s(0)),0) = s(s(0)).
 sum(s(0),s(s(0))) = s(s(s(0))).
 sum(s(0),s(0)) = s(s(0)).
 sum(s(0),0) = s(0).
 sum(0,s(s(0))) = s(s(0)).
 sum(0,s(0)) = s(0).
 sum(0,0) = 0.

 sum(s(0),0) = 0.
 sum(s(s(0)),0) = 0.
 sum(s(s(0)),s(0)) = s(0).
 sum(s(0),s(0)) = s(0).
 sum(s(0),s(s(0))) = s(s(0)).
 sum(s(s(0)),s(s(0))) = s(s(0)).
 sum(s(s(0)),s(s(s(0)))) = s(s(s(0))).
 sum(s(0),s(s(s(0)))) = s(s(s(0))).

FLIP input Overly general program

 Examples

 All the positive examples shown in the table above.

 Background theory

 None

 sum(X,s(Y)) = sum(s(X),Y)
 sum(X,0) = X

Corrected program Comments

 sum(X,s(Y)) = sum(s(X),Y)
 sum(X,0) = X

 k=3; 
 C=[0,s(0),s(s(0))] 

 The overly general program is already correct.
 No top-down correction is necessary.
Wrong program Specification

 fact(0) = sum(0,0)
 fact(s(X)) = mult(s(X),fact(X))
 mult(X,0) = 0
 mult(s(X),Y) = sum(Y,mult(X,Y))
 sum(X,0) = X
 sum(X,s(Y)) = s(sum(X,Y))

 fact(0)=s(0)
 fact(s(X))=mult(s(X),fact(X))
 mult(X,0)=0
 mult(s(X),Y)=sum(Y,mult(X,Y))
 sum(X,0)=X
 sum(X,s(Y))=s(sum(X,Y))

Positive example set Negative example set

 mult(s(s(s(s(0)))),0) = 0.
 mult(s(s(s(0))),0) = 0.
 sum(s(0),s(s(s(s(0))))) = s(s(s(s(s(0))))).
 sum(0,s(s(s(s(0))))) = s(s(s(s(0)))).
 mult(s(0),0) = 0.
 mult(s(s(0)),0) = 0.
 sum(0,s(s(s(0)))) = s(s(s(0))).
 sum(s(0),s(s(s(0)))) = s(s(s(s(0)))).
 sum(s(0),s(s(0))) = s(s(s(0))).
 sum(0,s(s(0))) = s(s(0)).
 sum(s(0),s(0)) = s(s(0)).
 sum(0,s(0)) = s(0).
 fact(0) = s(0).

 fact(0) = 0.

FLIP input Overly general program

 Examples

 fact(0) = s(0).

 Background theory

 fact(s(X)) = mult(s(X),fact(X))
 mult(X,0) = 0
 mult(s(X),Y) = sum(Y,mult(X,Y))
 sum(X,0) = X
 sum(X,s(Y)) = s(sum(X,Y))

 fact(0) = s(0)
 fact(s(X)) = mult(s(X),fact(X))
 mult(X,0) = 0
 mult(s(X),Y) = sum(Y,mult(X,Y))
 sum(X,0) = X
 sum(X,s(Y)) = s(sum(X,Y))

Corrected program Comments

 fact(0) = s(0)
 fact(s(X)) = mult(s(X),fact(X))
 mult(X,0) = 0
 mult(s(X),Y) = sum(Y,mult(X,Y))
 sum(X,0) = X
 sum(X,s(Y)) = s(sum(X,Y))

 k=3; 
 C=[0,s(0)] 

 The overly general program is already correct.
 No top-down correction is necessary.
Wrong program Specification

 playdice(X) = double(winningface(X))
 double(0) = 0
 double(s(X)) = double(X)
 winningface(s(X)) = s(winningface(X))
 winningface(0) = 0

 playdice(X) = double(winningface(X))
 winningface(s(0)) = s(0)
 winningface(s(s(0))) = s(s(0))
 double(X) = sum(X,X)
 sum(X,0) = X
 sum(X,s(Y)) = s(sum(X,Y))

Positive example set Negative example set

 playdice(s(s(0))) = s(s(s(s(0)))).
 playdice(s(0)) = s(s(0)).
 double(s(s(s(s(0))))) = s(s(s(s(s(s(s(s(0)))))))).
 double(s(s(s(0)))) = s(s(s(s(s(s(0)))))).
 double(s(s(0))) = s(s(s(s(0)))).
 double(s(0)) = s(s(0)).
 double(0) = 0.
 winningface(s(s(0))) = s(s(0)).
 winningface(s(0)) = s(0).

 winningface(0) = 0.
 winningface(s(s(s(0)))) = s(s(s(0))).
 winningface(s(s(s(s(0))))) = s(s(s(s(0)))).
 playdice(0) = 0.
 playdice(s(0)) = 0.
 playdice(s(s(0))) = 0.
 playdice(s(s(s(0)))) = 0.
 playdice(s(s(s(s(0))))) = 0.
 double(s(0)) = 0.
 double(s(s(0))) = 0.
 double(s(s(s(0)))) = 0.
 double(s(s(s(s(0))))) = 0.

FLIP input Overly general program

 Examples

 double(s(s(s(s(0))))) = s(s(s(s(s(s(s(s(0)))))))).
 double(s(s(s(0)))) = s(s(s(s(s(s(0)))))).
 double(s(s(0))) = s(s(s(s(0)))).
 double(s(0)) = s(s(0)).
 double(0) = 0.


 Background theory

 double(0) = 0

 playdice(X) = double(winningface(X))
 double(0) = 0
 double(s(X)) = s(s(double(X)))
  winningface(s(X)) = s(winningface(X))
 winningface(0) = 0

Corrected program Comments

 playdice(X) = double(winningface(X))
 double(0) = 0
 double(s(X)) = s(s(double(X)))
 winningface(s(0)) = s(0)
 winningface(s(s(0))) = s(s(0))

 k=2; 
 C=[0,s(0),s(s(0)),s(s(s(0)))] 

 View the outcome 

Download

Buggy 2.0

Related papers

  1. M. Alpuente, D. Ballis, F. Correa, M. Falaschi. An Integrated Framework for the Diagnosis and Correction of Rule-Based Programs (2009) [pdf].

CSS style Copyright©2009 Michele Baggi
Last modified: September, 2009