Page 110 - 《软件学报》2025年第8期

左正康 等: 动态顺序统计树类结构的函数式建模及其自动化验证 3533

(1) 综合考虑不同搜索树结构的性质和操作, 将动态集合和顺序统计量的相关操作融入其中, 添加了额外的高
效数据检索操作. 基于此, 建立了动态顺序统计树类结构的函数式建模框架, 包含其函数式定义、建模策略和不变
式, 简化了建模流程;
(2) 提出了动态顺序统计树类结构相关算法的自动化验证框架, 使用同态的列表模拟动态顺序统计树类结构
的 10 种操作, 设计并验证了列表辅助函数, 借助列表辅助函数构建了通用且可复用的验证引理库, 可自动化验证
动态顺序统计树相关算法的功能正确性;
(3) 将动态顺序统计树类结构的函数式建模框架分别实例化为不平衡的二叉搜索树、红黑树和 2−3 树, 实例
化得到的数据结构具有动态顺序统计树的高效检索特性. 本文所提的自动化验证框架除了适用现有工作已经得到
验证的搜索树操作 (查找、插入和删除), 还涵盖了动态集合操作 (如前继和后继等) 和顺序统计操作 (如选择和求
秩等).
本文第 1 节是对相关工作进行介绍. 第 2 节详细介绍动态顺序统计树类结构的函数式建模框架. 第 3 节介绍
动态顺序统计树类结构的 Isabelle 自动化验证框架. 第 4 节将建模框架实例化为不同的具体搜索树结构, 并借助自
动化验证框架对其正确性进行自动验证. 第 5 节进一步讨论自动化验证框架的适用范围和效果对比. 第 6 节是对
全文的总结以及未来的工作展望.

1 相关工作

在搜索树类结构的算法领域, 研究者们致力于开发高效、可扩展且具有良好性能的算法, 以应对不同应用场
景下的挑战. 在本节中, 将介绍与搜索树类结构相关的研究, 主要从具体搜索树结构的建模及验证, 和搜索树类结
构的建模及验证框架两个方面进行介绍.
在具体搜索树结构建模及验证的发展中, 研究者们提出了各种各样的算法, 并通过手工推导或交互式机械化
验证的方式确保正确性. 文献 [9] 将快速排序思想成功应用到二叉搜索树中, 形式化定义了随机二叉搜索树的结
构, 并对其高度、结构不变式以及对搜索和插入操作的影响进行了讨论和验证. 文献 [10] 验证了 Braun 树基本操
作的正确性, 并验证了从列表到 Braun 树的线性时间转换函数, 为 Braun 树的进一步研究和应用提供了新的思路.
文献 [11] 提出了根平衡树的概念, 并在函数式环境中验证了其摊销复杂度, 同时提供了无对数代码的实现以及与
传统树结构的竞争性评估. 文献 [12] 提供了 splay 树的可执行结构, 并验证了其基本性质及摊销复杂度. 文献 [13]
提出并验证了 2−3 手指树结构及性质, 支持在均摊的恒定时间内访问列表的两端. 文献 [14] 确定了原始权重平衡
树算法中插入和删除旋转参数的确切有效范围, 并使用生成反例树的有效算法证明了其完备性. 文献 [15] 利用集
合的抽象数据类型高效实现并证明了 van Emde Boas 树相关函数的正确性, 并从证明的可信基础中消除了人工定
义的时序函数. 总之, 尽管研究者们在具体搜索树结构的建模及验证方面取得了显著进展, 但现有研究主要针对特
定的单一算法程序进行建模及验证, 缺乏成熟且可靠的通用建模及验证模式, 可复用性较低.
在搜索树类结构的建模及验证框架方面, 文献 [16] 通过探究二叉搜索树类算法之间共性, 建立了二叉搜索树
类算法的函数式建模框架, 用区域 (locale) 刻画二叉搜索树类结构插入和删除高阶泛化函数, 在对具体的二叉搜索
树变体结构 (如 AVL 树、RBs 等) 进行建模时, 可进行相应的实例化, 并对其附加性质的验证进行细化, 给出了具
体化的验证方案. 不过, 该建模框架未对多叉的搜索树类结构进行讨论, 且其验证方案仍然停留在交互式机械化验
证的层面, 自动化水平较低. 文献 [5] 提出了一种用于验证搜索树类结构功能正确性的自动化验证框架, 借助一个
小型引理库, 对不同搜索树结构的功能正确性进行自动化证明, 展示了该框架的有效性和广泛适用性, 并讨论了从
集合到映射的泛化过程. 然而, 该框架仅对搜索树类结构的查找、插入和删除这 3 种基本操作进行了自动化验证,

不适用于动态集合和顺序统计量相关算法.
本文提出了一个针对动态顺序统计树类结构的 Isabelle 函数式建模和自动化验证框架, 涵盖了动态集合、顺
序统计和搜索树等 10 种常用操作, 构建了完善的验证引理库, 并给出了具体的验证方法. 进一步选取了不平衡的
二叉搜索树、平衡的二叉搜索树 (红黑树) 和平衡的多叉搜索树 (2−3 树) 为实例, 检验了建模和自动化验证框架