On the use of Specification Knowledge in Program Debugging
Mihai Nica, Jörg Weber, Franz Wotawa · 2009
Abstract: In this paper we present an approach that relies on the representation of the debugging problem as a constraint satisfaction problem. We show how arbitrary sequential programs together with specification knowledge like invariants can be represented as a set of constraints. We provide a formalization of the constraint representation and of the diagnosis problem which clarifies and improves previously published ideas. We also correct a flaw in a previously published paper which could lead to undesired diagnostic results. Moreover, based on the constraint representation we explain how to use a fast constraint solver, which is freely available, for computing diagnoses. Using such a constraint solver we obtain first experimental results for a set of Java programs. The results indicate that the use of specification knowledge reduces the number of diagnoses substantially. This shows that the integration of specifications like pre- and postconditions or invariants, which can be provided as annotations in the program, can significantly help to make model-based debugging applicable in practice. 1.