liu.seSearch for publications in DiVA
Change search
ReferencesLink to record
Permanent link

Direct link
Using Assertions in Declarative and Operational Models for Automated Debugging
Linköping University, Department of Computer and Information Science, PELAB - Programming Environment Laboratory. Linköping University, The Institute of Technology.ORCID iD: 0000-0002-3435-4996
New Mexico State University, Las Cruces, New Mexico, USA.
Linköping University, Department of Computer and Information Science. Linköping University, The Institute of Technology.
1992 (English)Conference paper (Refereed)
Abstract [en]

 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
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
URN: urn:nbn:se:liu:diva-110089OAI: diva2:742714
Tolouse’92 - The fifth International Conference in Software Engineering and its Applications, Tolouse, December 7-11, 1992
Available from: 2014-09-02 Created: 2014-09-02 Last updated: 2014-10-03

Open Access in DiVA

No full text

Search in DiVA

By author/editor
Fritzson, PeterShahmehri, Nahid
By organisation
PELAB - Programming Environment LaboratoryThe Institute of TechnologyDepartment of Computer and Information Science
Electrical Engineering, Electronic Engineering, Information Engineering

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 40 hits
ReferencesLink to record
Permanent link

Direct link