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

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

a find (λy. y>x_pred) lst=Some x
sucd
pred
t 1 验证 list_pred 正确性
x
max min
b c 查找节点 x 的位置
list_pred
列表
t 2 t 3 t 4 t 5
模拟
... x_pred x x_sucd ...
a
list_sucd
查找节点x的位置 x_pred t 2

pred 验证 list_sucd 正确性
t 1 x_sucd
sucd
x find (λy. y>x) lst=Some x_sucd

图 6 list_pred 和 list_sucd 的模拟操作及验证

如果有序列表 lst 中第 1 个大于元素 x 的元素是 y, 那么元素 x 是元素 y 的前继元素, 元素 y 则是元素 x 的后
继元素. 在有序列表中实现 list_pred 和 list_sucd 只需要先查找节点 x 的位置, 然后找到节点 x 前一个位置的元素
和后一个位置的元素即可, 涉及的情况较少. 因此, 用 list_pred 和 list_sucd 来模拟 pred 和 sucd 函数操作, 可以降
低问题的复杂度, 便于自动化证明组件处理.
Isabelle 中的 find 函数可以按条件查询列表中满足条件的第 1 个元素. 借助 find 函数和 λ 函数组合可验证
list_pred 和 list_sucd 的正确性.
(3) list_sel 和 list_rank: 前者表示给定一个具体数值 k, 查找有序列表中第 k 小的元素. 后者则表示给定一个元
素 x, 计算该元素为有序列表中的第几小的元素.
如图 7 所示, 选择函数 select 实现在动态顺序统计树类结构中查找具有给定次序的元素的功能, 即查找第 k
小的元素. select 函数功能的实现依赖于树的节点大小信息. 通过比较给定值 k 与左子树的大小信息, 来判断往树
的左子树或者右子树中查找元素. 如果往右子树中查找元素, 则需将 k 的值依次减去左子树的大小值和根节点单
个节点的大小值 (值为 1), 再将得出的值作为新一轮递归的输入. 求秩函数 rank 实现确定一个元素的次序的功能,
即给定一个元素 x, 求该元素是树中第几小的元素. 根据目标节点与当前根节点的大小关系, 判断查找路径的方向,
同时累计树的大小信息, 表示比目标节点元素键值更小的节点个数. 当找到目标元素 x 后, 累计的树的大小信息为
最终的结果. 两个函数的实现都需要在常规的递归查找过程中添加额外的处理树的大小信息操作, 增加了额外的
证明义务. 需要将问题简化, 才能实现自动化验证.

select rank lst!k=x (给定k)
根据给定 k 值查找 根据元素 x 键值査找
c 验证 list_sel 正确性
list_sel 根据给定 k 值顺序查找
a e 列表模拟
... a b ... c ... d e ...
t 1 t 6
b d list_rank 根据给定元素 x 顺序査找
验证 list_rank 正确性
t 2 t 3 t 4 t 5
lst!k=x (给定x)
图 7 list_sel 和 list_rank 的模拟操作及验证