More Web Proxy on the site http://driver.im/

Article

Free access

Compositional analysis of modular logic programs

Authors:

Michael Codish,

Saumya K. Debray,

Roberto GiacobazziAuthors Info & Claims

POPL '93: Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 451 - 464

https://doi.org/10.1145/158511.158703

Published: 01 March 1993 Publication History

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. Blair, and A. Walker. Towards a Theory of Declarative Knowledge. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming, pp. 89-148. Morgan Kaufmann, Los Altos, Ca., 1988.]]

Digital Library

[2]

R. Barbuti, R. Giacobazzi, and G. Levi. A General Framework for Semantics-based Bottom-up Abstract Interpretation of Logic Programs. Technical Report TR 12/91, Dipartimento di Informatica, Universit~ di Pisa, 1991. To appear in A CM Transactions on Programming Languages and Systems.]]

Digital Library

[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.]]

Digital Library

[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]

M. Codish, D. Dams, and E. Yardeni. Bottomup Abstract interpretation of Logic Programs. Technical report, Dept. of Computer Science, The Weizmann Institute, Rehovot, 1990. To appear in Theoretical Computer Science.]]

Digital Library

[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]

K.D. Cooper, K. Kennedy, and L. Torczon. Interprocedural Optimization" Eliminating Unecessary Recompilation. In Proc. SIGPLAN '85 Symp. on Compiler Cons~rnction, pp. 58-67, 1986.]]

Digital Library

[11]

P. Cousot and R. Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Proc. Fourth A CM Syrup. Principles of Programming Languages, pp. 238-252, 1977.]]

Digital Library

[12]

P. Cousot and R. Cousot. Systematic Design of Program Analysis Frameworks. In Proc. Sixth A CM Syrup. Principles of Programming Languages, pp. 269-282, 1979.]]

Digital Library

[13]

P. Cousot and R. Cousot. Comparing the Galois Connection and Widening/Narrowing Approaches to Abstract Interpretation. In M. Bruynooghe and M. Wirsing, editors, Proc. of PLILP'92, volume 631 of Lecture Notes in Computer Science, pages 269-295. Springer-Verlag, Berlin, 1992.]]

Digital Library

[14]

M. Falaschi, G. Levi, M. Martelli, and C. Palamidessi. Declarative Modeling of the Operational Behavior of Logic Languages. Theoretical Computer Science, 69(3):289-318, 1989.]]

Digital Library

[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 and E. Shapiro. Fully abstract compositional semantics for logic programs, in Proc. Sixteenth Annual A CM Symp. on Principles of Programming Languages, pp. 134-142. ACM, 1989.]]

Digital Library

[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]

J. E. ttopcroft and 3. D. Ullman, Introduction to Automata Theory, Languages, and Computation, Addison-Wesley, 1979.]]

Digital Library

[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. Springer-Verlag, Berlin, 1987. Second edition.]]

Digital Library

[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]

V. Santhanam and D. Odnert, "Register Allocation across Procedure and Module Boundaries", Proc. A CM SIGPLAN-90 Conference on Programming Language Design and Implemen~ation, White Plains, NY, June 1990, pp. 28-39.]]

Digital Library

[24]

W.F. Tichy and M.C. Baker. Smart Recompilation. In Proc. Twelfth A CM Syrup. on Principles of Programming Languages, pp. 236-244. ACM, 1985.]]

Digital Library

Cited By

Koppel JKearl JSolar-Lezama A(2022)Automatically deriving control-flow graph generators from operational semanticsProceedings of the ACM on Programming Languages10.1145/35476486:ICFP(742-771)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547648
Kovács A(2022)Staged compilation with two-level type theoryProceedings of the ACM on Programming Languages10.1145/35476416:ICFP(540-569)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547641
Ullrich Sde Moura L(2022)‘do’ unchained: embracing local imperativity in a purely functional language (functional pearl)Proceedings of the ACM on Programming Languages10.1145/35476406:ICFP(512-539)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547640
Show More Cited By

Index Terms

Compositional analysis of modular logic programs
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Modules / packages
2. Theory of computation
  1. Logic
    1. Constraint and logic programming
  2. Semantics and reasoning
    1. Program semantics

Recommendations

Fully abstract compositional semantics for logic programs
POPL '89: Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

We propose a framework for discussing fully abstract compositional semantics, which exposes the interrelations between the choices of observables, compositions, and meanings. Every choice of observables and compositions determines a unique fully ...
A refinement calculus for logic programs

Existing refinement calculi provide frameworks for the stepwise development of imperative programs from specifications. This paper presents a refinement calculus for deriving logic programs. The calculus contains a wide-spectrum logic programming ...
Compositional model-theoretic semantics for logic programs
Abstract
We present a compositional model-theoretic semantics for logic programs, where the composition of programs is modelled by the composition of the admissible Herbrand models of the programs. An Herbrand model is admissible if it is supported by the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '93: Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

March 1993

510 pages

ISBN:0897915607

DOI:10.1145/158511

Chairmen:
Mary Van Deusen
IBM Watson Research Center
,
Bernard Lang
INRIA Rocquencourt

Copyright © 1993 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 March 1993

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

POPL93

Sponsor:

POPL93: 20th ACM Symposium on Principles of Programming Languages

South Carolina, Charleston, USA

Acceptance Rates

POPL '93 Paper Acceptance Rate 39 of 199 submissions, 20%;

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

48
Total Citations
View Citations
319
Total Downloads

Downloads (Last 12 months)71
Downloads (Last 6 weeks)11

Reflects downloads up to 11 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Koppel JKearl JSolar-Lezama A(2022)Automatically deriving control-flow graph generators from operational semanticsProceedings of the ACM on Programming Languages10.1145/35476486:ICFP(742-771)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547648
Kovács A(2022)Staged compilation with two-level type theoryProceedings of the ACM on Programming Languages10.1145/35476416:ICFP(540-569)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547641
Ullrich Sde Moura L(2022)‘do’ unchained: embracing local imperativity in a purely functional language (functional pearl)Proceedings of the ACM on Programming Languages10.1145/35476406:ICFP(512-539)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547640
Illous HLemerre MRival X(2021)Interprocedural Shape Analysis Using Separation Logic-Based Transformer SummariesStatic Analysis10.1007/978-3-030-65474-0_12(248-273)Online publication date: 13-Jan-2021
https://doi.org/10.1007/978-3-030-65474-0_12
Comini MLevi G(2017) Beyond the s -Semantics: a Theory of Observables Logic and algebra10.1201/9780203748671-3(25-67)Online publication date: 2-Nov-2017
https://doi.org/10.1201/9780203748671-3
Castelnuovo GNaik MRinetzky NSagiv MYang H(2015)Modularity in Lattices: A Case Study on the Correspondence Between Top-Down and Bottom-Up AnalysisStatic Analysis10.1007/978-3-662-48288-9_15(252-274)Online publication date: 2-Sep-2015
https://doi.org/10.1007/978-3-662-48288-9_15
Ramírez-Deantes DCorreas JPuebla G(2010)Modular termination analysis of java bytecode and its application to phoneME core librariesProceedings of the 7th international conference on Formal Aspects of Component Software10.1007/978-3-642-27269-1_13(218-236)Online publication date: 14-Oct-2010
https://dl.acm.org/doi/10.1007/978-3-642-27269-1_13
Bruscoli PGuglielmi A(2009)On the proof complexity of deep inferenceACM Transactions on Computational Logic10.1145/1462179.146218610:2(1-34)Online publication date: 2-Mar-2009
https://dl.acm.org/doi/10.1145/1462179.1462186
Schröder LPattinson D(2009)PSPACE bounds for rank-1 modal logicsACM Transactions on Computational Logic10.1145/1462179.146218510:2(1-33)Online publication date: 2-Mar-2009
https://dl.acm.org/doi/10.1145/1462179.1462185
Gabbrielli MMeo M(2009)A compositional semantics for CHRACM Transactions on Computational Logic10.1145/1462179.146218310:2(1-36)Online publication date: 2-Mar-2009
https://dl.acm.org/doi/10.1145/1462179.1462183
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents