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

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

5 自动化验证框架的适用范围及效果

5.1 适用范围

本文提出了动态顺序统计树类结构相关算法的自动化验证框架, 该框架的设计思路为: 使用同态的列表模拟
动态顺序统计树类结构的操作, 设计并验证列表辅助函数, 进一步借助列表辅助函数构建通用且可复用的验证引
理库. 本文的自动化验证框架主要适用于以下情况.
(1) 适用于至少满足两个不变式 inv S 和 T inv siz 的树型结构. 在第 4 节中, 以不平衡的二叉搜索树、红黑树和
e
2−3 树为典型案例进行了详细的讨论, 验证了本文自动化验证框架的适用性和有效性. 实际上, 动态顺序统计树类
结构操作的函数实现以及功能正确性验证依赖于搜索树不变式 inv S 和树的大小不变式 inv size . 对于至少满足两个
T
不变式 inv S 和 T inv siz 的树型结构, 如高度平衡树、AA 树、2−3−4 树等, 其函数操作的功能正确性均可借助本文
e
的自动化验证框架得到自动验证.
(2) 适用于动态顺序统计树类结构的 10 种操作, 包括动态集合相关操作 (即求最大/小值、前/后继)、顺序统
计操作 (即求树的大小、选择和求秩) 和搜索树操作 (即查找、插入和删除). 动态顺序统计树类结构能在 O(logn)
时间内实现顺序统计操作 [1] . 对于动态顺序统计树类结构常用的 10 种操作功能正确性的自动验证, Nipkow 在文
献 [5] 中提出的自动化验证框架仅适用于其中关于搜索树类结构的算法操作, 不适用于动态集合相关操作和顺序
统计操作. 而本文提出的自动化验证框架对这 10 种操作的功能正确性均能实现自动验证. 对于这 10 种操作以外
的特殊操作功能正确性的自动验证, 如实例化为区间树结构时如何维护区间信息等, 本文的自动化验证框架暂不
适用. 不过, 本文中用列表模拟树操作来简化目标命题的方法是通用的, 且验证引理库具有可扩展性. 在验证这类
特殊操作的功能正确性时, 可以按照相同的思路针对性地构建辅助验证引理集, 扩展验证引理库, 以此来简化目标
命题. 因此, 对于这类特殊操作, 本文的自动化验证框架可提供参考.
(3) 适用于功能正确性的自动化验证. 本文的自动化验证框架可以用于动态顺序统计树类结构的 10 种操作的
功能正确性验证, 实现自动证明. 而对于结构正确性的验证, 仍需构建专门的引理进行辅助验证, 自动化验证框架
无法直接实现自动证明. 然而, 通过第 3.3.2 节中提出的拆分方案, 可以将不变式 invar 进行拆分, 得到细化引理, 从
而降低验证目标命题的复杂度. 对于这些拆分后的细化引理, 自动化验证框架是适用的, 从而提高整体的自动化验
证效果.

5.2 效果对比
对于搜索树类算法的验证, 现有工作主要通过交互式验证方法 [9−16] 来确保正确性. 其思路为先设计待证明的
引理, 在初步化简命题之后, 分析化简后得到的子目标, 根据子目标的特性构造前置引理, 进一步化简子目标. 通过
不断地构造前置引理, 逐步化简子目标, 最终得到证明. 这一过程需要较多的人工参与, 前置引理的构造也需要创
造性思维, 对开发人员提出了较高的要求. 且这种方法不具有通用性, 在应用场景发生变化时, 需要重新构造前置
引理, 费时费力.
此外, Nipkow 在文献 [5] 中提出了验证搜索树类结构功能正确性的自动化验证框架, 对不同搜索树结构的功
能正确性进行了自动化证明. 然而, 该框架仅对搜索树类结构的查找、插入和删除操作进行了自动化验证, 不适用
于动态集合和顺序统计量相关算法操作.
本文提出的自动化验证框架, 一方面, 不需要额外构造前置引理, 减少人工参与. 且本文的验证引理库是通用
的, 在应用场景发生变化时, 依然可以证明目标命题. 另一方面, 本文的自动化验证框架除了适用现有工作已经得
到验证的搜索树相关操作 (查找、插入和删除), 还涵盖了动态集合 (如前继和后继等) 和顺序统计相关操作 (如选
择和求秩等). 交互式验证方法、文献 [5] 和本文的自动化验证框架这 3 种方法的对比如表 1 所示.
以函数 select 和函数 rank 的正确性验证为例, 图 22 给出了交互式验证方法和本文自动化验证框架的验证过
程对比. 从图 22 中可以看出, 采用本文提出的自动化验证框架, 不需要额外构造前置引理, 且验证代码行数显著
减少.