Prolog 的序列化抽象解释

虽然已提出许多针对 Prolog 的抽象解释框架和分析方法，旨在提取有助于程序优化的信息，但这些方法都未能捕捉现有实现语言中的某些控制结构。在本文中，我们提出了一种新的抽象解释框架，用于处理深度优先搜索规则和 cut 运算符。该框架依赖于替换序列（substitution sequence）来建模目标执行的结果。该框架包括（i）一种具体语义的函数定义，（ii）以后置固定点类（post-fixpoints）形式定义的具体语义的安全抽象，以及（iii）一种通用的抽象解释算法。我们展示了传统的替换抽象域可轻松适应新的框架，并提供了实证，说明该方法有效。我们还展示了以前的确定性分析工作（该工作在现有抽象解释框架中无法表达）可视为该框架的一个实例。