目标依赖共享分析中的最优性
Optimality in Goal-Dependent Analysis of Sharing
摘要：
利用抽象解释理论对逻辑程序进行静态分析，面临正确性、最优性和精度问题。我们提出了一个框架，配备了两个统一运营商的向前统一（调用程序）和向后统一（从程序返回）的指称，目标相关的语义。后者通过匹配操作实现。我们的建议澄清和统一了许多不同的框架和思想的静态分析的逻辑编程在一个单一的，正式的设置。在抽象方面，我们专注于域共享的Jacobs和Langen，并提供最佳的正确近似的所有原始的语义算子，即投影，重命名，向前和向后统一。我们表明，抽象的统一运营商是严格更精确的比那些在文献中定义在同一个抽象域。在某些情况下，我们的运营商是更精确的比那些更复杂的领域，涉及线性和自由度。逻辑程序设计理论与实践（Theory and Practice of Logic Programming，TPLP）
英文摘要：
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)
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
