@techreport{R-93-12,
TITLE = {Using Assertion in Declarative Models for Automated Debugging},
AUTHOR = {Peter Fritzson and Mikhail Auguston and Nahid Shahmehri},
YEAR = {1993},
NUMBER = {R-93-12},
INSTITUTION = ida,
ADDRESS = idaaddr,
ABSTRACTURL = {/publications/cgi-bin/tr-fetch.pl?r-93-12+abstr},
ABSTRACT = {Our previously developed GADT method was the first declarative algorithmic debugging technique for procedural imperative languages with side-effects. GADT is generally applicable to procedural languages, and is not dependent on any ad hoc assumptions regarding the subject program. The original form of algorithmic debugging, introduced by Shapiro [Shapiro-82], is however limited to small Prolog programs without side-effects. Another drawback of the original method is the large number of interactions with the user during bug localization.To our knowledge, the extended GADT presented here is the first method which uses powerful operational assertions in 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. Previously, we have enhanced the bug localization properties of GADT, using lookup in a category partition testing database. In addition, we use program slicing, a data flow analysis technique, to dynamically compute which parts of the program are relevant for the search.A prototype of the GADT has been implemented in Pascal, supporting debugging in a subset of Pascal. An interpreter of FORMAN assertions has also been implemented in Pascal. During bug localization, both types of assertions are evaluated on execution traces.},
IDANR = {LiTH-IDA-R-93-12}