×

Optimality in goal-dependent analysis of sharing. (English) Zbl 1181.68095

Summary: We face the problems of correctness, optimality, and precision for the static analysis of logic programs, using the theory of abstract interpretation. We propose a framework with a denotational, goal-dependent semantics equipped with two unification operators for forward unification (calling a procedure) and backward unification (returning from a procedure). The latter is implemented through a matching operation. Our proposal clarifies and unifies many different frameworks and ideas on static analysis of logic programming in a single, formal setting. On the abstract side, we focus on the domain sharing by D. Jacobs and A. Langen [J. Log. Program. 13, No. 2–3, 291–314 (1992; Zbl 0776.68026)] and provide the best correct approximation of all the primitive semantic operators, namely, projection, renaming, and forward and backward unifications. We show that the abstract unification operators are strictly more precise than those in the literature defined over the same abstract domain. In some cases, our operators are more precise than those developed for more complex domains involving linearity and freeness.

MSC:

68N17 Logic programming

Citations:

Zbl 0776.68026
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] DOI: 10.1145/321978.321991 · Zbl 0339.68004 · doi:10.1145/321978.321991
[2] Hans, Aliasing and Groundness Analysis of Logic Programs through Abstract Interpretation and Its Safety (1992)
[3] Søndergaard, Proc. ESOP 86 pp 327– (1986) · doi:10.1007/3-540-16442-1_25
[4] DOI: 10.1016/S0743-1066(99)00007-2 · Zbl 0944.68029 · doi:10.1016/S0743-1066(99)00007-2
[5] DOI: 10.1016/0743-1066(91)80001-T · Zbl 0717.68010 · doi:10.1016/0743-1066(91)80001-T
[6] DOI: 10.1016/0304-3975(94)90084-1 · Zbl 0811.68068 · doi:10.1016/0304-3975(94)90084-1
[7] DOI: 10.1145/333979.333989 · Zbl 1133.68370 · doi:10.1145/333979.333989
[8] DOI: 10.1016/S0743-1066(97)10002-4 · Zbl 0905.68029 · doi:10.1016/S0743-1066(97)10002-4
[9] Furukawa, Logic Programming: Proc. of the Eighth International Conference (1991)
[10] DOI: 10.1109/ICCL.1994.288389 · doi:10.1109/ICCL.1994.288389
[11] DOI: 10.1016/0743-1066(92)90030-7 · Zbl 0776.68024 · doi:10.1016/0743-1066(92)90030-7
[12] Cousot, Proc. of the Sixth ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages pp 269– (1979) · doi:10.1145/567752.567778
[13] DOI: 10.1016/0743-1066(95)00123-9 · Zbl 0874.68052 · doi:10.1016/0743-1066(95)00123-9
[14] Cortesi, Optimal Groundness Analysis Using Propositional Formulas (1994)
[15] Palamidessi, Automata, Languages and Programming, 17th International Colloquium Warwick University, England, July 16–20, 1990, Proc. pp 386– (1990)
[16] DOI: 10.1017/S1471068404001978 · Zbl 1093.68015 · doi:10.1017/S1471068404001978
[17] DOI: 10.1016/0743-1066(92)90035-2 · Zbl 0776.68032 · doi:10.1016/0743-1066(92)90035-2
[18] DOI: 10.1016/S0304-3975(00)00312-1 · Zbl 0997.68021 · doi:10.1016/S0304-3975(00)00312-1
[19] Muthukumar, Logic Programming: Proc. of the Eighth International Conference pp 49– (1991)
[20] Apt, Handbook of Theoretical Computer Science. Vol. B: Formal Models and Semantics pp 495– (1990)
[21] DOI: 10.1145/177492.177650 · doi:10.1145/177492.177650
[22] Amato, Logic Based Program Synthesis and Transformation 12th International Workshop, LOPSTR 2002, Madrid, Spain, September 17–20, 2002. Revised Selected Papers pp 52– (2003)
[23] Lloyd, Foundations of Logic Programming (1987) · Zbl 0668.68004 · doi:10.1007/978-3-642-83189-8
[24] Amato, Proc. of the Joint Conference on Declarative Programming (AGP’02) pp 189– (2002)
[25] DOI: 10.1016/S0890-5401(02)00048-2 · Zbl 1036.68020 · doi:10.1016/S0890-5401(02)00048-2
[26] DOI: 10.1145/174625.174627 · doi:10.1145/174625.174627
[27] Le Charlier, Logic Programming: Proc. of the Eighth International Conference pp 64– (1991)
[28] King, Abstract Matching Can Improve on Abstract Unification (1995)
[29] DOI: 10.1016/S0743-1066(00)00009-1 · Zbl 0964.68017 · doi:10.1016/S0743-1066(00)00009-1
[30] King, Programming Languages and Systems ESOP ’94, Fifth European Symposium on Programming Edinburg, U.K., April 11–13, 1994, Proc. pp 363– (1994)
[31] DOI: 10.1016/0743-1066(92)90034-Z · Zbl 0776.68026 · doi:10.1016/0743-1066(92)90034-Z
[32] DOI: 10.1017/S1471068402001497 · Zbl 1105.68329 · doi:10.1017/S1471068402001497
[33] DOI: 10.1017/S1471068403001868 · Zbl 1088.68027 · doi:10.1017/S1471068403001868
[34] DOI: 10.1016/0743-1066(93)00007-F · Zbl 0829.68023 · doi:10.1016/0743-1066(93)00007-F
[35] Henkin, Cylindric Algebras Part I (1971)
[36] DOI: 10.1016/S0743-1066(98)10026-2 · Zbl 0942.68610 · doi:10.1016/S0743-1066(98)10026-2
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.