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

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

对于多叉型动态顺序统计树类结构, 可按照相似的思路对其结构进行递归定义. 以每个非叶子节点都有 2 个
或 3 个子节点的 2−3 树 [1] 为例, 叶子节点和 2 个子节点的情况可以沿用二叉型动态顺序统计树类结构的 Leaf 和
Node 定义. 而对于 3 个节点的情况, 可按照定义 2 个子节点情况的相似思路, 将其定义为<n, l, a, m, b, r>. 其中, n
同样表示树的大小信息, a 和 b 表示根节点上的两个关键字信息, l、m 和 r 分别表示左、中和右子树信息. 其对应
的操作函数只需要按照同样的思路, 额外处理 3 个节点的情况即可. 本文的第 4 节给出了多叉型结构的典型代表
2−3 树的具体建模实现思路. 在本文的剩余部分, 将主要以二叉型的动态顺序统计树类结构为基准进行阐述. 对于
多叉型的结构, 在实际建模时可遵循类似的思路补充额外的多节点情况.

2.2 动态顺序统计树类结构的函数式建模策略
动态顺序统计树类结构可以在搜索树结构中扩充树的大小信息实现, 因此其仍保留了搜索树性质. 结合树形
结构来看, 搜索树性质可概括为: 左子树的节点键值均小于根节点, 右子树的节点键值均大于根节点. 基于搜索树
的这一性质, 本文提出了标准化、统一的函数式建模策略, 即自顶向下查找, 自底向上调整, 如图 2 所示.

a a
查找策略 调整策略
b t 4 b t 4
执行修改类函数操作后
c c
t 1 t 1

t 2 t 3 t 2 t 3
图 2 统一的函数式建模策略

对于不改变树中节点信息的函数操作, 统称为检索类函数, 如 isin、select 等, 采取查找策略. 检索类函数操作
的核心在于找到相应的节点信息. 根据查找策略, 在寻找节点时, 需要从根节点出发, 根据根节点与目标节点的关
键字大小关系, 选择向左或向右的路径, 自顶向下递归地在其子树中寻找目标节点. 在寻找的过程中, 可以根据需
要执行一些前置处理操作, 如汇总树的大小信息, 以满足不同函数的实现需求. 在寻找到目标节点的位置后, 根据
函数所需实现的功能处理最后的信息并返回最终的结果.
对于会改变树中节点信息的函数操作, 统称为修改类函数, 如 insert、delete 等, 结合使用查找策略和调整策
略. 修改类函数操作的核心在于调整整棵树, 以维持整体的平衡性. 利用查找策略, 可以找到目标节点的位置. 在找
到目标节点的位置之后, 在对其进行处理时, 可能会破坏树的整体平衡性. 此时, 需要借助调整策略对树的整体进
行调整. 由于修改类函数并未对查找路径以外的节点位置进行操作, 所以在调整过程中只需对查找路径上的节点
进行调整操作即可. 根据调整策略, 在处理完最后的信息后, 还需沿原路径返回并执行相应的调整操作. 换言之, 调
整策略从目标节点的位置出发, 自底向上地执行调整操作, 调整到根节点时结束, 返回调整后得到的树.
为了方便叙述, 在本节中将建模策略分成了两步操作. 实际上, 利用递归的特性, 这两步操作在函数式建模中
可以用一步递归完成. 这一点在后文的具体建模中会有更清晰的体现.
根据函数式建模策略, 可以建立动态顺序统计树类结构相关操作的高阶复合函数, 如下所示.

′
fun < ∗ funcName∗ >:: “ < ∗targetType∗ >⇒ a dost ⇒< ∗resultType∗ > ” where
[ ]
“ < ∗ funcName∗ > x Lea f = ∗ad justLea f∗ < ∗resultLea f∗ > ”|
“ < ∗ funcName∗ > x (Node n l a r) =
([∗ preOperation∗] case < ∗compOperation∗ > o f
[ ]
LT ⇒ ∗ad justLT∗ < ∗resultLT∗ > |
[ ]
GT ⇒ ∗ad justGT∗ < ∗resultGT∗ > |
[ ]
EQ ⇒ ∗ad justEQ∗ < ∗resultEQ∗ >)”