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

软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn
2025,36(8):3531−3553 [doi: 10.13328/j.cnki.jos.007349] [CSTR: 32375.14.jos.007349] http://www.jos.org.cn
©中国科学院软件研究所版权所有. Tel: +86-10-62562563

*
动态顺序统计树类结构的函数式建模及其自动化验证

左正康 1 , 刘增鑫 1 , 柯雨含 1 , 游 珍 1,2 , 王昌晶 1

1
(江西师范大学 计算机信息工程学院, 江西 南昌 330022)
(网络化支撑软件国家国际科技合作基地 (江西师范大学), 江西 南昌 330022)
2
通信作者: 王昌晶, E-mail: wcj@jxnu.edu.cn

摘 要: 动态顺序统计树结构是一类融合了动态集合、顺序统计量以及搜索树结构特性的数据结构, 支持高效的
数据检索操作, 广泛应用于数据库系统、内存管理和文件管理等领域. 然而, 当前工作侧重讨论结构不变性, 如平
衡性, 而忽略了功能正确性的讨论. 且现有研究方法主要针对具体的算法程序进行手工推导或交互式机械化验证,
缺乏成熟且可靠的通用验证模式, 自动化水平较低. 为此, 设计动态顺序统计搜索树类结构的 Isabelle 函数式建模
框架和自动化验证框架, 构建经过验证的通用验证引理库, 可以节省开发人员验证代码的时间和成本. 基于函数式
建模框架, 选取不平衡的二叉搜索树、平衡的二叉搜索树 (以红黑树为代表) 和平衡的多叉搜索树 (以 2−3 树为代
表) 作为实例化的案例来展示. 借助自动验证框架, 多个实例化案例可自动验证, 仅需要使用归纳法并调用一次
auto 方法或使用 try 命令即可, 为复杂数据结构算法功能和结构正确性的自动化验证提供了参考.
关键词: 动态顺序统计树; 搜索树; 函数式建模; 自动化验证; Isabelle 定理证明器
中图法分类号: TP311

中文引用格式: 左正康, 刘增鑫, 柯雨含, 游珍, 王昌晶. 动态顺序统计树类结构的函数式建模及其自动化验证. 软件学报, 2025,
36(8): 3531–3553. http://www.jos.org.cn/1000-9825/7349.htm
英文引用格式: Zuo ZK, Liu ZX, Ke YH, You Z, Wang CJ. Functional Modeling and Automatic Verification of Dynamic Order
Statistic Tree Structures. Ruan Jian Xue Bao/Journal of Software, 2025, 36(8): 3531–3553 (in Chinese). http://www.jos.org.cn/1000-
9825/7349.htm

Functional Modeling and Automatic Verification of Dynamic Order Statistic Tree Structures
1
1
1,2
1
ZUO Zheng-Kang , LIU Zeng-Xin , KE Yu-Han , YOU Zhen , WANG Chang-Jing 1
1
(School of Computer Information Engineering, Jiangxi Normal University, Nanchang 330022, China)
2
(National-level International S & T Cooperation Base of Networked Supporting Software (Jiangxi Normal University), Nanchang 330022,
China)
Abstract: Dynamic order statistic tree structures are a type of data structure that integrates the features of dynamic sets, order statistics,
and search tree structures, supporting efficient data retrieval operations. These structures are widely used in fields such as database
systems, memory management, and file management. However, current research primarily focuses on structural invariants, such as balance,
while neglecting discussions on functional correctness. In addition, existing research methods mainly involve manual derivation or
interactive mechanized verification for specific algorithms, lacking mature and reliable general verification frameworks and exhibiting a
low level of automation. To address this, a functional modeling and automated verification framework for dynamic order statistic search
tree structures, based on Isabelle, has been designed. A verified general lemma library is established to reduce the time and cost of code
verification for developers. Using this functional modeling framework, unbalanced binary search trees, balanced binary search trees

* 基金项目: 国家自然科学基金 (62462036, 62462037); 江西省自然科学基金面上项目 (20232BAB202010, 20212BAB202018); 江西省教
育厅科技重点项目 (GJJ210307, GJJ2200302, GJJ210333); 江西省主要学科学术与技术带头人培养项目 (20232BCJ22013)
本文由“形式化方法与应用”专题特约编辑陈明帅研究员、田聪教授、熊英飞副教授推荐.
收稿时间: 2024-08-26; 修改时间: 2024-10-14; 采用时间: 2024-11-26; jos 在线出版时间: 2024-12-10
CNKI 网络首发时间: 2025-04-03