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

3538 软件学报 2025 年第 36 卷第 8 期

过函数 inorder 来实现.
对于 Abs 同态性的验证, 一方面, 需要额外定义列表辅助函数模拟动态顺序统计树函数操作, 并保证列表辅助
函数的正确性 (第 3.2 节); 另一方面, 需要针对列表辅助函数设计通用的验证引理集, 形成通用的验证引理库, 以
应对不同场景下的需求 (第 3.3 节).

3.2 自动化验证框架的列表辅助函数
动态顺序统计树类结构的种类繁多, 但每个具体的动态顺序统计树都至少提供 10 种操作. 我们在 Isabelle 中
用区域 (locale) 刻画了这些基本操作, 如图 4 所示. 其中, 't 类型可以用'a dost 或 ′ a dost syn 代替. 对于树为空的情况
(empty), 其正确性证明是简单的, 本文将忽略对其的讨论.

最大值
动态集合 最小值
相关操作 前继
后继
动态顺序统计
树的大小
顺序统计 树类结构的
操作 选择
求秩 10 种操作
查找
搜索树
操作 插入
删除
图 4 动态顺序统计树类结构的 10 种操作

对于函数 tsize, 在第 2 节中讨论了其特殊实现方式. 基于这种实现方式及建模策略, 函数 tsize 的正确性验证
也变得更为简单, 只需要通过归纳法并调用一次 auto 方法即可得证, 无需构造额外的列表辅助函数及引理集.
而对于其他操作, 我们设计相应的列表辅助函数进行模拟, 以达到简化问题的目的. 借助 Isabelle 源码库中已
经得到验证的函数及其组合, 可以验证列表辅助函数的正确性. 具体如下.
(1) list_max 和 list_min: 查找有序列表中的最大值和最小值.
如图 5 所示, 对于动态顺序统计树类结构中求最大值和最小值的函数 max 和 min, 设计了 list_max 和 list_min
模拟. 其中, list_max 通过遍历有序列表至表尾, 获取最大值, 而 list_min 则通过提取有序列表的表头元素, 获取最
小值. 这两个函数的正确性证明可以分别借助 Isabelle 集合 (set) 中的 Max 和 Min 函数辅助验证, 使用归纳法并调
用一次 auto 方法就能得到证明.

d list_max Max
min max set
列表模拟 验证正确性
b e a b c d e f a b d
c f e
a c f list_min
Min
图 5 list_max 和 list_min 的模拟操作及验证

(2) list_pred 和 list_sucd: 查找在有序列表中, 指定元素的前继和后继元素.
一个元素的前继元素是指树中小于该元素的最大元素, 后继元素则是指大于该元素的最小元素. 在动态顺序
统计树类结构中, 求前继元素的 pred 函数和求后继元素的 sucd 函数的实现均依赖于搜索树性质.
如图 6 所示, 以 pred 函数为例, 一般来说, 元素 x 左子树中的最大元素即为元素 x 的前继元素. 若元素 x 的左
子树为空, 则需要向上查找其祖先节点以确定前继元素. 结合树形结构来看, 即沿着元素 x 的父节点向上查找, 直
到找到一个元素 y, 元素 y 对应结点的右子树包含元素 x. 而 sucd 函数的实现思路则相反, 找元素 x 右子树中的最
小元素或找祖先节点中左子树含有元素 x 的节点元素, 即为元素 x 的后继元素. 在实际的建模场景中, 两个函数的
实现均需考虑较多的情况, 其正确性验证较为复杂, 常规的自动化证明组件难以应付.