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

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

况, 引理 13 和 14 表示元素不在列表中, 引理 15 则表示列表中最大的元素 (即有序列表的最后一个元素) 没有后
继元素. 引理 16−18 分别对应根节点 (等于)、左子树 (小于)、和右子树 (大于) 的情况. 对于二叉型的结构, 这种方
式已经涵盖了所有的路径执行情况. 而对于多叉型结构, 同样具有搜索树性质. 依据建模策略, 同样可以将其分为
小于、等于和大于的情况, 再根据具体的结构, 在上述 3 种情况的基础上再细分小于、等于和大于的情况. 将树结
构映射到列表结构中后, 二叉型和多叉型结构对应的情况是一样的, 所以该方式同样有效. 引理 19 对应处理归纳
法中非平凡情况节点增加的情况.

引理 13 sorted (lst @ [a]) ⟹ x > a ⟹ list_sucd x (lst @ [a]) = None
Some ( list_min lst 2 )
引理 14 sorted (a # lst) ⟹ x < a ⟹ list_sucd x (a # lst) = None
x = a
引理 15 sorted (lst @ [a]) ⟹ list_sucd a (lst @ [a]) = None
sorted (lst 1 @ a # lst 2 ) ⟹ lst 2 ≠ [] ⟹
引理 16 list_sucd x lst 1 a lst 2
list_sucd a (lst 1 @ a # lst 2 ) = Some (list_min lst 2 )
sorted (lst 1 @ a # lst 2 ) ⟹ x < a ⟹
引理 17 x < a
list_sucd x (lst 1 @ a # lst 2 ) = list_sucd x (lst 1 @ [a])
list_sucd lst 1 a
sorted (lst 1 @ a # lst 2 ) ⟹ x > a ⟹
引理 18
list_sucd x (lst 1 @ a # lst 2 ) = list_sucd x lst 2
list_sucd lst 2
sorted (lst 1 @ a # b # lst 2 ) ⟹
引理 19 x > a
list_sucd a (lst 1 @ a # b # lst 2 ) = Some b
图 13 list_sucd 的验证引理集

定理 5. tsize 函数. invar t ⇒ tsize t = size (inorder t).
定理 5 表示 tsize 函数获取的树的节点大小值是正确的. 对于该定理的证明, 自动化证明组件足以应付, 无需
构造额外的验证引理集. 图 14 展示了定理 5 的自动化验证 (tsize 实例化为 dost_size), 只需要通过归纳法并调用一
次 auto 方法即得证.

图 14 dost_size 的正确性验证

定理 6. select 函数. invar t ⇒ k > 0 ⇒ select k t = list_sel (k −1) (inorder t).
定理 7. rank 函数. invar t ⇒ rank x t = list_rank x (inorder t).
与函数 list_pred 函数 list_sucd 验证引理集的构建思路类似, 函数 list_sel 和 list_rank 均对不在列表中、等于、
小于和大于的情况进行了模拟操作并验证, 如图 15 所示. 函数 select 的查找过程依赖于树的大小信息, 因此, 函数
list_sel 的模拟过程需根据列表的大小信息来判断查找方向, 如引理 20–24 所示. 函数 rank 的查找过程为常规的递
归查找, 因此 list_rank 的模拟过程则根据键值大小判断方向即可, 如引理 25–29 所示.

引理 25 sorted (a # lst) ⟹ x < a ⟹ list_rank x lst = None
引理 20 k > size lst ⟹ list_sel k lst = None
引理 26 sorted (lst @ [a]) ⟹ x > a ⟹ list_rank x (lst @ [a]) = None
引理 21 k = size lst 1 ⟹ list_sel k (lst 1 @ a # lst 2 ) = Some a
sorted (lst 1 @ a # lst 2 ) ⟹ k = size lst 1 + 1 ⟹
引理 22 引理 27
list_rank a (lst 1 @ a # lst 2 ) = Some k
k < size lst 1 ⟹ list_sel k (lst 1 @ a # lst 2 ) = list_sel k lst 1
k > size lst 1 ⟹ list_sel k (lst 1 @ a # lst 2 ) = sorted (lst 1 @ a # lst 2 ) ⟹ x < a ⟹
引理 23 引理 28
list_sel (k−size lst 1 −1) lst 2 list_rank x (lst 1 @ a # lst 2 ) = list_rank x lst 1
k > size lst 1 +1 ⟹ list_sel k (lst 1 @ a # lst 2 ) = sorted (lst 1 @ a # lst 2 ) ⟹ x > a ⟹ k = size lst 1 + 1 ⟹
引理 24 引理 29
list_sel (k−size lst 1 −1−1) lst 2 list_rank x (lst 1 @ a # lst 2 ) = plus_option k (list_rank x lst 2 )
图 15 list_sel 和 list_rank 的验证引理集