替罪羊树的函数式建模与机械化验证

摘要

基于机器定理证明的形式化验证方法通过数学逻辑推理确保软件系统符合形式规约，从而有效规避潜在缺陷引发的严重后果，是确保软件正确性的重要方法.替罪羊树是一种平衡二叉搜索树，与常见的平衡二叉搜索树不同的是，它创新性地采用惰性平衡机制，只有当特定子树的不平衡度超过阈值时才触发重构操作维护平衡，避免了过大的开销，但其正确性验证是一个难题.为此，该文在Isabelle中给出了替罪羊树重构、插入、删除操作的函数式建模，并在Isabelle定理证明器中对上述操作进行机械化验证.从验证过程、验证脚本的模块化和代码的可执行性3个方面与Dafny验证进行对比.相较于目前替罪羊树结构的Dafny验证，定理数由180减少到113,且无须构造中间断言，从而减轻了验证的负担.

关键词

替罪羊树 / 函数式建模 / Isabelle定理证明器 / 机械化验证

基金资助

国家自然科学基金(62462037); 江西省主要学科学术与技术带头人培养课题(20232BCJ22013)资助项目