Splay⁺树算法的函数式建模及其自动化验证

摘要

Splay树是一种自平衡的二叉搜索树，支持高效的数据检索操作，广泛应用于序列访问、内存管理和文件系统等领域中．然而，目前关于Splay树算法的验证工作大多局限于手工推导或交互式机械化验证，自动化程度较低，需要较多人为干预．为此，该文提出了Splay树算法的自动化验证方法．首先，使用locale刻画Splay树典型算法的局部参数和逻辑规约．然后，设计了Splay⁺树的结构，以更高效地实现这些算法，并基于该结构进行函数式建模．接着，构建验证引理库，并在Isabelle中自动化验证了算法的正确性．最后，通过对locale的区域解释检验了方法的有效性．

关键词

Splay树 / 函数式建模 / 自动化验证 / Isabelle定理证明器