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

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

(5) 从任一节点到其每个叶子的所有路径都包含相同数目的黑色节点, 用 inv height 来表示这一性质.
颜色性质不变式 inv rb 表示红黑树需满足上述性质. 基于第 2.3 节的不变式, 将 invar 实例化为 invar rbt , 将 inv prop
实例化为 inv rb , 可定义树 dost rbt 的不变式, 如下所示.

//红黑树dost rbt 的颜色性质不变式
definition “inv rb t ≡ inv color t ∧inv height t ∧ dost rbt _color t = Black”
//红黑树dost rbt 的不变式
definition “invar rbt t ≡ inv ST t ∧ inv size t ∧inv rb t”

以选择和求秩函数为例, 基于第 2.2 节中的高阶复合函数可对其进行函数式建模, 实现思路与第 4.1.1 节类似,
限于篇幅略.
对于红黑树中函数功能正确性的验证, 基于第 3.3 节给出的基于引理库的自动化验证策略, 同样能够得到自
动化验证. 第 3.3.1 节中给出的验证引理库均是通用的, 因此同样使用验证引理库中的 list_sel 和 list_rank 验证引
理集, 且只需要使用归纳法并调用一次 auto 方法即可完成选择和求秩函数的自动化验证, 如图 20 所示.

选择函数 dost rbt _select
的正确性定理
归纳法
auto 方法

list_sel 验证引理集 辅助函数的正确性引理
求秩函数 dost bst _rank
的正确性定理
归纳法
auto 方法

list_rank 验证引理集 辅助函数的正确性引理
图 20 函数 dost rbt _select 和 dost rbt _rank 的功能正确性自动化验证过程

对于红黑树中函数结构正确性的验证, 实现思路与第 4.1.2 节类似. 借助第 3.3.2 节的拆分方案, 将不变式
invar rbt 拆分为 inv ST 、 inv size 和 inv rb 等, 得到细化引理. 对于细化引理, 本文的自动化验证框架同样可以自动化
验证.

4.3 实例化为平衡的多叉搜索树
2−3 树是一种特殊的 B-树 [23] 结构, 常用于文件系统和数据库系统中, 动态顺序统计 2−3 树可用于实现目录结
构管理, 快速检索相应数据. 2−3 树的每个非叶节点都有 2 个或 3 个子树, 而且所有叶子节点都在同一层上. 本节
以 2−3 树作为平衡的多叉搜索树的典型案例进行讨论. 基于第 2.1 节中动态顺序统计树类结构的函数式定义, 可
将其结构定义如下.

′
datatype a dost 23 = Leaf|
′ ′ ′
Node2 nat “ a dost 23 ” a “ a dost 23 ”|
′
′
′
′
′
Node3 nat “ a dost 23 ” a “ a dost 23 ” a “ a dost 23 ”
对于 2−3 树这类包含多个子树的多叉搜索树, 其操作函数的实现思路与二叉搜索树是一致的, 只需要额外补
充对多子树节点 (Node3) 的处理. 将函数 tsize 更新为函数 dost 23 _size, 只需要额外添加对 Node3 节点的处理操作
即可. 如下展示了不变式 inv size 额外添加的处理操作, 其中函数 size3 用于计算 Node3 节点对应树的大小值.