Skip to main content
SpringerLink
Log in

Program Development Using Abstract Interpretation (And the Ciao System Preprocessor)

  • Conference paper
  • First Online:
Static Analysis (SAS 2003)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2694))

Included in the following conference series:

Abstract

The technique of Abstract Interpretation has allowed the development of very sophisticated global program analyses which are at the same time provably correct and practical. We present in a tutorial fashion a novel program development framework which uses abstract interpretation as a fundamental tool. The framework uses modular, incremental abstract interpretation to obtain information about the program. This information is used to validate programs, to detect bugs with respect to partial specifications written using assertions (in the program itself and/or in system libraries), to generate and simplify run-time tests, and to perform high-level program transformations such as multiple abstract specialization, parallelization, and resource usage control, all in a provably correct way. In the case of validation and debugging, the assertions can refer to a variety of program points such as procedure entry, procedure exit, points within procedures, or global computations. The system can reason with much richer information than, for example, traditional types. This includes data structure shape (including pointer sharing), bounds on data structure sizes, and other operational variable instantiation properties, as well as procedure-level properties such as determinacy, termination, non-failure, and bounds on resource consumption (time or space cost). CiaoPP, the preprocessor of the Ciao multi-paradigm programming system, which implements the described functionality, will be used to illustrate the fundamental ideas.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. F. Bourdoncle. Abstract debugging of higher-order imperative languages. In Programming Languages Design and Implementation’93, pages 46–55, 1993.

    Google Scholar 

  2. F. Bueno, D. Cabeza, M. Carro, M. Hermenegildo, P. López-García, and G. Puebla. The Ciao Prolog System. Reference Manual. The Ciao System Documentation Series-TR CLIP3/97.1, School of Computer Science, Technical University of Madrid (UPM), August 1997. System and on-line version of the manual available at http://clip.dia.fi.upm.es/Software/Ciao/.

    Google Scholar 

  3. F. Bueno, D. Cabeza, M. Hermenegildo, and G. Puebla. Global Analysis of Standard Prolog Programs. In European Symposium on Programming, number 1058 in LNCS, pages 108–124, Sweden, April 1996. Springer-Verlag.

    Google Scholar 

  4. F. Bueno, M. García de la Banda, and M. Hermenegildo. Effectiveness of Abstract Interpretation in Automatic Parallelization: A Case Study in Logic Programming. ACM Transactions on Programming Languages and Systems, 21(2):189–238, March 1999.

    Article  Google Scholar 

  5. F. Bueno, P. Deransart, W. Drabent, G. Ferrand, M. Hermenegildo, J. Maluszynski, and G. Puebla. On the Role of Semantic Approximations in Validation and Diagnosis of Constraint Logic Programs. In Proc. of the 3rd. Int’l Workshop on Automated Debugging-AADEBUG’97, pages 155–170, Linköping, Sweden, May 1997. U. of Linköping Press.

    Google Scholar 

  6. F. Bueno, M. García de la Banda, M. Hermenegildo, K. Marriott, G. Puebla, and P. Stuckey. A Model for Inter-module Analysis and Optimizing Compilation. In Logic-based Program Synthesis and Transformation, number 2042 in LNCS, pages 86–102. Springer-Verlag, 2001.

    Chapter  Google Scholar 

  7. D. Cabeza and M. Hermenegildo. Extracting Non-strict Independent Andparallelism Using Sharing and Freeness Information. In 1994 International Static. Analysis Symposium, number 864 in LNCS, pages 297–313, Namur, Belgium, September 1994. Springer-Verlag.

    Google Scholar 

  8. B. Le Charlier and P. Van Hentenryck. Experimental Evaluation of a Generic Abstract Interpretation Algorithm for Prolog. ACM Transactions on Programming Languages and Systems, 16(1):35–101, 1994.

    Article  Google Scholar 

  9. M. Comini, G. Levi, M. C. Meo, and G. Vitiello. Abstract diagnosis. Journal of Logic Programming, 39(1–3):43–93, 1999.

    Article  MATH  MathSciNet  Google Scholar 

  10. M. Comini, G. Levi, and G. Vitiello. Declarative diagnosis revisited. In 1995 International Logic Programming Symposium, pages 275–287, Portland, Oregon, December 1995. MIT Press, Cambridge, MA.

    Google Scholar 

  11. P. Cousot. Automatic Verification by Abstract Interpretation, Invited Tutorial. In Fourth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI), number 2575 in LNCS, pages 20–24. Springer, January 2003.

    Chapter  Google Scholar 

  12. P. Cousot and R. Cousot. Abstract Interpretation: a Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Fourth ACM Symposium on Principles of Programming Languages, pages 238–252, 1977.

    Google Scholar 

  13. P. Cousot and R. Cousot. Systematic Design of Program Transformation Frameworks by Abstract Interpretation. In POPL’02: 29ST ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 178–190, Portland, Oregon, January 2002. ACM.

    Google Scholar 

  14. P.W. Dart and J. Zobel. A Regular Type Language for Logic Programs. In F. Pfenning, editor, Types in Logic Programming, pages 157–187. MIT Press, 1992.

    Google Scholar 

  15. M. García de la Banda, M. Hermenegildo, M. Bruynooghe, V. Dumortier, G. Janssens, and W. Simoens. Global Analysis of Constraint Logic Programs. ACM Trans. on Programming Languages and Systems, 18(5):564–615, 1996.

    Article  Google Scholar 

  16. M. García de la Banda, M. Hermenegildo, and K. Marriott. Independence in CLP Languages. ACM Transactions on Programming Languages and Systems, 22(2):269–339, March 2000.

    Article  Google Scholar 

  17. S.K. Debray, P. López-García, and M. Hermenegildo. Non-Failure Analysis for Logic Programs. In 1997 International Conference on Logic Programming, pages 48–62, Cambridge, MA, June 1997. MIT Press, Cambridge, MA.

    Google Scholar 

  18. S.K. Debray, P. López-García, M. Hermenegildo, and N.-W. Lin. Estimating the Computational Cost of Logic Programs. In Static Analysis Symposium, SAS’94, number 864 in LNCS, pages 255–265, Namur, Belgium, September 1994. Springer-Verlag.

    Google Scholar 

  19. S.K. Debray, P. López-García, M. Hermenegildo, and N.-W. Lin. Lower Bound Cost Estimation for Logic Programs. In 1997 International Logic Programming Symposium, pages 291–305. MIT Press, Cambridge, MA, October 1997.

    Google Scholar 

  20. J. Gallagher and G. Puebla. Abstract Interpretation over Non-Deterministic Finite Tree Automata for Set-Based Analysis of Logic Programs. In Fourth International Symposium on Practical Aspects of Declarative Languages, number 2257 in LNCS, pages 243–261. Springer-Verlag, January 2002.

    Chapter  Google Scholar 

  21. J.P. Gallagher and D.A. de Waal. Fast and precise regular approximations of logic programs. In Pascal Van Hentenryck, editor, Proc. of the 11th International Conference on Logic Programming, pages 599–613. MIT Press, 1994.

    Google Scholar 

  22. M. García de la Banda, M. Hermenegildo, M. Bruynooghe, V. Dumortier, G. Janssens, and W. Simoens. Global Analysis of Constraint Logic Programs. ACM Transactions on Programming Languages and Systems, 18(5):564–615, September 1996.

    Article  Google Scholar 

  23. F. Giannotti and M. Hermenegildo. A Technique for Recursive Invariance Detection and Selective Program Specialization. In Proc. 3rd. Int’l Symposium on. Programming Language Implementation and Logic Programming, number 528 in LNCS, pages 323–335. Springer-Verlag, August 1991.

    Google Scholar 

  24. M. Hermenegildo. A Documentation Generator for (C)LP Systems. In International Conference on Computational Logic, CL2000, number 1861 in LNAI, pages 1345–1361. Springer-Verlag, July 2000.

    Google Scholar 

  25. M. Hermenegildo, F. Bueno, D. Cabeza, M. Carro, M. García de la Banda, P. López-García, and G. Puebla. The CIAO Multi-Dialect Compiler and System: An Experimentation Workbench for Future (C)LP Systems. In Parallelism and Implementation of Logic and Constraint Logic Programming, pages 65–85. Nova Science, Commack, NY, USA, April 1999.

    Google Scholar 

  26. M. Hermenegildo, F. Bueno, G. Puebla, and P. López-García. Program Analysis, Debugging and Optimization Using the Ciao System Preprocessor. In 1999 International Conference on Logic Programming, pages 52–66, Cambridge, MA, November 1999. MIT Press.

    Google Scholar 

  27. M. Hermenegildo, G. Puebla, and F. Bueno. Using Global Analysis, Partial Specifications, and an Extensible Assertion Language for Program Validation and Debugging. In K. R. Apt, V. Marek, M. Truszczynski, and D. S. Warren, editors, The Logic Programming Paradigm: a 25-Year Perspective, pages 161–192. Springer-Verlag, July 1999.

    Google Scholar 

  28. M. Hermenegildo, G. Puebla, K. Marriott, and P. Stuckey. Incremental Analysis of Constraint Logic Programs. ACM Transactions on Programming Languages and Systems, 22(2):187–223, March 2000.

    Article  Google Scholar 

  29. M. Hermenegildo and F. Rossi. Strict and Non-Strict Independent And-Parallelism in Logic Programs: Correctness, Efficiency, and Compile-Time Conditions. Journal of Logic Programming, 22(1):1–45, 1995.

    Article  MATH  MathSciNet  Google Scholar 

  30. M. Leuschel. Program Specialisation and Abstract Interpretation Reconciled. In Joint International Conference and Symposium on Logic Programming, June 1998.

    Google Scholar 

  31. Y. Lichtenstein and E. Y. Shapiro. Abstract algorithmic debugging. In R. A. Kowalski and K. A. Bowen, editors, Fifth International Conference and Symposium on Logic Programming, pages 512–531, Seattle, Washington, August 1988. MIT.

    Google Scholar 

  32. P. López-García and M. Hermenegildo. Efficient Term Size Computation for Granularity Control. In International Conference on Logic Programming, pages 647–661, Cambridge, MA, June 1995. MIT Press, Cambridge, MA.

    Google Scholar 

  33. P. López-García, M. Hermenegildo, and S.K. Debray. A Methodology for Granularity Based Control of Parallelism in Logic Programs. J. of Symbolic Computation, Special Issue on Parallel Symbolic Computation, 22:715–734, 1996.

    Google Scholar 

  34. K. Marriott, M. García de la Banda, and M. Hermenegildo. Analyzing Logic Programs with Dynamic Scheduling. In 20th. Annual ACM Conf. on Principles of Programming Languages, pages 240–254. ACM, January 1994.

    Google Scholar 

  35. K. Muthukumar, F. Bueno, M. García de la Banda, and M. Hermenegildo. Automatic Compile-time Parallelization of Logic Programs for Restricted, Goallevel, Independent And-parallelism. Journal of Logic Programming, 38(2):165–218, February 1999.

    Article  MATH  MathSciNet  Google Scholar 

  36. K. Muthukumar and M. Hermenegildo. Combined Determination of Sharing and Freeness of Program Variables Through Abstract Interpretation. In 1991 International Conference on Logic Programming, pages 49–63. MIT Press, June 1991.

    Google Scholar 

  37. K. Muthukumar and M. Hermenegildo. Compile-time Derivation of Variable Dependency Using Abstract Interpretation. Journal of Logic Programming, 13(2/3):315–347, July 1992.

    Article  MATH  Google Scholar 

  38. G. Puebla, F. Bueno, and M. Hermenegildo. A Generic Preprocessor for Program Validation and Debugging. In P. Deransart, M. Hermenegildo, and J. Maluszynski, editors, Analysis and Visualization Tools for Constraint Programming, number 1870 in LNCS, pages 63–107. Springer-Verlag, September 2000.

    Chapter  Google Scholar 

  39. G. Puebla, F. Bueno, and M. Hermenegildo. An Assertion Language for Constraint Logic Programs. In P. Deransart, M. Hermenegildo, and J. Maluszynski, editors, Analysis and Visualization Tools for Constraint Programming, number 1870 in LNCS, pages 23–61. Springer-Verlag, September 2000.

    Chapter  Google Scholar 

  40. G. Puebla, F. Bueno, and M. Hermenegildo. Combined Static and Dynamic Assertion-Based Debugging of Constraint Logic Programs. In Logic-based Program Synthesis and Transformation (LOPSTR’99), number 1817 in LNCS, pages 273–292. Springer-Verlag, 2000.

    Chapter  Google Scholar 

  41. G. Puebla, M. García de la Banda, K. Marriott, and P. Stuckey. Optimization of Logic Programs with Dynamic Scheduling. In 1997 International Conference on Logic Programming, pages 93–107, Cambridge, MA, June 1997. MIT Press.

    Google Scholar 

  42. G. Puebla and M. Hermenegildo. Optimized Algorithms for the Incremental Analysis of Logic Programs. In International Static Analysis Symposium, number 1145 in LNCS, pages 270–284. Springer-Verlag, September 1996.

    Google Scholar 

  43. G. Puebla and M. Hermenegildo. Abstract Specialization and its Application to Program Parallelization. In J. Gallagher, editor, Logic Program Synthesis and Transformation, number 1207 in LNCS, pages 169–186. Springer-Verlag, 1997.

    Google Scholar 

  44. G. Puebla and M. Hermenegildo. Abstract Multiple Specialization and its Application to Program Parallelization. J. of Logic Programming. Special Issue on Synthesis, Transformation and Analysis of Logic Programs, 41(2&3):279–316, November 1999.

    MATH  MathSciNet  Google Scholar 

  45. G. Puebla and M. Hermenegildo. Some Issues in Analysis and Specialization of Modular Ciao-Prolog Programs. In Special Issue on Optimization and Implementation of Declarative Programming Languages, volume 30 of Electronic Notes in Theoretical Computer Science. Elsevier — North Holland, March 2000.

    Google Scholar 

  46. G. Puebla, M. Hermenegildo, and J. Gallagher. An Integration of Partial Evaluation in a Generic Abstract Interpretation Framework. In O Danvy, editor, ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM’99), number NS-99-1 in BRISC Series, pages 75–85. University of Aarhus, Denmark, January 1999.

    Google Scholar 

  47. C. Vaucheret and F. Bueno. More precise yet efficient type inference for logic programs. In International Static Analysis Symposium, number 2477 in LNCS, pages 102–116. Springer-Verlag, September 2002.

    Google Scholar 

  48. E. Yardeni and E. Shapiro. A Type System for Logic Programs. Concurrent Prolog: Collected Papers, pages 211–244, 1987.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Technical University of Madrid (UPM), Madrid

    Manuel V. Hermenegildo, Germán Puebla, Francisco Bueno & Pedro López-García

  2. Departments of Computer Science and Electrical and Computer Engineering, University of New Mexico, USA

    Manuel V. Hermenegildo

Authors
  1. Manuel V. Hermenegildo
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Germán Puebla
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Francisco Bueno
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Pedro López-García
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. École Polytechnique, STIX, 91128, Palaiseau cedex, France

    Radhia Cousot

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hermenegildo, M.V., Puebla, G., Bueno, F., López-García, P. (2003). Program Development Using Abstract Interpretation (And the Ciao System Preprocessor). In: Cousot, R. (eds) Static Analysis. SAS 2003. Lecture Notes in Computer Science, vol 2694. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44898-5_8

Download citation

  • DOI: https://doi.org/10.1007/3-540-44898-5_8

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-40325-8

  • Online ISBN: 978-3-540-44898-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation