Abstract
Abstract interpretation is a formal method that enables the static determination (i.e. at compile-time) of the dynamic properties (i.e. at run-time) of programs. So far, this method has mainly been used to build sophisticated, optimizing compilers. In this paper, we show how abstract interpretation techniques can be used to perform, prior to their execution, a static and automatic debugging of imperative programs. This novel approach, which we call abstract debugging, lets programmers use assertions to express invariance properties as well as inevitable properties of programs, such as termination. We show how such assertions can be used to find the origin of bugs, rather than their occurrences, and determine necessary conditions of program correctness, that is, necessary conditions for programs to be bug-free and correct with respect to the programmer's assertions. We also show that assertions can be used to restrict the control-flow of a program and examine its behavior along specific execution paths and find necessary conditions for the program to reach a particular point in a given state. Finally, we present the Syntox system that enables the abstract debugging of Pascal programs by the determination of the range of scalar variables, and discuss implementation, algorithmic and complexity issues.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Alfred V. Aho, Ravi Sethi and Jeffrey D. Ullman: “Compilers — Principles, Techniques and Tools”, Addison-Wesley Publishing Company (1986)
François Bourdoncle: “Interprocedural Abstract Interpretation of Block Structured Languages with Nested Procedures, Aliasing and Recursivity”, Proc. of the International Workshop PULP'90, Lecture Notes in Computer Science 456, Springer-Verlag (1990)
François Bourdoncle: “Abstract Interpretation By Dynamic Partitioning”, Journal of Functional Programming, Vol. 2, No. 4 (1992)
François Bourdoncle: “Sémantiques des langages impératifs d'ordre supérieur et interprétation abstraite”, Ph. D. dissertation, Ecole Polytechnique (1992)
François Bourdoncle: “Efficient Chaotic Iteration Strategies with Widenings”, Proc. of the International Conf. on Formal Methods in Programming and their Applications, Lecture Notes in Computer Science, Springer-Verlag (1993) to appear
François Bourdoncle: “Abstract Debugging of Higher-Order Imperative Languages”, Proc. of SIGPLAN '93 Conference on Programming Language Design and Implementation (1993)
Patrick and Radhia Cousot: “Abstract Interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints”, Proc. of the 4th ACM Symp. on POPL (1977) 238–252
Patrick Cousot: “Asynchronous iterative methods for solving a fixpoint system of monotone equations”, Research Report IMAG-RR-88, Université Scientifique et Médicale de Grenoble (1977)
Patrick Cousot and Nicolas Halbwachs: “Automatic discovery of linear constraints among variables of a program”, Proc. of the 5th ACM Symp. on POPL (1978) 84–97
Patrick Cousot: “Méthodes itératives de construction et d'approximation de points fixes d'opérateurs monotones sur un treillis. Analyse sémantique de programmes”, Ph. D. dissertation, Université Scientifique et Médicale de Grenoble (1978)
Patrick and Radhia Cousot: “Static determination of dynamic properties of recursive procedures”, Formal Description of Programming Concepts, North Holland Publishing Company (1978) 237–277
Patrick Cousot: “Semantic foundations of program analysis”, in Muchnick and Jones-Eds., Program Flow Analysis, Theory and Applications, Prentice-Hall (1981) 303–343
Alain Deutsch: “On determining lifetime and aliasing of dynamically allocated data in higher-order functional specifications”, Proc. of the 17th ACM Symp. on POPL (1990)
Alain Deutsch: “A Storeless Model of Aliasing and its Abstractions using Finite Representations of Right-Regular Equivalence Relations”, Proc. of the IEEE'92 International Conference on Computer Languages, IEEE Press (1992)
Philippe Granger: “Static analysis of arithmetical congruences”, International Journal of Computer Mathematics (1989) 165–190
Rajiv Gupta: “A Fresh Look at Optimizing Array Bound Checking”, Proc. of SIG-PLAN '90 Conf. on Programming Language Design and Implementation (1990) 272–282
Victoria Markstein, John Cocke and Peter Markstein: “Optimization of Range Checking”, Proc. of the SIGPLAN'82 Symp. on Compiler Construction (1982) 114–119
ISO/IEC 7185: “Information technology — Programming languages — Pascal”, Revised 1983, Second edition (1990)
Micha Sharir and Amir Pnueli: “Two Approaches to Interprocedural Data Flow Analysis” in Muchnick and Jones Eds., Program Flow Analysis, Theory and Applications, Prentice-Hall (1981) 189–233
R.E. Tarjan: “Depth-first search and linear graph algorithms”, SIAM J. Comput., 1 (1972) 146–160
Andrew P. Tolmach and Andrew W. Appel: “Debugging Standard ML Without Reverse Engineering”, Proc. 1990 ACM Conf. on Lisp and Functional Programming, ACM Press (1990) 1–12
Niklaus Wirth and Kathleen Jensen: “Pascal user manual and report” (Second Ed.), Springer-Verlag (1978)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bourdoncle, F. (1993). Assertion-based debugging of imperative programs by abstract interpretation. In: Sommerville, I., Paul, M. (eds) Software Engineering — ESEC '93. ESEC 1993. Lecture Notes in Computer Science, vol 717. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57209-0_33
Download citation
DOI: https://doi.org/10.1007/3-540-57209-0_33
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57209-1
Online ISBN: 978-3-540-47972-7
eBook Packages: Springer Book Archive