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

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

的适用性和有效性.

2 动态顺序统计树类结构的函数式建模框架

为了简化建模流程, 提高代码的可重用性, 本文建立了动态顺序统计树类结构的函数式建模框架, 包括其函数
式定义、建模策略和不变式. 本节讨论了动态顺序统计树类结构的函数式定义, 设计了统一的建模策略. 对于其对
应的选择、求秩等操作, 刻画了通用的高阶复合函数, 并对这些操作算法的不变式进行了规范. 此外, 本节还讨论
了如何在确保整体操作的时间复杂度不变的情况下, 添加额外的高效数据检索操作.

2.1 动态顺序统计树类结构的函数式定义
搜索树类结构允许根据键值进行元素搜索, 能够快速检索、插入和删除元素, 可用于实现动态集合的相关操
作 [17] . 动态顺序统计树类结构可以在搜索树的基础上, 通过添加树的大小信息实现. 对于二叉型动态顺序统计树
类结构, 可以将其数据类型递归地定义为:

′
′
datatype a dost = Lea f|Node nat “ a dost” a “ a dost”,
′
′
其中, 'a 是抽象的, 可以根据需要实例化为不同的具体的类型. Leaf 表示叶子节点 (即节点为空), Node 表示非叶子
节点 (即节点非空), 其 4 个参数分别对应树的大小、左子树、根节点和右子树信息. 通过这种定义方式, 该结构不
仅能实现搜索树类结构原有的基本操作, 还能高效实现动态集合和顺序统计量相关操作.
上述定义的数据类型是抽象的, 在不同的应用场景中, 可以根据需要将其实例化为不同的类型, 得到相对复杂
的结构. 例如, 将其实例化为动态顺序统计红黑树或动态顺序统计 2−3 树等, 可应对实际应用场景. 在实例化到不
同的搜索树结构的过程中, 可能会出现含有其他附加信息的情况, 如红黑树的颜色信息等, 统称为 extra_prop. 可
使用关键字 type_synonym 来实现继承数据类型 dost 的基础上扩充额外的信息 [7] . 基于此, 可以定义数据类型 dost
的类型同义词 dost syn , 如下所示:

type_synonym a dost syn = “( a×extra_prop) dost”.
′
′
基于上述定义的数据类型, 可以定义函数 tsize 用于获取动态顺序统计树结构中树的大小信息. 如下所示.

//获取树的大小信息
fun tsize :: “ a dost ⇒ nat” where
′
“tsize Leaf = 0”|“tsize (Noden___) = n”
这个函数需要升级常规的搜索树操作来保证获取信息的准确性. 函数 size2 用于计算任一层根节点对应的树
的大小. 基于 size2 函数, 可定义函数 szNode 更新节点对应的树的大小信息, 并将其代替原始的 Node. 如此做, 在
对树中的节点信息进行更新时, 树的大小信息也会同步更改. 这些函数的正确执行依赖于建模策略和不变式的构
建, 在后文中会对其进行详细的介绍.

//计算树的大小信息
definition “size2 l r ≡ tsize l+tsize r +1”
//更新节点对应的树的大小信息
definition “szNode l a r ≡ Node (size2 l r) l a r”

需要说明的是, 函数 tsize、size2 和 szNode 都能在运行时间为 O(1) 的情况下实现. 所以, 将 Node 转换为 szNode
不会影响整体的时间复杂度. 因此, 在动态顺序统计树类结构中关于搜索树的基本操作, 与底层搜索树操作具有相
同的复杂度.
在上述定义的基础上, 我们给出如下缩写描述:


 Lea f ≡<>


.


 Node n l a r ≡< n,l,a,r >