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

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

在验证其结构正确性 (定理 11) 之前, 可先验证其维持平衡的调整函数 ( bal_ fun 等) 的结构正确性. 进一步,
1
可将不变式 invar 拆分为 inv ST 、 inv size 和 inv prop (定义见第 2.3 节) 分别进行验证, 以降低整体的验证复杂度. 对于
拆分后得到的细化引理, 本文的自动化验证框架可以适用, 提升整体的自动化验证水平.
对于函数 delete 的结构正确性验证 (定理 12), 可同样按照上述拆分方案对定理进行拆分, 以达到简化目标定
理的目的, 进一步借助自动化验证框架自动验证拆分后的细化引理, 提高自动化水平.

4 建模和自动化验证实例

为了评估动态顺序统计树类结构函数式建模和 Isabelle 自动化验证框架的有效性, 本文选取了不平衡的二叉
搜索树、平衡的二叉搜索树 (红黑树) 和平衡的多叉搜索树 (2−3 树) 为实例, 从不同维度检验框架的适用性.

4.1 实例化为不平衡的二叉搜索树
不平衡的二叉搜索树即为最基础的二叉搜索树, 只有搜索树性质而没有平衡操作, 不带有附加性质. 基于动态
顺序统计树类结构的函数式定义 (第 2.1 节) 和不变式 (第 2.3 节), 将 dost syn 实例化为 dost bst , 不变式 invar 实例化
为 invar bst , 不平衡的动态顺序统计二叉搜索树的结构和不变式定义可表示如下.

type_synonym a dost bst = “ a dost”//不平衡的二叉搜索树的结构定义
′
′
definition “invar bst t ≡ inv ST t ∧ inv size t”//不平衡的二叉搜索树的不变式定义
不平衡的二叉搜索树的正确性定理包括功能正确性定理和结构正确性定理, 功能正确性定理表示各个函数操
作能够正确实现预想的功能, 结构正确性定理表示执行修改类函数操作前后不变式 invar bst 成立.

dost bst 的功能正确性验证
4.1.1
(1) 函数式建模
基于第 2.2 节中的函数式建模策略, 可以设计不平衡的二叉搜索树 dost bst 的具体函数. 以选择和求秩函数为
例, 可分别实例化为 dost bst _select 和 dost bst _rank. 选择函数 dost bst _select 用于查找树 dost bst 中第 k 小的元素, 求秩
dost bst _rank 用于计算给定元素 x 的排名, 即比它小的元素的数量. 动态顺序统计树类结构在每个节点处维护
函数
了树的大小值, 即以当前节点为根的子树中的节点数量, 该值可以通过函数 tsize (定义见第 2.1 节) 获取. 则选择函
dost bst _select 可以通过比较给定值 dost bst _rank 在查找
数 k 与 tsize l+1 来确定查找路径, 并递归执行, 而求秩函数
过程中递归累加比 x 小的节点数量 (值为 tsize l+1), 两个函数的实现过程如图 17 所示.

比较 k 和 tsize l+1 比较 x 和 a
等于 等于
小于 大于 小于 大于
a a
修改 k 为 k−(tsize l+1) 累加 tsize l+1
a.size a.size

la ra la ra
l.size r.size l.size r.size

t 1 t 2 t 3 t 4 t 1 t 2 t 3 t 4
左子树 l 右子树 r 左子树 l 右子树 r
(a) 选择函数 dost bst _select (b) 求秩函数 dost bst _rank
dost bst _rank 的实现过程
图 17 选择函数 dost bst _select 和求秩函数

基于第 2.2 节中的高阶复合函数, 可对函数 dost bst _select 和 dost bst _rank 进行函数式建模, 如下所示. 其中,
let n = tsize l+1 为查找过程前的前置操作 (preOperation), cmp k n 和 cmp x a 分别对应两个函数的比较大小操作
(compOperation), 通过比较之后的结果 (LT、GT 和 EQ) 确定查找路径.