AbstractIntegrating semi-naive fixpoint iteration from deductive data bases [3,2,4] (François Bancilhon and Raghu Ramakrishnan: An amateur's introduction to recursive query processing strategies. In ACM SIGMOD Conference, 1986, 16-52; Isaac Balbin and Kotagiri Ramamohanarao: A generalization of the differential approach to recursive query evaluation. Journal of Logic Programming (JLP) 4, 3, 1987, 259-262; François Bancilhon and Raghu Ramakrishnan: Performance evaluation of data intensive logic programs. In Foundations of Deductive Databases.) as well as continuations into worklist-based solvers, we derive a new application independent local fixpoint algorithm for distributive constraint systems. Seemingly different efficient algorithms for abstract interpretation like those for linear constant propagation for imperative languages [16] (Susan Horwitz, Thomas W. Reps, and Mooly Sagiv: Precise interprocedural dataflow analysis with applications to constant propagation. In Proceedings of 6th International Conference on Theory and Practice of Software Development (TAPSOFT), Volume 915 of LNCS, Springer-Verlag, 1995, 651-665.) as well as for control-flow analysis for functional languages [12] (Nevin Heintze: Set-based analysis of ML programs. In ACM Conference on Lisp and Functional Programming (LFP), 1994, 306-317.) turn out to be instances of our scheme. Besides this systematizing contribution we also derive a new efficient algorithm for abstract OLDT-resolution as considered in [14,15,24] (Pascal Van Hentenryck, Olivier Degimbe, Baudouin Le Charlier, and Laurent Michel: Abstract Interpretation of Prolog based on OLDT resolution. Technical Report CS-93-05, Brown University, Providence, RI 02912, 1993; Pascal Van Hentenryck, Olivier Degimbe, Baudouin Le Charlier, and Laurent Michel: The impact of granularity in abstract interpretation of Prolog. In Proceedings of Static Analysis, 3rd International Workshop (WSA), Volume 724 of LNCS, Springer-Verlag, 1993, 1-14; Helmut Seidl and Christian Fecht: Interprocedural analysis based on PDAs. Technical Report 97-06, University Trier, 1997, Extended Abstract in: Verification, Model Checking and Abstract Interpretation A Workshop in Association with ILPS'97. Long version to appear in Journal of Logic Programming (JLP).) for Prolog.
Categories and Subject Descriptors: D.3.4 [Programming Languages]: Processors; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs; F.2.2 [Analysis of Algorithms and Problem Complexity]: Nonnumerical Algorithms and Problems; H.3.3 [Information Storage and Retrieval]: Information Search and Retrieval
Additional Key Words and Phrases: fixpoint computation, semi-naive iteration, program analysis
Selected references
- Isaac Balbin and Kotagiri Ramamohanarao. A generalization of the differential approach to recursive query evaluation. Journal of Logic Programming, 4(3):259-262, September 1987.
- François Bancilhon and Raghu Ramakrishnan. An amateur's introduction to recursive query processing strategies. In Carlo Zaniolo, editor, Proceedings of the 1986 ACM SIGMOD International Conference on Management of Data, pages 16-52, Washington, D.C., 28-30 May 1986. SIGMOD Record 15(2), June 1986.
- Baudouin Le Charlier and Pascal Van Hentenryck. Experimental evaluation of a generic abstract interpretation algorithm for PROLOG. ACM Transactions on Programming Languages and Systems, 16(1):35-101, January 1994.
- Vincent Englebert, Baudouin Le Charlier, Didier Roland, and Pascal Van Hentenryck. Generic abstract interpretation algorithms for Prolog: Two optimization techniques and their experimental evaluation. Software -- Practice and Experience, 23(4):419-459, April 1993.
- Nevin Heintze and David McAllester. On the cubic bottleneck in subtyping and flow analysis. In Proceedings, Twelth Annual IEEE Symposium on Logic in Computer Science, pages 342-351, Warsaw, Poland, 29 June-2 July 1997. IEEE Computer Society Press.
- David Melski and Thomas Reps. Interconvertibility of set constraints and context-free language reachability. In Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pages 74-89, Amsterdam, The Netherlands, 12-13 June 1997.
- K. Muthukumar and Manuel V. Hermenegildo. Compile-time derivation of variable dependency using abstract interpretation. Journal of Logic Programming, 13(2-3):315-347, July 1992.
- Flemming Nielson and Hanne Riis Nielson. Infinitary control flow analysis: a collecting semantics for closure analysis. In Conference Record of POPL '97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 332-345, Paris, France, 15-17 January 1997.
- Robert Paige. Symbolic finite differencing -- part I. In Neil D. Jones, editor, ESOP'90, 3rd European Symposium on Programming, volume 432 of Lecture Notes in Computer Science, pages 36-56, Copenhagen, Denmark, 15-18 May 1990. Springer.
- Jens Palsberg. Closure analysis in constraint form. ACM Transactions on Programming Languages and Systems, 17(1):47-62, January 1995.
- Jens Palsberg and Patrick O'Keefe. A type system equivalent to flow analysis. ACM Transactions on Programming Languages and Systems, 17(4):576-599, July 1995.
- Thomas W. Reps, Susan Horwitz, and Mooly Sagiv. Precise interprocedural dataflow analysis via graph reachability. In Conference Record of POPL '95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 49-61, San Francisco, California, January 1995.
- H. Seidl and M. H. Sørensen. Constraints to stop higher-order deforestation. In Conference Record of POPL '97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 400-413, Paris, France, 15-17 January 1997.
- Harald Søndergaard. An application of abstract interpretation of logic programs: Occur check reduction. In Bernard Robinet and Reinhard Wilhelm, editors, ESOP 86, European Symposium on Programming, volume 213 of Lecture Notes in Computer Science, pages 327-338, Saarbrücken, Federal Republic of Germany, 17-19 March 1986. Springer.