包含算术谓词的程序的自动终止分析
摘要：逻辑程序中显示算术谓词的终止不容易，因为整数的常规顺序不是良序的。介绍了一种新方法，可轻松整合到自动终止分析系统TermiLog中，用于证明这种情况下的终止性。 该方法包括以下步骤：首先，自动推导出用于表示整数范围的有限抽象域。基于这种抽象，将抽象解释应用于程序。结果是有限数量的用于扩展查询映射对的回答的抽象化原子。对于每个可能非终止的查询映射对，猜测一个有界（整数值）的终止函数。如果遍历该对会降低终止函数的值，则可以确定终止性。对于每个查询映射对，通常简单的函数就足够了，这使我们的方法比经典方法更具优势，后者使用单个终止函数来处理所有循环，这无疑更加复杂和难以自动猜测。值得注意的是，使用我们的方法可以自动显示McCarthy的91函数的终止性。 总结起来，所提出的方法基于整数的有限抽象与查询映射对技术相结合，实质上能将终止证明分解为多个情况，每个情况只需要一个简单的终止函数就足够。因此，在TermiLog和类似系统的框架下，整个终止证明过程可以自动完成。
作者：Nachum Dershowitz, Naomi Lindenstrauss, Yehoshua Sagiv, Alexander Serebrenik
论文ID：cs/0011036
分类：Programming Languages
分类简称：cs.PL
提交时间：2007-05-23