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

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

//实例化为不平衡的二叉搜索树dost bst 的选择函数
′
′
fun dost bst _select :: “nat ⇒ a dost bst ⇒ a option” where
“dost bst _select k <>= None”|
“dost bst _select k < _,l,a,r >= (let n = tsize l+1 in case cmp k n o f
LT ⇒ dost bst _select k l|
GT ⇒ dost bst _select (k −n) r|
EQ ⇒ Some a)”
//实例化为不平衡的二叉搜索树dost bst 的求秩函数
fun dost bst _rank :: “ a ⇒ a dost bst ⇒ nat option” where
′
′

“dost bst _rank_ <>= None”|
“dost bst _rank x < _,l,a,r >= (let n = tsize l+1 in case cmp x a of
LT ⇒ dost bst _rank x l|

GT ⇒ plus_option n (dost bst _rank x r)|
EQ ⇒ Some n)”
(2) 自动化验证
基于第 3.3 节给出的基于引理库的自动化验证策略, 可以在 Isabelle 中自动验证树 dost bst 函数的功能正确
dost bst _rank 的功能正确性验证, 在采用归纳法拆解目标后, 使用 auto 方法调用验证
性. 对于函数 dost bst _select 和
引理库中对应的验证引理集, 并添加相应的函数定义和辅助函数的正确性引理, 可以化简目标命题进而实现自
动证明, 如图 18 所示. 对于其他函数功能正确性的验证, 同样仅需使用归纳法并调用一次 auto 方法或使用 try
命令即可.

选择函数 dost bst _select
的正确性定理
归纳法
auto 方法

list_sel 验证引理集 函数定义 辅助函数的正确性引理
求秩函数 dost bst _rank
的正确性定理
归纳法
auto 方法

list_rank 验证引理集 函数定义 辅助函数的正确性引理
图 18 函数 dost bst _select 和 dost bst _rank 的功能正确性自动化验证过程

4.1.2 dost bst 的结构正确性验证
选择和求秩函数操作前后不会改变树的结构, 仅需对其功能正确性进行验证. 但是, 对于插入函数 insert 等修
改类函数, 在操作过程中可能会改变树中的节点信息. 因此, 对于此类函数的验证, 除了验证其功能正确性以外, 还
需保证其操作前后不变式 invar bst 成立, 即验证结构正确性.
(1) 函数式建模
以函数 insert 为例, 基于第 2.2 节中的高阶复合函数, 将 insert 实例化 dost bst _insert, 对其进行函数式建模, 如
下所示. 其中, szNode 对应平衡调整操作 (adjustLeaf、adjustLT、adjustGT 和 adjustEQ).