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

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

//实例化为不平衡的二叉搜索树dost bst 的插入函数
′
′
′
fun dost bst _insert :: “ a ⇒ a dost bst ⇒ a dost bst ” where
“dost bst _insert x <>= szNode Leaf x Leaf”|
“dost bst _insert x < _,l,a,r >= (case cmp x a o f
LT ⇒ szNode (dost bst _insert x l) a r|
GT ⇒ szNode l a (dost bst _insert x r)|
EQ ⇒ szNode l a r)”

(2) 自动化验证
对于其结构正确性的验证, 则需借助第 3.3.2 节的拆分方案. 树 dost bst 的不变式 invar bst 满足 inv ST 和 inv size , 不
具有附加性质 inv prop . 因此, 先分别基于 inv ST 和 inv size 进行验证, 再验证函数 dost bst _insert 的结构正确性. 对于拆分
后得到的细化引理, 本文的自动化验证框架可以适用, 提升整体的自动化验证水平, 如图 19 所示.

inv size 对应的细化引理
归纳法
auto 方法
list_ins 验证引理集 函数定义

inv ST 对应的细化引理
归纳法 list_ins 验证引理集
auto 方法 函数定义
try 命令
直接得出

插入函数 dost bst _insert
的结构正确性定理

函数定义 inv ST 细化引理 inv size 细化引理

图 19 函数 dost bst _insert 的结构正确性验证过程

4.2 实例化为平衡的二叉搜索树
红黑树是最为常用的平衡二叉搜索树, 广泛应用于操作系统内核、数据库索引和任务调度等领域. 例如, 在
Linux 内核中, 可使用动态顺序统计红黑树来管理进程调度、内存区域和虚拟内存页表等数据结构, 优化数据的
存储和检索效率. 红黑树最早由 Bayer [21] 提出, Guibas 等人 [22] 引入了红/黑的颜色约定. 红黑树具有附加的颜色性
质, 在调整操作中, 需要对颜色性质进行调整. 基于第 2.1 节中动态顺序统计树类结构的函数式定义, 将 dost syn 实
例化为 dost rbt , 并将 extra_prop 实例化为附加的红/黑颜色信息 tcolor, 其结构可定义为:

type_synonym a dost rbt = “( a×tcolor) dost”.
′
′
红黑树具有以下性质:
(1) 每个节点是红色或黑色, 故引入附加信息 tcolor 来表示;
(2) 根节点是黑色, 即 dost rbt _color t = Black;
(3) 所有的叶子节点 (<>) 都是黑色, 即 dost rbt _color Leaf = Black, 这是默认的;
(4) 每个红色节点的两个子节点都是黑色, 即从每个叶子节点到根节点的所有路径中, 不能出现两个连续的红
色节点, 用 inv color 来表示这一性质;