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

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

其中, 'a 类型对应的元素需满足全序关系 (后文也是如此), 符号<* *> 表示在对具体的函数建模过程中, 需根据函
数的实际功能填充的部分. 符号 [* *] 则表示可选项.
依据函数式建模策略可以推知, 通过目标节点信息和树的信息, 可以确定整个函数的操作路径. 所以, 在高阶
复合函数的函数类型中, 前两个参数分别表示目标节点 (targetType) 和动态顺序统计树的数据类型 ('a dost), 以此
来获取对应的信息并确定函数的操作路径. 第 3 个参数表示最后的结果类型 (resultType), 对于检索类函数, 对应检
索得到的信息; 对于修改类函数, 则对应调整后得到的动态顺序统计树.
在高阶复合函数的函数体中, 对于树为空的情况, 只需要根据函数功能返回对应的结果 (resultLeaf) 即可. 而对
于树不为空的情况的操作则更为复杂些. 首先, 需借助查找策略, 比较目标节点和当前节点的大小关系 (compOperation).
然后, 根据比较的结果确定需要执行的函数操作. 若比较结果为小于 (LT) 或大于 (GT), 则递归地在其左子树或右
子树上寻找目标节点的位置 (分别对应 resultLT 和 resultGT). 若为相等 (EQ), 则说明查找成功, 执行相应的函数操
作对目标节点进行处理, 返回处理后的结果 (resultEQ). 在查找的过程中, 可以根据需要补充一些前置操作 (preOperation)
对当前的信息进行处理. 对于修改类函数操作, 则还需要在返回最终结果前, 依据调整策略进行平衡调整 (adjustLeaf、
adjustLT、adjustGT 和 adjustEQ).

2.3 动态顺序统计树类结构的不变式
不变式是指程序在执行过程中必须遵守的逻辑规则 [18] . 在对动态顺序统计树类结构对应的算法进行建模时,
需要保证算法执行前后得到的动态顺序统计树均满足不变式. 因此, 不变式是函数式建模的一个标准, 当对修改类
函数操作进行建模时, 其调整操作得到的结果需满足不变式.
动态顺序统计树结构的性质可被定义如下.
(1) 搜索树性质不变式 (简称 inv ST ), 即中序遍历节点的键值按照线性升序的方式排序 [17] . 函数 inorder 按照中
序遍历的顺序将动态顺序统计树中的节点转换为列表. 得到转换后的列表之后, 借助 Isabelle 中的函数 sorted 可判
断该列表是否按升序排列. inv ST 可定义为这两个函数的组合, 如下所示.

//将动态顺序统计树转换为列表 (针对dost类型)
fun inorder :: “ a dost ⇒ a list” where
′
′
“inorder <>= []”|
“inorder < _,l,a,r >= inorder l @ a # inorder r”
//搜索树性质不变式
definition “inv ST t ≡ sorted (inorder t)”

inv ST 的实现需要获取树中节点的键值信息, 而不依赖其他额外的信息. 对于扩充了额外信息的 dost syn 类型,
其节点中不仅包含键值信息, 还有其他额外信息. 因此, 在 dost syn 类型中实现 inv ST 时, 需要从节点中提取出键值信
息, 即将上述的 inorder 函数替换为 inorder2 函数, 如下所示. 可以发现, 相较于 inorder 函数, inorder2 函数仅在处
理过程中额外添加了一步忽略额外信息的操作. 类似地, 对于其他同样不依赖额外信息的 dost syn 类型函数, 实现思
路与 dost 类型一致, 只需要忽略额外信息即可.

//将动态顺序统计树转换为列表 (针对dost syn 类型)
′
′
fun inorder2 :: “ a dost syn ⇒ a list” where
“inorder2 <>= []”|
“inorder2 < _,l,(a,_),r >= inorder l @ a # inorder r”
(2) 树的大小不变式 (简称 inv size ), 即树中的每个 Node 节点中的 nat 类型对应的信息, 都应正确存储对应的树
的大小值. inv size 可通过递归实现, 即需保证根节点中存储的树的大小值是正确的, 且其左、右子树对应的节点也
同样正确. 基于 size2 函数, 可对 inv size 进行函数式建模, 其定义如下.