Horn 子句程序的集合分析
计算机科学中的逻辑
2007-08-17 v1
摘要
我们考虑用其所包含元素的集合来近似数据结构。例如，列表、二叉树、元组等可以用其中元素的集合或多重集来近似。此类近似可用于提供逻辑程序的部分正确性属性。例如，人们可能希望指定：每当原子 被证明时，列表 和 包含相同的多重集元素（即 是 的排列）。如果排序去除了重复项，则希望推断出 和 底层的元素集合是相同的。如果这些结果能够被静态且自动地确定，将非常有用。我们提出了一种结构化并自动化此类集合分析的方案。该方案的核心在于使用线性逻辑作为 Horn 子句逻辑底层的计算逻辑。
引用
@article{arxiv.0708.2230,
title = {Collection analysis for Horn clause programs},
author = {Dale Miller},
journal= {arXiv preprint arXiv:0708.2230},
year = {2007}
}