Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits
Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits
复制标题
DOI：
10.1007/s10817-017-9431-7
复制
发表时间：
2019-03-01
期刊：
影响因子：
--
通讯作者：
Pottier, Francois
中科院分区：
文献类型：
--
作者：
Chargueraud, Arthur;Pottier, Francois
Union-Find是简单数据结构的一个著名例子，其摊销渐近时间复杂度分析是非平凡的。我们提出了一个Coq形式化的分析，Alstrup等人。的最新证据。此外，我们将Union-Find实现为一个OCaml库，并正式赋予它一个模块化规范，提供完整的功能正确性保证以及摊销的复杂性约束。为了在Coq中对命令式OCaml代码进行推理，我们使用CFML工具，该工具为OCaml的一个子集实现了分离逻辑，并且我们使用时间信用对其进行了扩展。虽然原则上大家都知道摊销分析可以用时间信用来解释，而且时间信用可以被视为分离逻辑中的资源，但我们相信我们的工作是这种方法的第一次实际演示。最后，为了解释我们方法的元理论基础，我们为无类型按值调用演算定义了一个带有时间积分的分离逻辑，并正式验证了它的合理性。
Union-Find is a famous example of a simple data structure whose amortized asymptotic time complexity analysis is nontrivial. We present a Coq formalization of this analysis, following Alstrup et al.'s recent proof. Moreover, we implement Union-Find as an OCaml library and formally endow it with a modular specification that offers a full functional correctness guarantee as well as an amortized complexity bound. In order to reason in Coq about imperative OCaml code, we use the CFML tool, which implements Separation Logic for a subset of OCaml, and which we extend with time credits. Although it was known in principle that amortized analysis can be explained in terms of time credits and that time credits can be viewed as resources in Separation Logic, we believe our work is the first practical demonstration of this approach. Finally, in order to explain the meta-theoretical foundations of our approach, we define a Separation Logic with time credits for an untyped call-by-value -calculus, and formally verify its soundness.