A Formalization of Program Debugging in the Situation Calculus

Abstract

Program debugging is one of the most time-consuming parts of the software development cycle. In recent years, automatic debugging has been an active research area in software engi-neering; it has also attracted attention from the AI commu-nity. However, existing approaches are mostly experiential; moreover, those model-based approaches are based on ab-stract models of programs, which lends an experiential fla-vor to the approaches, due to the heuristic nature of choosing an abstract model. We believe that it is necessary to estab-lish a precise theoretical foundation for debugging from first principles. In this paper, we present a first step towards this foundation: using Reiter’s theoretical framework of model-based diagnosis, we give a clean formalization of the program debugging task in the situation calculus, a logical language suitable for describing dynamic worlds. Examples are given to illustrate our formalization.