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

Article

Free access

Type analysis of Prolog using type graphs

Authors:

P. Van Hentenryck,

B. Le CharlierAuthors Info & Claims

PLDI '94: Proceedings of the ACM SIGPLAN 1994 conference on Programming language design and implementation

Pages 337 - 348

https://doi.org/10.1145/178243.178479

Published: 01 June 1994 Publication History

Abstract

Type analysis of Prolog is of primary importance for high-performance compilers, since type information may lead to better indexing and to sophisticated specializations of unification and built-in predicates to name a few. However, these optimizations often require a sophisticated type inference system capable of inferring disjunctive and recursive types and hence expensive in computation time.

The purpose of this paper is to describe a type analysis system for Prolog based on abstract interpretation and type graphs (i.e. disjunctive rational trees) with this functionality. The system (about 15,000 lines of C) consists of the combination of a generic fixpoint algorithm, a generic pattern domain, and a type graph domain. The main contribution of the paper is to show that this approach can be engineered to be practical for medium-sized programs without sacrificing accuracy. The main technical contributions to achieve this result are (1) a novel widening operator for type graphs which appears to be accurate and effective in keeping the sizes of the graphs, and hence the computation time, reasonably small; (2) the use of the generic pattern domain to obtain a compact representation of equality constraints between subterms and to factor out sure structural information.

References

[1]

M. Bruynooghe. A Practical Framework for the Abstract Interpretation of Logic Programs. Journal of Logic Programming, 10(2):91-124, February 1991.

Digital Library

[2]

M Bruynooghe and G Janssens. An Instance of Abstract Interpretation: Integrating Type and Mode Inferencing. In Proc. Fifth lnternational Conference on Logic Programming, pages 669-683, Seattie, WA, August 1988. MIT Press, Cambridge.

[3]

A. Cortesi, B. Le Charlier, and P. Van Hentenryck. Combinations of Abstract Domains for Logic Programming. In 21st Annual A CM SIGPLAN- SIGACT Symposium on Principles Of Programming Languages, Portland, OR, January 1994.

Digital Library

[4]

P Cousot and R. Cousot. Abstract Interpretation: A Unified Lattice ModeI for Static Analysis of Programs by Construction or Approximation of Fixpoints. In New York ACM Press, editor, Conf. Record of Fourth A CM Symposium on Programming Languages (POPL'77), pages 238-252, Los Angeles, CA, January 1977.

Digital Library

[5]

M. Dincbas, H. Simonis, and P. Van Hentenryck. Solving Large Combinatorial Problems in Logic Programming. Journal of Logic Programming, 8(1- 2):75-93, January/March 1990.

Digital Library

[6]

V. Englebert, B. Le Charher, D. Roland, and P. Van Hentenryck. Generic Abstract Interpretation Algorithms for Prolog: Two Optimization Techniques and Their ExperimentM Evaluation. Software Practice and Experience, 23(4), April 1993.

Digital Library

[7]

T. Fruehwirth, E. Shapiro, M. Vardi, and E. Yardeni. Logic Programs as Types for Logic Programs. In !EEE 6th Annual Symposium on Logic in Computer Science, pages 300-309, 1991.

[8]

N. Heintze. Practical Aspects of Set-based Analysis. In Proceedings of the International Joznt Conference and Symposium on Logic Programming (JJCSLP-92), Washington, DC, November 1992.

[9]

N. Heintze and J. Jaffar. A Finite Presentation Theorem for Approximating Logic Programs. In Proc. 17th A CM Syrup. on Principles of Programming Languages, pages 197-209, 1990.

Digital Library

[10]

G. Janssens and M. Bruynooghe. Deriving Description of Possible Values of Program Variables by Means of Abstract Interpretation. Journal of Logic Programming, 13(2-3):205-258, 1992.

Digital Library

[11]

T. Kanamori and T. Kawamura. Analysing Success Patterns of Logic Programs by Abstract Hybrid Interpretation. Technical report, ICOT, 1987.

[12]

B. Le Charlier and P. Van Hentenryck. Experimental Evaluation of a Generic Abstract Interpretation Algorithm for Prolog. A CM Transactions on Programming Languages and Systems. To appear. An extended abstract appeared in the Proceedings of Fourth IEEE International Conference on Computer Languages (ICCL'92), San Francisco, CA, April 1992.

Digital Library

[13]

B. Le Charlier and P. Van Hentenryck. A Universal Top-Down Fixpoint Algorithm. Technical Report CS-92-25, CS Department, Brown University, 1992.

Digital Library

[14]

K. Marriott and H. Sondergaard. Notes for a Tutorial on Abstract Interpretation of Logic Programs. North American Conference on Logic Programming, Cleveland, Ohio, October 1989.

[15]

P. Mishra. Towards a Theory of Types in Prolog. In International Symposzum on Logic Programming, pages 289-298, 1984.

[16]

B. Monsuez. Polymorphic Types and Widening Operators. In International Workshop on Static Analysis (WSA-93), Padova, Italy, September 1993.

Digital Library

[17]

A. Mulkers, W. Winsborough, and M. Bruynooghe. Analysis of Shared Data Structures for Compfie- Time Garbage Collection in Logic Programs. In Seventh International Conference on Logzc Programming (ICLP-90), pages 747-764, Jerusalem, Israel, June 1990. MIT Press, Cambridge.

Digital Library

[18]

K. Muthukumar and M. Hermenegildo. Compile- Time Derivation of Variable Dependency Using Abstract Interpretation. Journal of Logic Programming, 13(2-3):315-347, August 1992.

Digital Library

[19]

L. Sterling and E. Shapiro. The Art of Prolog: Advanced Programming Techniques. MIT Press, Cambridge, Ms, 1986.

Digital Library

[20]

P. Van Hentenryck. Constraint Saris/action in Logic Programming. Logic Programming Series, The MIT Press, Cambridge, MA, 1989.

Digital Library

[21]

P. Van Hentenryck, A. Cortesi, and B. Le Charlier. Type Analysis of Prolog Using Type Graphs. Technical Report CS-93-52, CS Department, Brown University, November 1993.

Digital Library

[22]

K. Verschaetse and D. De Schreye. Deriving Termination Proofs for Logic Programs Using Abstract Procedures. in Eighth International Conference on Logic Programming (ICLP-91), Paris (France), June 1991.

[23]

W. Winsborough. Multiple Specialization using Minimal-Function Graph Semantics. Journal of Logic Programming, 13(4), July 1992.

Digital Library

Cited By

Cortesi AZanioli M(2011)Widening and narrowing operators for abstract interpretationComputer Languages, Systems and Structures10.1016/j.cl.2010.09.00137:1(24-42)Online publication date: 1-Apr-2011
https://dl.acm.org/doi/10.1016/j.cl.2010.09.001
Cortesi A(2008)Widening Operators for Abstract InterpretationProceedings of the 2008 Sixth IEEE International Conference on Software Engineering and Formal Methods10.1109/SEFM.2008.20(31-40)Online publication date: 10-Nov-2008
https://dl.acm.org/doi/10.1109/SEFM.2008.20
Martin JKing ASoper P(2005)Typed norms for typed logic programsLogic Program Synthesis and Transformation10.1007/3-540-62718-9_13(224-238)Online publication date: 3-Jun-2005
https://doi.org/10.1007/3-540-62718-9_13
Show More Cited By

Index Terms

Type analysis of Prolog using type graphs
1. Software and its engineering
  1. Software notations and tools
    1. Compilers
    2. General programming languages
      1. Language types
2. Theory of computation

Recommendations

Type Analysis of Prolog Using Type Graphs
Formalizing Type Operations Using the “Image” Type Constructor

In this paper we introduce a new approach to formalizing certain type operations in type theory. Traditionally, many type constructors in type theory are independently axiomatized and the correctness of these axioms is argued semantically. In this paper ...
Type analysis of Prolog using type graphs

Type analysis of Prolog is of primary importance for high-performance compilers, since type information may lead to better indexing and to sophisticated specializations of unification and built-in predicates to name a few. However, these optimizations ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI '94: Proceedings of the ACM SIGPLAN 1994 conference on Programming language design and implementation

August 1994

360 pages

ISBN:089791662X

DOI:10.1145/178243

Chairmen:
Vivek Sarkar
IBM Santa Teresa Lab.
,
Barbara Ryder
Rutgers Univ., New Brunswick, NJ
,
Mary Lou Soffa
Univ. of Pittsburgh, Pittsburgh, PA

ACM SIGPLAN Notices Volume 29, Issue 6
June 1994
360 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/773473
Guest Editor:
Brent T. Hailpern
Issue’s Table of Contents

Copyright © 1994 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

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 June 1994

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

PLDI94

Sponsor:

SIGPLAN

PLDI94: ACM SIGPLAN Conference on Programming Language Design and Implementation

June 20 - 24, 1994

Florida, Orlando, USA

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

12
Total Citations
View Citations
418
Total Downloads

Downloads (Last 12 months)91
Downloads (Last 6 weeks)8

Reflects downloads up to 12 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Cortesi AZanioli M(2011)Widening and narrowing operators for abstract interpretationComputer Languages, Systems and Structures10.1016/j.cl.2010.09.00137:1(24-42)Online publication date: 1-Apr-2011
https://dl.acm.org/doi/10.1016/j.cl.2010.09.001
Cortesi A(2008)Widening Operators for Abstract InterpretationProceedings of the 2008 Sixth IEEE International Conference on Software Engineering and Formal Methods10.1109/SEFM.2008.20(31-40)Online publication date: 10-Nov-2008
https://dl.acm.org/doi/10.1109/SEFM.2008.20
Martin JKing ASoper P(2005)Typed norms for typed logic programsLogic Program Synthesis and Transformation10.1007/3-540-62718-9_13(224-238)Online publication date: 3-Jun-2005
https://doi.org/10.1007/3-540-62718-9_13
Weyer GWinsborough W(2005)Annotated structure shape graphs for abstract analysis of PrologProgramming Languages: Implementations, Logics, and Programs10.1007/3-540-61756-6_79(92-106)Online publication date: 7-Jun-2005
https://doi.org/10.1007/3-540-61756-6_79
Waal DThielscher M(2005)Solving deductive planning problems using program analysis and transformationLogic Program Synthesis and Transformation10.1007/3-540-60939-3_15(189-203)Online publication date: 1-Jun-2005
https://doi.org/10.1007/3-540-60939-3_15
Solnon CRueher M(2005)Propagation of inter-argument dependencies in “Tuple-distributive” type inference systemsLogic Program Synthesis and Transformation — Meta-Programming in Logic10.1007/3-540-58792-6_13(199-214)Online publication date: 9-Jun-2005
https://doi.org/10.1007/3-540-58792-6_13
Waal DGallagher J(2005)The applicability of logic program analysis and transformation to theorem provingAutomated Deduction — CADE-1210.1007/3-540-58156-1_15(207-221)Online publication date: 30-May-2005
https://doi.org/10.1007/3-540-58156-1_15
Basu SRamakrishnan C(2003)Compositional analysis for verification of parameterized systemsProceedings of the 9th international conference on Tools and algorithms for the construction and analysis of systems10.5555/1765871.1765902(315-330)Online publication date: 7-Apr-2003
https://dl.acm.org/doi/10.5555/1765871.1765902
Basu SRamakrishnan C(2003)Compositional Analysis for Verification of Parameterized SystemsTools and Algorithms for the Construction and Analysis of Systems10.1007/3-540-36577-X_23(315-330)Online publication date: 28-Feb-2003
https://doi.org/10.1007/3-540-36577-X_23
Heintze NMcAllester D(1997)On the complexity of set-based analysisACM SIGPLAN Notices10.1145/258949.25896332:8(150-163)Online publication date: 1-Aug-1997
https://dl.acm.org/doi/10.1145/258949.258963
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