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

3532 软件学报 2025 年第 36 卷第 8 期

(exemplified by red-black trees), and balanced multi-way search trees (exemplified by 2–3 trees) are selected as instantiated cases for
demonstration. With the help of the automated verification framework, multiple instantiated cases can be automatically verified by simply
using induction and invoking the auto method once, or by using the try command. This provides a reference for automated verification of
functional and structural correctness in complex data structure algorithms.
Key words: dynamic order statistic tree; search tree; functional modeling; automated verification; Isabelle theorem prover

动态顺序统计树结构是一类融合了动态集合、顺序统计量以及搜索树结构特性的数据结构. 除了基本的动态
)
(
集合操作外, 还支持快速的数据检索、高效的插入和删除, 且能在 O logn 时间内实现顺序统计操作 [1] . 其中, 动态
集合是指由算法操作的数据集在整个过程中能增大、缩小或发生其他变化 [2] . 顺序统计量是指在一组统计样本中
按照大小顺序排列后的特定位置的值, 其对应的顺序统计操作主要包括两种, 一种是在一组数据中找到第 k 小 (或
第 k 大) 元素的选择操作, 另一种是给出一个指定元素在数据集的全序位置的求秩操作 [3,4] . 动态顺序统计树类结
构能在具体的搜索树结构中通过扩充树的大小信息实现, 广泛应用于数据库系统、内存管理和文件管理等领域.
然而, 当前搜索树类结构的相关工作侧重讨论结构特性, 如平衡性, 而忽略了功能正确性的重要性 [5] . 这可能使得
该结构及对应算法出现未预料到的错误, 增加了后期调试和维护的难度. 因此, 对动态顺序统计树等搜索树类结构
进行功能正确性验证, 是确保算法可靠性、安全性和有效性的重要措施.
在建模方面, 建立函数式建模框架可以提供一个结构化的开发环境, 能将数据结构对应的算法函数功能清晰
地呈现出来, 有助于开发人员更快速、更高效地进行开发工作. 而在对动态顺序统计树类结构进行函数式建模的
过程中, 需要综合考虑选用实例化的搜索树结构、具体的应用场景以及它们在实际应用中的功能. 这就意味着需
要在不同的复杂结构中找到其中的共性, 制定统一的建模策略和操作模式, 需要更多的创造性思维和技巧. 在验证
方面, 形式化定理证明是保证程序正确性的有效途径, Isabelle/HOL [6,7] 是当前被广泛使用的定理证明器. 然而, 大多
数在 Isabelle 上对搜索树类结构的验证, 都是针对具体的算法程序进行交互式机械化验证. 一方面, 其验证的可复
用性较低, 验证对象或场景发生变化时需要重新设计验证方案. 另一方面, 其自动化的程度低, 需要更多的人为干
预, 验证过程需要耗费大量时间和人力成本. 建立函数式验证框架, 构建统一的验证模式, 引入自动验证技术, 可以
在保证验证准确性的前提下, 尽可能地减少人为参与. 因此, 研究函数式建模框架和自动化验证框架可以简化建模
和验证流程, 有效地减少人工干预的需求, 从而节省开发人员验证代码的时间和成本.
文献 [5,8] 分别介绍了在 Isabelle 中实现自动验证的两种方式: 一是通过简单的归纳法或分情况讨论, 然后调
[8]
用一次 auto 方法得到自动化证明 [5] ; 二是通过 try 命令, 调用 Sledgehammer 等组件将当前命题翻译为一阶逻辑,
然后搜索引理库中的引理探索证明路径, 自动生成证明. 两种方式均采用一组固定的基本引理以及关于辅助函数
的引理作为参数. 这意味着在 Isabelle 中实现自动验证还需要设计通用的验证引理库. 一方面, 引理库整体的设计
思想应注重简化问题复杂性, 将复杂问题逐步分解为更小的子问题, 使自动化证明组件能够高效处理. 另一方面,
引理库中辅助引理的设计应考虑可靠性和通用性, 保证辅助引理正确性的同时, 确保其能应对不同场景下的证明
需求.
本文旨在 Isabelle 中设计动态顺序统计树类结构的函数式建模和自动化验证框架, 并将该建模框架实例化为
不同的搜索树类结构, 借助自动化验证框架自动验证其中函数的功能正确性. 本文的技术路线图如图 1 所示. 由
此, 本文工作的主要贡献点总结如下.

函数式 Isabelle 实例化案例
建模框架 自动化验证框架

函数式定义 datatype 'a dost=Leaf | Node nat “a dost” 'a “'a dost” 列表辅助函数 验证引理库 不平衡的二叉搜索树
建模策略 自顶向下查找, 自底向上调整 平衡的二叉搜索树: 红黑树
不变式 definition “invar t≡inv ST t ^ inv size t ^ inv prop t” ... ... 平衡的多叉搜索树: 2−3 树

图 1 技术路线图