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

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

小键值. 因此, max 和 min 函数可以分别通过递归遍历右、左子树节点实现. list_max 和 list_min 可以很好地模拟
这一情况, 只需遍历获得列表最末端、首端的键值即可. 由此, 可分别构建 list_max 和 list_min 的验证引理集, 如
图 11 所示. 引理 1 表示 list_max 可以正确获取列表最末端的键值元素. 引理 2 和引理 3 分别表示 list_max、list_min
能够模拟递归向右、左子树查找的过程.

引理 1 list_max (lst @ [a]) = a
list_max lst 2
list_max
引理 2 lst 2 ≠ [] ⟹ list_max (lst 1 @ a # lst 2 ) = list_max lst 2 a
lst 1 lst 2
list_min
list_min lst 1
引理 3 lst 1 ≠ [] ⟹ list_min (lst 1 @ a # lst 2 ) = list_min lst 1

图 11 list_max 和 list_min 的验证引理集

定理 3. pred 函数. invar t ⇒ pred x t = list_pred x (inorder t).
pred 函数获取前继元素对应两种情况: 一是左子树不为空时, 获取目标节点左子树中的最大元素; 二是左子树
为空时, 自底向上找到第 1 个右子树包含目标节点的祖先节点, 祖先节点对应的元素即为前继元素. 前者依赖于
max 函数, 可以用函数 list_max 模拟. 后者的实现需要正确记录祖先节点信息. 在自顶向下的查找过程中, 如果依
据查找策略判断得出沿着右边的路径进行查找, 则需记录当前的根节点信息 (对应记录目标节点的祖先节点信
息). 当找到目标节点时, 若其左子树为空, 则最近记录的根节点即为目标节点的前继节点.
基于上述分析, 可以构建函数 list_pred 的验证引理集, 如图 12 所示. 引理 4−6 处理边界情况, 即没有前继元素
的情况, 引理 4 和引理 5 表示若元素 x 不在列表中, 则无法求得其前继元素; 引理 5 表示列表中最小的元素 (即有
序列表的第 1 个元素) 没有前继元素. 引理 7−9 分别模拟目标节点等于、小于和大于当前根节点的情况. 若等于,
需要调用函数 link_max 来获取对应左子树中的最大元素, 该元素即为前继元素. 若小于或大于, 则需模拟树中向
左或向右递归查找的过程. 对应引理 7−9, 引理 10−12 则分别处理使用归纳法后节点增加的情况.

引理 4 sorted (a # lst) ⟹ x < a ⟹ list_pred x (a # lst) = None
引理 5 sorted (a # lst) ⟹ list_pred a (a # lst) = None
引理 6 sorted (lst @ [a]) ⟹ x > a ⟹ list_pred x (lst @ [a]) = None
Some ( list_max lst 1 )
sorted (lst 1 @ a # lst 2 ) ⟹ lst 1 ≠ [] ⟹
引理 7
list_pred a (lst 1 @ a # lst 2 ) = Some (list_max lst 1 )
x = a
sorted (lst 1 @ a # lst 2 ) ⟹ x < a ⟹
引理 8
list_pred x (lst 1 @ a # lst 2 ) = list_pred x lst 1 list_pred x lst 1 a lst 2
sorted (lst 1 @ a # lst 2 ) ⟹ x > a ⟹
引理 9
list_pred x (lst 1 @ a # lst 2 ) = list_pred x (a # lst 2 ) x < a
sorted (a # lst 1 @ b # lst 2 ) ⟹ lst 1 ≠ [] ⟹ list_pred lst 1
引理 10
list_pred b (a # lst 1 @ b # lst 2 ) = Some (list_max lst 1 )
sorted (a # lst 1 @ b # lst 2 ) ⟹ x < b ⟹ list_pred lst 2
引理 11
list_pred x (a # lst 1 @ b # lst 2 ) = list_pred x (a # lst 1 ) x > a
sorted (a # lst 1 @ b # lst 2 ) ⟹ x > b ⟹
引理 12
list_pred x (a # lst 1 @ b # lst 2 ) = list_pred x (b # lst 2 )
图 12 list_pred 的验证引理集

定理 4. sucd 函数. invar t ⇒ sucd x t = list_sucd x (inorder t).
求后继元素的函数 sucd 的实现思路与 pred 类似, 两者互为镜像操作. 函数 sucd 需借助 min 函数并记录左边
路径的根节点信息. 由此, 可以构建函数 list_sucd 的验证引理集, 如图 13 所示. 引理 13−15 处理没有后继元素的情