标题：基于Isabelle的算法程序建模与验证的应用研究
作者：黄志鹏 陈小强 王鸿
作者单位：吉安职业技术学院，江西 吉安 343000
关键字：软件安全；函数式建模；机械化验证；Isabelle定理证明器；二叉搜索树
摘要：基于定理证明的形式化验证技术不受状态空间限制，对确保软件正确性至关重要。当前二叉搜索树指令式算法的形式化验证尤为困难，尤其在循环不变式构造上。相比之下，函数式程序因递归定义和无需循环不变式而更易于验证。为此，通过研究二叉搜索树类算法的共性，基于二叉搜索树类算法的Isabelle函数式建模框架，在Isabelle中对AVL插入和删除操作进行函数式建模，并验证插入和删除操作维持搜索树性质的正确性。