Compositional analysis of modular logic programs

ABSTRACT

This paper describes a semantic basis for a compositional approach to the analysis of logic programs. A logic program is viewed as consisting of a set of modules, each module defining a subset of the program's predicates. Analyses are constructed by considering abstract interpretations of a compositional semantics. The abstract meaning of a module corresponds to its analysis and composition of abstract meanings corresponds to composition of analyses. Such an approach is essential for large program development so that altering one module does not require re-analysis of the entire program. We claim that for a substantial class of programs, compositional analyses which are based on a notion of abstract unfolding provide the same precision as non-compositional analysis. A compositional analysis for ground dependencies is included to illustrate the approach. To the best of our knowledge this is the first account of a compositional framework for the analysis of logic programs.

REFERENCES

• 1: K. R. Apt , H. A. Blair , A. Walker, Towards a theory of declarative knowledge, Foundations of deductive databases and logic programming, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1988
• 2: Roberto Barbuti , Roberto Giacobazzi , Giorgio Levi, A general framework for semantics-based bottom-up abstract interpretation of logic programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.1, p.133-181, Jan. 1993 [doi>10.1145/151646.151650]
• 3: BIM_Prolog reference manual. B.I.M. B- 3078, Everberg, Belgium.
• 4: A. Bossi, M. Gabbrielli, G. Levi, and M. C. Meo. Contributions to the Semantics of Open Logic Programs. In Proceedings of the Internalional Conference on Fifth Generation Computer Systems 199e, pp. 570-580, 1992.
• 5: M. Bruynooghe, G. :lanssens, B. Demoen, and A. Callebaut. Abstract Interpretation: Towards the Global Optimization of Prolog Programs. In Proc. Fourth IEEE Int'l Syrup. on Logic Programming, pp. 192-204. IEEE Comp. Soc. Press, 1987.
• 6: M. Carlsson and J. Widen. SICS~us Prolog Users Manual SICS, Sweden, 1988.
• 7: W. Chen. A Theory of Modules Based on Second- Order Logic. In Proc. Fourth IEEE Int'l Syrup. on Logic Programming, pp. 24-33. IEEE Comp. Soc. Press, 1987.
• 8: Michael Codish , Dennis Dams , Eyal Yardeni, Bottom-up abstract interpretation of logic programs, Theoretical Computer Science, v.124 n.1, p.93-125, Feb. 14, 1994 [doi>10.1016/0304-3975(94)90055-8]
• 9: M. Codish, M. Falaschi, and K. Marriott. Suspension Analysis for Concurrent Logic Programs. In K. Furukawa, editor, Proc. Eighth Int'l Conf. on Logic Programming, pp. 331-345. The MIT Press, Cambridge, Mass., 1991.
• 10: Keith D. Cooper , Ken Kennedy , Linda Lorczon, Interprocedural optimization: eliminating unnecessary recompilation, Proceedings of the 1986 SIGPLAN symposium on Compiler construction, p.58-67, June 25-27, 1986, Palo Alto, California, United States
• 11: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 12: Patrick Cousot , Radhia Cousot, Systematic design of program analysis frameworks, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.269-282, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567778]
• 13: Patrick Cousot , Radhia Cousot, Comparing the Galois Connection and Widening/Narrowing Approaches to Abstract Interpretation, Proceedings of the 4th International Symposium on Programming Language Implementation and Logic Programming, p.269-295, August 26-28, 1992
• 14: M. Falaschi , G. Levi , C. Palamidessi , M. Martelli, Declarative modeling of the operational behavior of logic languages, Theoretical Computer Science, v.69 n.3, p.289-318, Dec. 18, 1989 [doi>10.1016/0304-3975(89)90070-4]
• 15: H. Gaifman, M. J. Maher, and E. Y. Shapiro. Reactive Behavior Semantics for Concurrent Constraint Logic Programs. In E. Lusk and R. Overbeck, editors, Proc. North American Conf. on Logic Programming'89, pp. 553-572. The MIT Press, Cambridge, Mass., 1989.
• 16: H. Gaifman , E. Shapiro, Fully abstract compositional semantics for logic programs, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.134-142, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75289]
• 17: R. Gerth, M. Codish, Y. Lichtenstein, and E. Shapiro. Fully abstract denotational semantics for Concurrent Prolog. In Proc. Third 1EEE Symp. on Logic In Computer Science, pp. 320- 335. IEEE Computer Society Press, 1988.
• 18: John E. Hopcroft , Jeffrey D. Ullman, Introduction To Automata Theory, Languages, And Computation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
• 19: G. Levi. Models, Unfolding Rules and Fixpoint Semantics. In R. A. Kowalski and K. A. Bowen, editors, Proc. Fifth Int 'l Conf. on Logic Programming, pp. 1649-1665. The MIT Press, Cambridge, Mass., 1988.
• 20: J. W. Lloyd, Foundations of logic programming; (2nd extended ed.), Springer-Verlag New York, Inc., New York, NY, 1987
• 21: P. Mancarella and D. Pedreschi. An Algebra of Logic Programs. In R. A. Kowalski and K. A. Bowen, editors, Proc. Fifth Int'l Conf. on Logic Programming, pp. 1006-1023. The MIT Press, Cambridge, Mass., 1988.
• 22: D. Miller. A Theory of Modules for Logic Programming, in Proceedings IEEE Symposium on Logic Programming, pp. 106-114, 1986.
• 23: Vatsa Santhanam , Daryl Odnert, Register allocation across procedure and module boundaries, Proceedings of the ACM SIGPLAN 1990 conference on Programming language design and implementation, p.28-39, June 1990, White Plains, New York, United States
• 24: Walter F. Tichy , Mark C. Baker, Smart recompilation, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.236-244, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318648]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Logic and constraint programming

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: Modules and interfaces

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Algorithms, Theory