| 摘要: |
| 动态顺序统计树结构是一类融合了动态集合、顺序统计量以及搜索树结构特性的数据结构, 支持高效的数据检索操作, 广泛应用于数据库系统、内存管理和文件管理等领域. 然而, 当前工作侧重讨论结构不变性, 如平衡性, 而忽略了功能正确性的讨论. 且现有研究方法主要针对具体的算法程序进行手工推导或交互式机械化验证, 缺乏成熟且可靠的通用验证模式, 自动化水平较低. 为此, 设计动态顺序统计搜索树类结构的Isabelle函数式建模框架和自动化验证框架, 构建经过验证的通用验证引理库, 可以节省开发人员验证代码的时间和成本. 基于函数式建模框架, 选取不平衡的二叉搜索树、平衡的二叉搜索树(以红黑树为代表)和平衡的多叉搜索树(以2-3树为代表)作为实例化的案例来展示. 借助自动验证框架, 多个实例化案例可自动验证, 仅需要使用归纳法并调用一次auto方法或使用try命令即可, 为复杂数据结构算法功能和结构正确性的自动化验证提供了参考. |
| 关键词: 动态顺序统计树 搜索树 函数式建模 自动化验证 Isabelle定理证明器 |
| DOI：10.13328/j.cnki.jos.007349 |
| 分类号: |
| 基金项目:国家自然科学基金(62462036, 62462037); 江西省自然科学基金面上项目(20232BAB202010, 20212BAB202018); 江西省教育厅科技重点项目(GJJ210307, GJJ2200302, GJJ210333); 江西省主要学科学术与技术带头人培养项目(20232BCJ22013) |
|
| Functional Modeling and Automatic Verification of Dynamic Order Statistic Tree Structures |
|
ZUO Zheng-Kang1, LIU Zeng-Xin1, KE Yu-Han1, YOU Zhen1,2, WANG Chang-Jing1
|
|
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 (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 |
