使用ACI-统一性分析多态类型逻辑程序
摘要：使用抽象解释技术对(部分)地域进行分析是一项重要的应用。通过利用类型信息提高此类分析的精度有几种提议，包括与Hill和King的合作，我们展示了如何利用程序的类型声明中的信息以准确且有限的方式来描述一个术语的实例化程度。这种方法适用于多态类型的程序，如Goedel或HAL。在此，我们按照Codish，Lagoon和Stuckey的作品对该方法进行改进。为了形式化我们要描述的术语的属性，我们使用标记函数，这是从术语中沿着某些路径提取子术语的函数。抽象术语收集术语的所有标记函数的结果。在分析过程中，程序在抽象术语上执行，而不是在具体术语上执行，并且通常的统一操作被替换为在一个包括著名的ACI理论在内的等同理论下的统一操作。因此，我们就所考虑的类型系统推广了Codish，Lagoon和Stuckey的作品，并将各个作品相互联系起来。
作者：Jan-Georg Smaus
论文ID：cs/0105007
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23