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

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

在有序列表中 list_sel 和 list_rank 函数的实现均可通过顺序查找完成. 在查找过程中, list_sel 函数通过递减给
定的 k 值查找, 当 k 值为 0 时, 得到第 k 小的元素; list_rank 函数根据元素 x 的键值查找, 找到元素 x 后返回累计遍
历的元素个数. 两个函数操作都是线性的, 简化了复杂操作, 自动化证明组件可以应付.
Isabelle 中的 nth 函数 (简写为符号!) 可以获取列表中的指定索引位置的元素. 利用这个函数, 可以验证 list_sel
和 list_rank 函数的正确性.
(4) list_isin、list_ins 和 list_del: 分别表示在有序列表中查找、插入和删除元素.
如图 8 所示, 动态顺序统计树类结构中的 isin、insert 和 delete 函数的实现都是需要先定位到元素 x 的位置.
isin 函数在查找后直接返回结果即可. insert 和 delete 函数则需要在查找之后执行相应的插入和删除操作. 由于插
入和删除操作可能会改变树的节点大小信息, 且会破坏树的平衡, 因此需要额外的调整操作来维持平衡, 即维持不
变式成立. 而不同的动态顺序统计树结构所对应的调整操作是不同的, 且调整操作需要考虑到不同的不平衡情况,
要处理的情况繁多且复杂, 直接用自动化证明组件得到自动验证是不实际的.

list_isin 查找 x 以判断其是否在列表中

set
... a x b ... x ∈ a x b
...
a
调整 list_ins 查找 a<x<b 的位置
列表 验证
t 1 c ... a b ... a b
查找 模拟 正确性 x
...
t 3 x 插入 x
b
list_del 查找 x 的位置
a b
... a x b ...
t 2 x − x
...
೷Ԣ x
图 8 list_isin、list_ins 和 list_del 的模拟操作及验证

对于有序列表, list_isin、list_ins 和 list_del 函数需要递归查找元素 x 的位置, 然后执行相应的查找、插入或
删除操作即可. 而由于列表本身是有序的, 故在插入和删除操作之后, 通过简单地合并列表, 能够保持有序性. 用
这 3 个函数模拟动态顺序统计树类结构的查找、插入和删除操作, 可以将其在复杂的调整操作中抽象出来, 专注
于查找、插入和删除的功能实现, 将问题简化.
list_isin、list_ins 和 list_del 函数的正确性证明可以借助集合中的属于 (∈)、并集 (∪) 和差集 (–) 来辅助验证,
同样可以仅使用归纳法并调用一次 auto 方法证明.

3.3 自动化验证框架的通用验证引理库
通过列表辅助函数模拟动态顺序统计树类结构的 10 种操作, 可以简化问题. 要进一步实现自动化验证, 需借
助列表辅助函数构建通用的验证引理集, 合并 10 种操作对应的验证引理集, 组成验证引理库. 图 9 展示了基于引
理库的自动化验证策略. 对于待证明的定理 T, 一般采用如下方式进行自动化验证.

待证明的定理 T theorem T: invar t ⟹ tree_fun x t = list_fun x (inorder t)
归纳法 apply (induct t arbitrary: x) apply (induction x t rule: tree_fun.induct)
auto 方法 by / apply (auto simp: list_fun_simps fun_defs proven_lemmas split: type.splits)

try 命令 by / apply (metis other_lemmas) by / apply (meson other_lemmas) …

图 9 基于引理库的自动化验证策略