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

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

定理 8. isin 函数. invar t ⇒ isin x t = list_isin x (inorder t).
定理 9. insert 函数. invar t ⇒ inorder (insert a t) = list_ins a (inorder t).
定理 10. delete 函数. invar t ⇒ inorder (delete a t) = list_del a (inorder t).
定理 8−10 给出了搜索树结构常规的查找、插入和删除操作对应的正确性验证操作. 具体的验证引理集的构
建思路与上文中的其他定理类似. 这些函数的引理集如图 16 所示.

⟦ sorted (lst 1 @ a # lst 2 ); a ≤ x ⟧ ⟹
引理 35
list_del x (lst 1 @ a # lst 2 ) = lst 1 @ list_del x (a # lst 2 )
引理 30 list_isin x lst = (x ∈ set lst) ⟦ sorted (lst 1 @ a # lst 2 ); x < a ⟧ ⟹
引理 36
引理 31 sorted (x # xs) = ((∀y ∈ set xs. x < y) ∧ sorted xs) list_del x (lst 1 @ a # lst 2 ) = list_del x lst 1 @ a # lst 2
⟦ sorted (lst 1 @ a # lst 2 @ b # lst 3 ); x < b ⟧ ⟹
引理 32 sorted (xs @ [x]) = (sorted xs ∧ (∀y ∈ set xs. y < x)) 引理 37 list_del x (lst 1 @ a # lst 2 @ b # lst 3 ) =
list_del x (lst 1 @ a # lst 2 ) @ b # lst 3
⟦ sorted (lst 1 @ a # lst 2 @ b # lst 3 @ c # lst 4 ); x < c ⟧ ⟹
⟦ sorted (lst 1 @ [a]); x < a ⟧ ⟹
引理 33 引理 38 list_del x (lst 1 @ a # lst 2 @ b # lst 3 @ c # lst 4 ) =
list_ins x (lst 1 @ a # lst 2 ) = (list_ins x lst 1 ) @ a # lst 2
list_del x (lst 1 @ a # lst 2 @ b # lst 3 ) @ c # lst 4
⟦ sorted (lst 1 @ [a]); a ≤ x ⟧ ⟹
引理 34 ⟦ sorted (lst 1 @ a # lst 2 @ b # lst 3 @ c # lst 4 @ d # lst 5 ); x < d ⟧ ⟹
list_ins x (lst 1 @ a # lst 2 ) = lst 1 @ list_ins x (a # lst 2 )
引理 39 list_del x (lst 1 @ a # lst 2 @ b # lst 3 @ c # lst 4 @ d # lst 5 ) =
list_del x (lst 1 @ a # lst 2 @ b # lst 3 @ c # lst 4 ) @ d # lst 5
图 16 list_isin、list_ins 和 list_del 的验证引理集

函数 isin 实现判断元素是否在树中的操作, 这一实现与集合中的属于 (∈) 的功能一致. 因此, 可以进一步将列
表辅助函数 list_isin 转化为集合操作, 用集合来辅助验证, 以简化命题, 如引理 30–32 所示. 函数 insert 和 delete 的
实现按常规思路即可, 函数 list_ins 和 list_del 只需考虑左、右插入和删除节点的情况, 如引理 33–39 所示.
定理 1−10 描述的是动态顺序统计树类结构 10 种操作的功能正确性定理. 基于自动化验证框架, 10 种操作的
功能正确性均能得到自动验证.

3.3.2 结构正确性验证拆分方案
除了验证动态顺序统计树类结构 10 种操作的功能正确性以外, 还需保证修改类函数 (insert 和 delete) 操作前
后不变式 invar 成立, 即验证结构正确性.
对于修改类函数, 在操作过程中可能会改变树中的节点信息, 还需要引入额外的调整策略来维持整体平衡性.
因此, 对于此类函数的结构正确性验证, 可通过定理 11 和定理 12 来保证.
定理 11. insert 函数. invar t ⇒ invar (insert a t).
定理 12. delete 函数. invar t ⇒ invar (delete a t).
不同的动态顺序统计树结构所具有的不变式 invar 都不相同, 维持这些 invar 的调整策略差异较大, 没有统一
的设计思路. 所以, 对于结构正确性的验证, 仍需要构建针对性的引理辅助验证. 不过, 这些针对性引理的设计也可
遵循固定的模式. 以函数 insert 的结构正确性验证为例, 可采取拆分方案, 如下所示.

  ( )
  inv ST t ⇒ inv ST bal_ fun t
  1
 
 
  ( )
 

  inv size t ⇒ inv size bal_ fun t
  1
 

 ( ) 

 ( )

 invar t ⇒ invar bal_ fun t  inv prop1 t ⇒ inv prop1 bal_ fun t
 1
  1
 
 
 
 
  ...
 
 
  ( )
 
  inv propn t ⇒ inv propn bal_ fun t

 1


 ...
invar t ⇒ invar (insert a t)  .

  ( )

  inv ST t ⇒ inv ST bal_fun t

  n
 
 
  ( )
 
  inv size t ⇒ inv size bal_ fun t


  n
 
 ( ) 
  ( )

 invar t ⇒ invar bal_ fun t  inv prop1 t ⇒ inv prop1 bal_ fun t
 n
  n
 
 
 
 
 
  ...
 
  ( )
 
  inv propn t ⇒ inv propn bal_ fun t
n