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

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

//函数dost23_size 中额外补充的 Node3 节点情况
dost 23 _size < n,_,_,_,_,_ >= n

//计算Node3节点对应树的大小值
definition “size3 l m r ≡ dost 23 _size l+dost 23 _size m+dost 23 _size r +2”
//函数inv size 中额外补充的Node3节点情况

inv size < n,l,_,m,_,r >= (inv size l∧inv size m∧inv size r ∧(size3 l m r = n))
2−3 树的所有叶子节点都在同一层, 即其同一层非叶子节点的高度是一致的. 函数 dost 23 _height 可以计算
2−3 树的高度. 由此, 可定义 2−3 树的高度不变式 inv height 确保 2−3 树高度一致性. 基于第 2.3 节的不变式, 可定义
2−3 树的不变式 invar 23 , 其不仅要满足 inv ST 和 inv size , 还需满足高度不变式 inv height . 具体定义如下.
//2−3树dost 23 的高度 不变式对应的 Node3 节点情况

′
fun inv height :: “ a dost 23 ⇒ bool” where
“inv height Node3_l_m_r = (inv height l & inv height m & inv height r &
dost 23 _height l = dost 23 _height m & dost 23 _height m = dost 23 _height r)”

//2−3树dost 23 的不变式
definition “invar 23 t ≡ inv ST t ∧ inv size t ∧ inv height t”
基于第 2 节的函数式建模框架和第 3 节的自动化验证框架, 可对 2−3 树的函数进行函数式建模并自动化验
证, 具体实现思路与第 4.1 节和第 4.2 节类似, 此处略.
本节旨在通过区域 (locale) 全面展示 2−3 树动态集合操作 (如前继和后继等), 顺序统计操作 (如选择和求秩
等) 和搜索树操作 (查找、插入和删除) 的正确性验证结果. 区域是一种程序模块化和参数化的复用机制, 能有效
表达函数式程序结构之间复杂的依赖关系 [17] . 通过区域声明, 前文定义了动态顺序统计树类结构通用的局部参数
(第 3.2 节图 4) 和逻辑规约 (第 3.3 节图 10). 其中, 局部参数对应要实现的 10 种函数操作, 逻辑规约对应待证明的
正确性定理 (包括功能正确性和结构正确性定理). 通过区域解释将局部参数实例化为 2−3 树的相关函数操作, 然
后对其逻辑规约进行验证. 在验证了 10 种函数操作的正确性定理之后, 逻辑规约的验证可以通过 try 命令直接得
出. 图 21 展示了 2−3 树 10 种函数操作的正确性验证结果, 进一步检验了本文第 2、3 节所提函数式建模和自动化
验证框架的有效性.

局部参数的实例化

逻辑规约的验证 try 命令直接得出

图 21 2−3 树 10 种函数操作的正确性验证结果