Analysis of Downward Closed Properties of Logic Programs

  • Patricia M. Hill
  • Fausto Spoto
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1816)


We study the analysis of downward closed properties of logic programs, which are a very abstract presentation of types. We generalise to a very large class of downward closed properties the construction of the traditional domains for groundness analysis in such a way that the results enjoy the good properties of that domain. Namely, we obtain abstract domains with a clear representation made of logical formulas and with optimal and well-known abstract operations. Moreover, they can be built using the linear refinement technique, and, therefore, are provably optimal and enjoy the condensing property, which is very important for a goal-independent analysis.


Abstract interpretation domain theory linear refinement type theory type analysis logic programming 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    T. Armstrong, K. Marriott, P. Schachte, and H. Søndergaard. Two Classes of Boolean Functions for Dependency Analysis. Science of Computer Programming, 31(1):3–45, 1998.zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    G. Birkhoff. Lattice Theory. In AMS Colloquium Publication, third ed., 1967.Google Scholar
  3. 3.
    M. Codish and B. Demoen. Deriving Polymorphic Type Dependencies for Logic Programs Using Multiple Incarnations of Prop. In Proc. of the first International Symposium on Static Analysis, volume 864 of Lecture Notes in Computer Science, pages 281–296. Springer-Verlag, 1994.Google Scholar
  4. 4.
    M. Codish and V. Lagoon. Type Dependencies for Logic Programs Using ACI-Unification. In Proceedings of the 1996 Israeli Symposium on Theory of Computing and Systems, pages 136–145. IEEE Press, June 1996. Extended version to appear in Theoretical Computer Science.Google Scholar
  5. 5.
    A. Cortesi, G. Filè, and W. Winsborough. Prop Revisited: Propositional Formula as Abstract Domain for Groundness Analysis. In Proc. Sixth IEEE Symp. on Logic In Computer Science, pages 322–327. IEEE Computer Society Press, 1991.Google Scholar
  6. 6.
    A. Cortesi, G. Filè, and W. Winsborough. Optimal Groundness Analysis Using Propositional Logic. Journal of Logic Programming, 27(2):137–167, 1996.zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    P. Cousot and R. Cousot. Systematic Design of Program Analysis Frameworks. In Proc. 6th ACM Symp. on Principles of Programming Languages, pages 269–282, 1979.Google Scholar
  8. 8.
    P. Cousot and R. Cousot. Abstract Interpretation and Applications to Logic Programs. Journal of Logic Programming, 13(2 & 3):103–179, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    N.J. Cutland. Computability: An Introduction to Recursive Function Theory. Cambridge University Press, 1980.Google Scholar
  10. 10.
    G. Filé, R. Giacobazzi, and F. Ranzato. A Unifying View on Abstract Domain Design. ACM Computing Surveys, 28(2):333–336, 1996.CrossRefGoogle Scholar
  11. 11.
    R. Giacobazzi, F. Ranzato, and F. Scozzari. Building Complete Abstract Interpretations in a Linear Logic-based Setting. In G. Levi, editor, Static Analysis, Proceedings of the 5th International Static Analysis Symposium SAS 98, volume 1503 of Lecture Notes in Computer Science, pages 215–229. Springer-Verlag, 1998.Google Scholar
  12. 12.
    Giorgio Levi and Fausto Spoto. An Experiment in Domain Refinement: Type Domains and Type Representations for Logic Programs. In Catuscia Palamidessi, Hugh Glaser, and Karl Meinke, editors, Principles of Declarative Programming, volume 1490 of Lecture Notes in Computer Science, pages 152–169, Pisa, Italy, September 1998. ©Springer-Verlag.CrossRefGoogle Scholar
  13. 13.
    K. Marriott and H. Søndergaard. Precise and Efficient Groundness Analysis for Logic Programs. ACM Letters on Programming Languages and Systems, 2(1–4):181–196, 1993.CrossRefGoogle Scholar
  14. 14.
    A. Martelli and U. Montanari. An Efficient Unification Algorithm. ACM Transactions on Programming Languages and Systems, 4:258–282, 1982.zbMATHCrossRefGoogle Scholar
  15. 15.
    F. Scozzari. Logical Optimality of Groundness Analysis. In P. Van Hentenryck, editor, Proceedings of the 4th International Static Analysis Symposium SAS’97, volume 1302 of Lecture Notes in Computer Science, pages 83–97. Springer-Verlag, 1997.Google Scholar
  16. 16.
    Jan-Georg Smaus, Patricia Hill, and Andy King. Mode Analysis for Typed Logic Programs. In Proc. of the LOPSTR’99 Workshop, pages 163–170, Venice, Italy, September 1999.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Patricia M. Hill
    • 1
  • Fausto Spoto
    • 2
  1. 1.School of Computer StudiesUniversity of LeedsLeedsUK
  2. 2.Dipartimento di InformaticaUniversità di PisaPisaItaly

Personalised recommendations