Optimality in goal-dependent analysis of Sharing
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 oil static analysis of logic programming in a single, formal setting. On the abstract side, we focus Oil the domain Sharing by Jacobs and Langen (The Journal of Logic Programming, 1992, vol. 13, nos. 2-3, pp. 291-314) 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 arc 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.
sharing logic programming abstract interpretation unification matching existentially quantified substitutions