Size-change termination as a contract: dynamically and statically enforcing termination for higher-order programs
Size-change termination as a contract: dynamically and statically enforcing termination for higher-order programs
复制标题
DOI：
10.1145/3314221.3314643
复制
发表时间：
2018-08
期刊：
影响因子：
--
通讯作者：
Phuc C. Nguyen;Thomas Gilray;Sam Tobin-Hochstadt;David Van Horn
中科院分区：
文献类型：
--
作者：
Phuc C. Nguyen;Thomas Gilray;Sam Tobin-Hochstadt;David Van Horn
终止性是一个重要的但不可判定的程序属性，这导致了大量的静态方法保守预测或强制终止的工作。其中一种方法是Lee、Jones和Ben-Amram的大小变化终止方法，它分为两个阶段：（1）将程序抽象为“大小变化图”，（2）检查这些图的大小变化性质：存在导致无限递减序列的路径。我们转置这两个阶段的操作语义，占运行时执行的大小更改属性，推迟（或完全避免）程序抽象。这种选择有两个关键的后果：（1）大小变化终止可以在运行时检查和（2）终止可以被重新表述为使用现有的系统抽象方法分析的安全属性。我们制定运行时的大小变化检查合同的风格Findler和Felleisen。结果恭维现有的合同，强制执行部分正确性规范，以获得合同的总正确性。我们的方法结合了鲁棒性的大小变化的原则终止与运行时提供的精确信息。它具有可调的开销，并且可以检查非终止性，而无需静态检查中所需的保守性。为了获得一个健全的和可计算的终止分析，我们直接应用现有的抽象解释技术的操作语义，避免了需要自定义的抽象终止。由此产生的分析仪与现有的专用分析仪相比具有竞争力。
Termination is an important but undecidable program property, which has led to a large body of work on static methods for conservatively predicting or enforcing termination. One such method is the size-change termination approach of Lee, Jones, and Ben-Amram, which operates in two phases: (1) abstract programs into “size-change graphs,” and (2) check these graphs for the size-change property: the existence of paths that lead to infinite decreasing sequences. We transpose these two phases with an operational semantics that accounts for the run-time enforcement of the size-change property, postponing (or entirely avoiding) program abstraction. This choice has two key consequences: (1) size-change termination can be checked at run-time and (2) termination can be rephrased as a safety property analyzed using existing methods for systematic abstraction. We formulate run-time size-change checks as contracts in the style of Findler and Felleisen. The result compliments existing contracts that enforce partial correctness specifications to obtain contracts for total correctness. Our approach combines the robustness of the size-change principle for termination with the precise information available at run-time. It has tunable overhead and can check for nontermination without the conservativeness necessary in static checking. To obtain a sound and computable termination analysis, we apply existing abstract interpretation techniques directly to the operational semantics, avoiding the need for custom abstractions for termination. The resulting analyzer is competitive with with existing, purpose-built analyzers.