Optimality in Goal-Dependent Analysis of Sharing

Details Optimality in Goal-Dependent Analysis of Sharing Optimality in Goal-Dependent Analysis of Sharing

2005-03-22

arxiv.org/abs/cs/0503055v2

Theory and Practice of Logic Programming, volume 9, issue 05, pp. 617-689, 2009

Computer Science

Programming Languages

Scientific paper

10.1017/S1471068409990111

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 Jacobs and Langen and provide the best correct approximation of all the primitive semantic operators, namely, projection, renaming, forward and backward unification. 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. To appear in Theory and Practice of Logic Programming (TPLP)

Affiliated with

Also associated with

No associations

Rating

Optimality in Goal-Dependent Analysis of Sharing does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Optimality in Goal-Dependent Analysis of Sharing, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Optimality in Goal-Dependent Analysis of Sharing will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-134714