In this paper, I introduce a language for modeling software called ZD, and show how it has been used for automatic program debugging. In particular, ZD allows a program to be represented simultaneously at several levels of abstraction, and keeps track of the relationships between explanations of program correctness at all these levels.

I also describe a program called Dudu, which takes ZD descriptions of a program, along with a purportedly correct program, and determines the most appropriate description of any bugs in the program. These explanations can be generated at any level of abstraction, as appropriate.

In order to be able to navigate in such a model, it is necessary that the model be quite specific about the meaning of all of its constructs. The main contribution of this paper is to outline these requirements, and the constructs in ZD that support them. The debugging capabilities are shown to demonstrate the sufficiency of these constraints.

AADEBUG'95 Program

AADEBUG'95 home page