Skip to main content
SpringerLink
Log in

Inferring argument size relationships with CLP(\(\mathcal{R}\))

  • Conference paper
  • First Online:
Logic Program Synthesis and Transformation (LOPSTR 1996)

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

Abstract

Argument size relationships are useful in termination analysis which, in turn, is important in program synthesis and goal-replacement transformations. We show how a precise analysis for inter-argument size relationships, formulated in terms of abstract interpretation, can be implemented straightforwardly in a language with constraint support like CLP(\(\mathcal{R}\)) or SICStus version 3. The analysis is based on polyhedral approximations and uses a simple relaxation technique to calculate least upper bounds and a delay method to improve the precision of widening. To the best of our knowledge, and despite its simplicity, the analysis derives relationships to an accuracy that is either comparable or better than any existing technique.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. Bagnara. On the detection of implicit and redundant numeric constraints in CLP programs. In GULP-PRODE'94, pages 312–326, 1994.

    Google Scholar 

  2. R. Bagnara. A hierarchy of constraint systems for data-flow analysis of constraint logic-based languages. Technical Report TR-96-10, Dipartimento di Informaticá, Universita di Pisa corso Italia 40, 56125 Pisa, Italy, 1996.

    Google Scholar 

  3. R. Bagnara, R. Giacobazzi, and G. Levi. Static Analysis of clp Programs over Numeric Domains. In WSA'92, 1992.

    Google Scholar 

  4. V. Balasundaram and K. Kennedy. A Technique for Summarizing Data Access and Its Use in Parallelism Enhancing Transformations. In PLDI'89, pages 41–53. ACM Press, 1989.

    Google Scholar 

  5. A. Bossi, M. Gabbrielli, G. Levi, and M. Martelli. The s-semantics approach: theory and applications. Journal of Logic Programming, 1991.

    Google Scholar 

  6. M. Codish and V. Lagoon. Persistant Type Analysis using a Non-Ground Domain. Technical report, Dept of Maths and Computer Science, Ben-Gurion University of the Negev, Israel, 1995.

    Google Scholar 

  7. A. Colmerauer. An Introduction to Prolog III. In CACM, volume 33, pages 70–90, July 1990.

    Google Scholar 

  8. P. Cousot and R. Cousot. Comparing the Galois Connection and Widening/Narrowing Approaches to Abstract Interpretation. Technical Report LIENS-92-16, Laboratoire d'Informatique de l'Ecole Normale Superiéure, 45 Rue d'Ulm, 7523 Paris Cédex 05, France, 1992.

    Google Scholar 

  9. P. Cousot and N. Halbwachs. Automatic Discovery of Linear Restraints among Variables of a Program. In POPL'78, pages 84–97, 1978.

    Google Scholar 

  10. B. De Backer and H. Beringer. A CLP language handling disjunctions of linear constraints. In ICLP'93, pages 550–563. MIT Press, 1993.

    Google Scholar 

  11. S. Debray and N. Lin. Cost Analysis for Logic Programs. ACM Transactions on Programming Languages and Systems, July 1992.

    Google Scholar 

  12. S. Decorte, D. De Schreye, and M. Fabris. Automatic Inference of Norms: a Missing Link in Automatic Termination Analysis. In ICLP'93, pages 420–436, 1993.

    Google Scholar 

  13. J. Gallagher, D. Boulanger, and Y. Saglam. Practical Model-Based Static Analysis for Definite Logic Programs. Technical Report CSTR-95-011, Department of Computer Science, University of Bristol, June 1995.

    Google Scholar 

  14. R. Giacobazzi, S. Debray, and G. Levi. Generalised Semantics and Abstract Interpretation for Constraint Logic Programs. Technical report, Dipartimento di Informatica, Universitá di Pisa, 1992.

    Google Scholar 

  15. N. Halbwachs. Détermination automatique de relations linéaires vérifiées par les variables d'un programme. Universit'e scientifique et médicale de Grenoble, 1979. Thèse de 3 ème d'informatique.

    Google Scholar 

  16. N. Halbwachs, Y.E. Proy, and P. Raymond. Verification of linear hybrid systems by means of convex approximations. In First International Static Analysis Symposium. Springer Verlag, September 1994.

    Google Scholar 

  17. N. C. Heintze, J. Jafar, S. Michaylov, P. J. Stuckey, and R. H. C. Yap. The CLP(\(\mathcal{R}\)) Programmer's Manual Version 1.2, 1992.

    Google Scholar 

  18. R. N. Horspool. Analyzing List Usage in Prolog Code. University of Victoria, March 1990.

    Google Scholar 

  19. G. Janssens, M. Bruynooghe, and V. Englebert. Abstracting numeric values in CLP(H,N). In PLILP'94, pages 400–414. Springer-Verlag, 1994.

    Google Scholar 

  20. M. Karr. Affine Relationships Among Variables of a Program. Acta Informatica, 6:133–151, 1976.

    Article  Google Scholar 

  21. D. B. Kemp and P. J. Stuckey. Analysis Based Constraint Query Optimisation. In ICLP'93, pages 666–682, 1993.

    Google Scholar 

  22. A. Kerbrat. Personal Communication on Polyhedral library polyhedra.tar. October, 1993.

    Google Scholar 

  23. J. Martin, A. King, and P. Soper. Typed Norms for Typed Logic Programs. In LOPSTR'96. Springer-Verlag, 1996.

    Google Scholar 

  24. F. Mesnard and J.-G. Ganascia. CLP(\(\mathcal{Q}\)) for Proving Interargument Relations. In META'92, pages 308–320, Uppsala, Sweden, 1992. Springer-Verlag.

    Google Scholar 

  25. H. Millroth. Reforming Compilation of Logic Programs. PhD thesis, Computing Science Department, Uppsala University, 1990.

    Google Scholar 

  26. H. Millroth. Personal Communication on the rôle of Argument Relationships in Reform. October, 1993.

    Google Scholar 

  27. L. Plümer. Termination Proofs for Logic Programs. Springer-Verlag, 1990.

    Google Scholar 

  28. K. Sohn. Constraints among Argument Sizes in Logic Programs. In PODS'94, pages 68–74. ACM Press, 1994.

    Google Scholar 

  29. J. D. Ullman. Implementation of Logical Query Languages for Databases. ACM Transactions on Database Systems, 10(3):289–321, 1985.

    Google Scholar 

  30. A. Van Gelder. Deriving constraints among argument sizes in logic programs. Annals of Mathematics and Artifical Intelligence, (3), 1991.

    Google Scholar 

  31. K. Verschaetse and D. De Schreye. Derivation of Linear Size Relations by Abstract Interpretation. In PLILP'92, pages 296–310. Springer-Verlag, 1992.

    Google Scholar 

  32. D. Wilde. A Library for doing Polyhedral Operations. Technical Report PI-785, Institut de Recherche en Informatique et Systemes Aleatoires, Campus Universitaire de Beauilieu, 35042 Rennes Cedex, France, 1993.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computing Laboratory, University of Kent at Canterbury, CT2 7NF, UK

    Florence Benoy & Andy King

Authors
  1. Florence Benoy
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andy King
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

John Gallagher

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Benoy, F., King, A. (1997). Inferring argument size relationships with CLP(\(\mathcal{R}\)). In: Gallagher, J. (eds) Logic Program Synthesis and Transformation. LOPSTR 1996. Lecture Notes in Computer Science, vol 1207. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-62718-9_12

Download citation

  • DOI: https://doi.org/10.1007/3-540-62718-9_12

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-62718-0

  • Online ISBN: 978-3-540-68494-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation