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

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

(1) 归纳法: induct 和 induction 均表示使用归纳法, 前者对单一对象进行归纳, 后者可处理多个对象. arbitrary
表示对除归纳变元 t 以外的自由变元使用全称量化 [7] , rule 明确指定归纳法则. 通过归纳法, 可以将目标定理拆解
为平凡情况和非平凡情况. 平凡情况对应树为空的情况. 非平凡情况则以树为 t 1 、t 2 时命题成立作为前提, 验证树
< n,t 1 ,a,t 2 > 时命题成立, 即对应归纳法“从 n 到 n+1”的思想.
为
(2) auto 方法: Isabelle 中提供的一种自动证明方法. simp 表示应用简化规则, 在这里需添加验证引理库中的辅
助验证引理集, 以简化子目标甚至直接得证. 除此之外, 在子目标中将使用到的函数定义以及辅助函数引理也需添
加其中. 例如, 求前继元素的函数 pred 中调用了 max 函数, 在证明 pred 函数的正确性时, 需要将 max 函数的相关
引理添加其中. 在子目标含有 if、case 等表达式时, split 可以有效地处理这些分支结构, 使 auto 方法可以分别处理
这些分支情况, 从而证明目标.
(3) try 命令: try 命令可调用 Isabelle 中一些用于自动化证明的组件, 如 Sledgehammer 等, 这些组件会给出自
动化证明的结果. 经过上述两步简化操作之后, 一般的定理可以直接得证. 而对于较为复杂的定理, 我们的验证引
理库也可将其简化成足够简单的形式, 借助 try 命令调用自动证明机器能够给出证明的结果.
因此, 验证引理库的构造需覆盖子目标拆解后对应的所有情况, 包括边界情况 (即查找失败) 和找到目标节点
的情况. 结合函数 inorder, 借助第 3.2 节中构建的列表辅助函数可以初步简化目标命题. 为了进一步简化目标, 在
寻找目标节点的过程中, 可以将列表辅助函数中使用到的列表拆成 3 份, 对应树形结构的左子树、根节点和右子
树. 在使用归纳法处理后, 非平凡情况下对应的子目标可能会导致节点数量的增加. 对于情况更为复杂的命题, 为
了进一步提升自动化验证效率, 可以额外添加对这些情况处理的引理.
为了实现动态顺序统计类结构 10 种操作对应定理的自动化验证, 需要根据各操作的逻辑特点设计相应的验
证引理集, 并将这些验证引理集整合成一个统一的验证引理库. 图 10 给出了 10 种操作的逻辑规约, 这些逻辑规约
实际对应需证明的定理, 包括功能正确性定理和结构正确性定理. 功能正确性是指各个函数操作是否能正确执行
预想的功能, 结构正确性是指执行修改类函数操作前后不变式 invar 成立. 对于动态顺序统计树类结构 10 种操作
的功能正确性, 借助第 3.3.1 节给出的 10 种操作对应定理的验证引理集, 可以实现自动化验证. 而对于 insert 和
delete 等修改类函数, 在操作过程中可能会改变树中的节点信息, 破坏树的平衡性. 对于此类函数操作, 除了验证其
功能正确性以外, 还需保证操作前后不变式 invar 成立, 即验证结构正确性. 不同的动态顺序统计树结构有不同的
调整策略维持整体平衡性, 这些调整策略没有统一的构建思路, 差异较大. 因此, 对于结构正确性的验证, 仍需要构
建针对性的引理辅助验证, 基于本文的自动化验证框架不能直接得到自动证明. 不过, 借助第 3.3.2 节中提出的拆
分方案, 拆分不变式 invar 得到细化引理, 以降低目标命题的验证复杂度. 对于拆分后得到的细化引理, 自动化验证
框架可以适用, 提升整体的自动化验证水平.

最大值
动态集合操作 最小值
的正确性定理 前继
后继
10种操作的 树的大小
功能正确性 顺序统计操作 选择
定理 的正确性定理 求秩
查找
搜索树操作
的正确性定理 插入
删除
插入操作的结构正确性
删除操作的结构正确性
图 10 动态顺序统计类结构 10 种操作的逻辑规约

3.3.1 功能正确性验证引理集
定理 1. max 函数. invar t ⇒ t , empty ⇒ max t = list_max (inorder t).
定理 2. min 函数. invar t ⇒ t , empty ⇒ min t = list_min (inorder t).
在动态顺序统计树类结构中, 根据 inv ST 可以推知, 树中最右边、最左边的节点键值分别为树的最大键值、最