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

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

表 1 验证方法的对比

是否为 适用动态集合操作 适用顺序统计操作 适用搜索树操作
验证方法
自动化验证 最大值 最小值 前继 后继 树的大小 选择 求秩 查找 插入 删除
交互式 [9−16] ○ ● ● ● ● ● ● ● ● ● ●
文献[5] ● ○ ○ ○ ○ ○ ○ ○ ● ● ●
本文 ● ● ● ● ● ● ● ● ● ● ●

select 函数的正确性验证 select 函数的正确性验证
需 前 不需要额外构造前置引理
额 置
外 引
构 理
造
rank 函数的正确性验证
rank 函数的正确性验证
需 前 不需要额外构造前置引理
额 置
外 引
构 理
造

(a) 交互式验证方法 (b) 本文自动化验证框架
图 22 交互式验证方法与本文自动化验证框架的验证过程对比

表 2 给出了两种方法的前置引理数和验证代码行数的对比. 具体而言, 对于函数 select 和函数 rank 的正确性
验证, 交互式验证方法分别需要构造 10 条、15 条前置引理, 对应 58 行、81 行验证代码. 而使用本文的自动化验
证框架, 无需构造前置引理, 验证代码行数均精简至 4 行.

表 2 前置引理数和验证代码行数的对比

验证方法 交互式验证方法 本文自动化验证框架
前置引理条数 10 0
select函数的正确性验证
验证代码行数 58 4
前置引理条数 15 0
rank函数的正确性验证
验证代码行数 81 4

dost rbt 中实现, 交互式验证方法需重新构造前置引理, 且由于红黑树
当应用场景发生改变时, 如改为在红黑树
dost rbt 结构的复杂程度远大于不平衡的二叉搜索树 dost bst , 因此前置引理的构造将更为复杂且繁琐. 而本文所提的
自动化验证框架具备良好的通用性, 依旧可以处理. 如图 23 所示, 对于红黑树 dost rbt 中 select 和 rank 函数的验证,
本文的自动化验证框架同样不需要构造前置引理, 得到自动验证, 代码行数也仅为 4 行.

select 函数的正确性验证 0 条前置引理, 4 行验证代码 select 函数的正确性验证 0 条前置引理, 4 行验证代码

rank 函数的正确性验证 0 条前置引理, 4 行验证代码 rank 函数的正确性验证 0 条前置引理, 4 行验证代码

(a) 不平衡的二叉搜索树 dost bst (b) 红黑树 dost rbt
图 23 自动化验证框架的通用性