Advertisement

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

  • Florence Benoy
  • Andy King
Conference paper
Part of the Lecture Notes in Computer Science book series (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.

Keywords

Convex Hull Logic Program List Length Abstract Interpretation Ground Representation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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. 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. 3.
    R. Bagnara, R. Giacobazzi, and G. Levi. Static Analysis of clp Programs over Numeric Domains. In WSA'92, 1992.Google Scholar
  4. 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. 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. 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. 7.
    A. Colmerauer. An Introduction to Prolog III. In CACM, volume 33, pages 70–90, July 1990.Google Scholar
  8. 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. 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. 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. 11.
    S. Debray and N. Lin. Cost Analysis for Logic Programs. ACM Transactions on Programming Languages and Systems, July 1992.Google Scholar
  12. 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. 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. 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. 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. 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. 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. 18.
    R. N. Horspool. Analyzing List Usage in Prolog Code. University of Victoria, March 1990.Google Scholar
  19. 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. 20.
    M. Karr. Affine Relationships Among Variables of a Program. Acta Informatica, 6:133–151, 1976.CrossRefGoogle Scholar
  21. 21.
    D. B. Kemp and P. J. Stuckey. Analysis Based Constraint Query Optimisation. In ICLP'93, pages 666–682, 1993.Google Scholar
  22. 22.
    A. Kerbrat. Personal Communication on Polyhedral library polyhedra.tar. October, 1993.Google Scholar
  23. 23.
    J. Martin, A. King, and P. Soper. Typed Norms for Typed Logic Programs. In LOPSTR'96. Springer-Verlag, 1996.Google Scholar
  24. 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. 25.
    H. Millroth. Reforming Compilation of Logic Programs. PhD thesis, Computing Science Department, Uppsala University, 1990.Google Scholar
  26. 26.
    H. Millroth. Personal Communication on the rôle of Argument Relationships in Reform. October, 1993.Google Scholar
  27. 27.
    L. Plümer. Termination Proofs for Logic Programs. Springer-Verlag, 1990.Google Scholar
  28. 28.
    K. Sohn. Constraints among Argument Sizes in Logic Programs. In PODS'94, pages 68–74. ACM Press, 1994.Google Scholar
  29. 29.
    J. D. Ullman. Implementation of Logical Query Languages for Databases. ACM Transactions on Database Systems, 10(3):289–321, 1985.Google Scholar
  30. 30.
    A. Van Gelder. Deriving constraints among argument sizes in logic programs. Annals of Mathematics and Artifical Intelligence, (3), 1991.Google Scholar
  31. 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. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Florence Benoy
    • 1
  • Andy King
    • 1
  1. 1.Computing LaboratoryUniversity of Kent at CanterburyUK

Personalised recommendations