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

作者：左正康; 黄志鹏; 黄箐; 孙欢; 曾志城; 胡颖; 王昌晶^*

来源：软件学报, 2023, 1-24.

DOI：10.13328/j.cnki.jos.007034

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

基于机器定理证明的形式化验证技术不受状态空间限制,是保证软件正确性、避免因潜在软件缺陷带来严重损失的重要方法. LLRB (left-leaning red-black trees)是一种二叉搜索树变体,其结构比传统的红黑树添加了额外的左倾约束条件,在验证时无法使用常规的证明策略,需要更多的人工干预和努力,其正确性验证是一个公认的难题.为此,基于二叉搜索树类算法Isabelle验证框架,对其附加性质部分进行细化,并给出具体化的验证方案.在Isabelle中对LLRB插入和删除操作进行函数式建模,对其不变量进行模块化处理,并验证函数的正确性.这是首次在Isabelle中对函数式LLRB插入和删除算法进行机械化验证,相较于目前LLRB算法的Dafny验证,定理数由158减少到84,且无需构造中间断言,减轻了验证的负担;同时,为复杂树结构算法的函数式建模及验证提供了一定的参考价值.

• 单位
  江西师范大学