Isabelle/HOL中经验证的Timsort的C语言实现
软件工程
2018-12-11 v1
摘要
传统算法的形式化验证因其在现代软件中的广泛应用而具有重要意义。Timsort是一种复杂且混合的稳定排序算法，由归并排序与插入排序衍生而来。尽管OpenJDK中的Timsort实现已得到形式化验证，但目前仍不存在标准且经形式化验证的C语言Timsort实现。本文研究Timsort实现及其在Isabelle/HOL中使用通用命令式语言Simpl的形式化验证。随后，我们从已验证的Simpl规约手动生成Timsort的C实现。由于Simpl具有类C的具体语法，代码生成十分直接。该C实现也已通过一组随机测试用例的测试。
引用
@article{arxiv.1812.03318,
title = {A Verified Timsort C Implementation in Isabelle/HOL},
author = {Yu Zhang and Yongwang Zhao and David Sanan},
journal= {arXiv preprint arXiv:1812.03318},
year = {2018}
}
备注
17 pages, 1 figure