Debugging, which involves both fault localization and bug repair, is critical for developers to identify and remove bugs in a program. Most existing debugging research techniques focus on imperative programs (e.g., C and Java) and rely on test suite to analyze correct and incorrect executions of the program to identify and repair suspicious statements.We propose a new debugging framework for models written in a declarative language, where the models are not "executed", but rather converted into a logical formula solvable using a constraint solver. In recent work, we developed a fault localization tool that takes as input an Alloy model consisting of a violated assertion and returns a ranked list of suspicious expressions contributing to the violation. Preliminary results show that the fault localization tool is accurate, useful, and scales to complex, real-world Alloy models.In this work, we propose a new repair technique and tool that can be integrated with our fault localization tool or used as a stand-alone tool. We aim to automatic repair bugs violating given assertions in Alloy models. We plan to adopt guided search and pattern-based repair techniques from imperative automatic program repair and modify DFA learning algorithms to synthesis repairs.
展开▼
