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

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

//树的大小不变式
′
fun inv size :: “ a dost ⇒ bool” where
“inv size <>= True”|
“inv size < n,l,a,r >= (inv size l ∧ inv size r ∧ (size2 l r = n))”

(3) 附加性质不变式 (统称 inv prop ), 这是一个可选项. 当实例化所用到的具体搜索树结构, 需要维持附加性质不
变时 (如颜色等), 加上相应的附加性质.
总而言之, 上述不变式 (1)−(3) 统称为动态顺序统计树类结构的不变式 (简称 invar), 其定义如下.

//动态顺序统计树类结构的不变式
definition “invar t ≡ inv ST t ∧ inv size t ∧ inv prop t”

3 动态顺序统计树类结构的 Isabelle 自动化验证框架

为了更高效地验证动态顺序统计树类结构相关算法函数的正确性, 减少开发人员验证代码的时间和成本, 本
节构建了动态顺序统计树类结构在 Isabelle 中的自动化验证框架, 如图 3 所示. 其设计理念为用列表模拟动态顺序
统计树类结构的 10 种操作, 设计对应的列表辅助函数, 并验证其正确性. 借助列表辅助函数可构建通用的验证引
理集, 合并 10 种操作对应的验证引理集, 组成验证引理库. 基于验证引理库, 动态顺序统计树类结构的 10 种操作
的功能正确性均能实现自动化验证. 第 3.1 节阐述了设计自动化验证框架的理论基础, 第 3.2 节设计并验证了列表
辅助函数, 第 3.3 节构建了通用的验证引理库.

动态顺序统计树类 列表模拟 验证正确性 Isabelle 库的
结构的 10 种操作 列表辅助函数 函数及其组合

构建验证引理集

验证引理库
自动化验证

功能正确性

图 3 动态顺序统计树类结构的自动化验证框架结构

3.1 自动化验证框架的理论基础
实现自动化验证需要简化问题的复杂性, 将复杂的问题逐步拆解为 Isabelle 自动化证明组件能高效处理的形
式. 具体函数的实现可以用同态的抽象函数来代替证明函数的正确性, 这一过程已被证明是正确的 [19] . 使用同态
的抽象函数代替具体函数进行函数式验证, 可以将复杂的问题证明分解为更为简单的形式, 从而简化证明过程 [5] .
对于动态顺序统计树类结构, 在验证其操作算法时, 涉及的情况较多, 自动化证明组件难以应付. 而对于列表这类
线性结构, 其结构的定义契合递归的思想, 对应函数的正确性验证较为简单. 如果能用列表模拟动态顺序统计树的
函数操作, 并将列表作为中介去验证动态顺序统计树的函数正确性, 则可以简化验证过程, 进一步实现自动化验证.
这一方法的关键在于实现将动态顺序统计树映射到列表的映射函数 Abs :: 't ⇒ 'a list. 并验证 Abs 是同态的,
即对于动态顺序统计树类结构中所有需要实现的函数操作 (统称为 tree_fun), 及其列表辅助函数操作 (统称为
list_fun), 满足以下关系 [20] :

invar t ⇒ Abs(tree_ fun(t)) = list_fun(Abs(t)).
函数 inorder 能够将动态顺序统计树中的节点按照中序遍历的顺序映射到列表中. 因此, 映射函数 Abs 可以通