Using Assertions in Declarative and Operational Models for Automated Debugging
1992 (English)Conference paper (Refereed)
This article presents an improved method for semiautomatic bug localization, by extending our previous generalized algorithm debugging technique, (GADT) [Fritzson et al. 1991], which uses declarative assertions about program units such as procedures and operational assertions about program behavior. For example, functional properties are best expressed through declarative assertions about procedure units, whereas order-dependent properties, or sequencing constraints in general, are more easily expressed using operational semantics. A powerful assertion language, called FORMAN, has been developed to this end. Such assertions can be collected into assertion libraries, which can greatly increase the degree of automation in bug localization. The long-range goal of this work is a semiautomatic debugging and testing system, which can be used during large-scale program development of nontrivial programs. To our knowledge, the extended GADT (EGADT) presented here is the first method that uses powerful operational assertions integrated with algorithmic debugging. In addition to providing support for local-level bug localization within procedures (which is not handled well by basic algorithmic debugging), the operational assertions reduce the number of irrelevant questions to the programmer during bug localization, thus further improving bug localization. A prototype of the GADT, implemented in PASCAL, supports debugging in a subset of Pascal. An interpreter of FORMAN assertions has also been implemented in PASCAL. During bug localization, both declarative and operational assertions are evaluated on execution traces.
Place, publisher, year, edition, pages
Electrical Engineering, Electronic Engineering, Information Engineering
IdentifiersURN: urn:nbn:se:liu:diva-110089OAI: oai:DiVA.org:liu-110089DiVA: diva2:742714
Tolouse’92 - The fifth International Conference in Software Engineering and its Applications, Tolouse, December 7-11, 1992