Horn子句程序的集合分析
摘要：利用包含在其中的物品的集合或多集合来近似表示数据结构。例如，列表、二叉树、元组等可以由其中的物品的集合或多集合来近似表示。这样的近似可以用来提供逻辑程序的部分正确性属性。例如，当证明了原子 $sort(t,s)$ 时，希望指定列表 $t$ 和 $s$ 包含相同的多集合物品（即 $s$ 是 $t$ 的一个排列）。如果排序会删除重复项，那么希望能推断出 $t$ 和 $s$ 的底层物品集合是相同的。如果这些结果可以静态和自动地确定，那么它们可能是有用的。我们提出了一种结构化和自动化的集合分析方案。这种方案的核心是使用线性逻辑作为Horn子句逻辑的计算逻辑。
作者：Dale Miller (INRIA Futurs)
论文ID：0708.2230
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-08-17