Program Repair Using The Order Relation Of Fault Localization

Software debugging is the process of fixing program bugs, is an important step ofsoftware development. This process is a difficult task. Locating an error from sourcecode is a challenging work without any automated assistance. When an error islocated, it may still take considerable time for a developer to make an appropriate fix.In recent years, the development of a variety of approaches to automate programdebugging can be seen. Most of these focus on fault localization, narrowing the searchscope for bugs to help developers identify faulty statements more quickly. However,many program repairs are made manually.This dissertation presents an approach for program repair based on the orderrelation of fault localization. Its key insight is to transform the faulty program toseveral nondeterministic programs, using the list of faulty statements with their orderrelation. That is, a faulty statement that has deterministic behavior is replaced withone that has nondeterministic behavior. These nondeterministic programs can betransformed to a few of Boolean satisfiability (SAT) problems. Repair model can befound by using the specification to prune the nondeterminism. This dissertation givesa weight to every clause of every SAT problem, according to the order relation of faultlocalization. Also, the mapping between the number of the statement that may befaulty and the boolean variables in every SAT problem is built. Thus, it reduces theseproblems to a Weighted Maximum Satisfiability (Weighted MAX-SAT) problem. Sothe process of finding a model that satisfies the specification constraints is ordered.The main work of this dissertation include: encode Java code and itsspecifications as a relational programming language (FIR: Forge Intermediate Representation), transform a deterministic FIR to a nondeterministic FIR, transform anondeterministic FIR to relational logic formulas, transform relational logic formulasto a SAT problem. Thus the mapping between the number of the statement and theboolean variables in every SAT problem is built. Several SAT problems are reduced toone Weighted MAX-SAT problem by using the mapping and the order relation ofstatements that may be faulty. Finally, a Weighted MAX-SAT solver is used to solvethe Weighted MAX-SAT problem then the repair model for the faulty program can befound.One of the shortcomings of the technique is that the accuracy of the repairedstatements is very closely tied to the correctness and completeness of the specificationconstraints and the maximum value of scope used in the validation phase. So itremains to be explored that how to bridge the gap between specification-based andtestcase-based repair. Initial experiments show the effectiveness of this approach inproducing repair model of Java programs that have clear specifications and thatmanipulate data structures.