LLRB算法的函数式建模及其机械化验证  

Functional Modeling and Mechanized Verification of LLRB Algorithm

作　　者：左正康[1] 黄志鹏 黄箐 孙欢[2] 曾志城 胡颖 王昌晶[1] ZUO Zheng-Kang;HUANG Zhi-Peng;HUANG Qing;SUN Huan;ZENG Zhi-Cheng;HU Ying;WANG Chang-Jing(School of Computer Information Engineering,Jiangxi Normal University,Nanchang 330022,China;School of Digital Industry,Jiangxi Normal University,Shangrao 334006,China)

机构地区：[1]江西师范大学计算机信息工程学院,江西南昌330022 [2]江西师范大学数字产业学院,江西上饶334006

出　　处：《软件学报》2024年第11期5016-5039,共24页Journal of Software

基　　金：国家自然科学基金(61862033,62262031);江西省自然科学基金(20212BAB202018);江西省教育厅科技重点项目(GJJ210307)。

摘　　要：基于机器定理证明的形式化验证技术不受状态空间限制,是保证软件正确性、避免因潜在软件缺陷带来严重损失的重要方法.LLRB(left-leaning red-black trees)是一种二叉搜索树变体,其结构比传统的红黑树添加了额外的左倾约束条件,在验证时无法使用常规的证明策略,需要更多的人工干预和努力,其正确性验证是一个公认的难题.为此,基于二叉搜索树类算法Isabelle验证框架,对其附加性质部分进行细化,并给出具体化的验证方案.在Isabelle中对LLRB插入和删除操作进行函数式建模,对其不变量进行模块化处理,并验证函数的正确性.这是首次在Isabelle中对函数式LLRB插入和删除算法进行机械化验证,相较于目前LLRB算法的Dafny验证,定理数由158减少至84,且无需构造中间断言,减轻了验证的负担;同时,为复杂树结构算法的函数式建模及验证提供了一定的参考价值.Unlimited by the state and space,the formal verification technology based on mechanized theorem proof is an important method to ensure software correctness and avoid serious loss from potential software bugs.LLRB(left-leaning red-black trees)is a variant of binary search trees,and its structure has an additional left-leaning constraint over the traditional red-black trees.During verification,conventional proof strategies cannot be employed,which requires more manual intervention and effort.Thus,the LLRB correctness verification is widely acknowledged as a challenging problem.To this end,based on the Isabelle verification framework for the binary search tree algorithm,this study refines the additional property part of the framework and provides a concrete verification scheme.The LLRB insertion and deletion operations are functionally modeled in Isabelle,with modular treatment of the LLRB invariants.Subsequently,the function correctness is verified.This is the first mechanized verification of functional LLRB insertion and deletion algorithms in Isabelle.Compared to the current Dafny verification of the LLRB algorithm,the theorem number is reduced from 158 to 84,and it is unnecessary for constructing intermediate assertions,which alleviates the verification burden.Meanwhile,this study provides references for functional modeling and verification of complex tree structure algorithms.

关 键 词：LLRB 函数式建模 机械化验证 Isabelle定理证明器 二叉搜索树 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]