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