软件学报

作者：左正康，刘增鑫，柯雨含，游珍，王昌晶

单位：左正康，江西师范大学 计算机信息工程学院, 江西 南昌 33002211,刘增鑫，江西师范大学 计算机信息工程学院, 江西 南昌 33002202,柯雨含，江西师范大学 计算机信息工程学院, 江西 南昌 33002203,游珍，江西师范大学 计算机信息工程学院, 江西 南昌 330022;网络化支撑软件国家国际科技合作基地(江西师范大学), 江西 南昌 33002204,王昌晶，江西师范大学 计算机信息工程学院, 江西 南昌 33002205

关键词：动态顺序统计树;搜索树;函数式建模;自动化验证;Isabelle定理证明器

基金：国家自然科学基金(62462036, 62462037); 江西省自然科学基金面上项目(20232BAB202010, 20212BAB202018); 江西省教育厅科技重点项目(GJJ210307, GJJ2200302, GJJ210333); 江西省主要学科学术与技术带头人培养项目(20232BCJ22013)

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

来源：2025年第8期

《软件学报》期刊编辑部

查看软件学报杂志2025年第8期