形式化方法可以对系统进行严格的规约,并可以从不同的角度验证开发的系统是否具有所期望的性质,在高可信软件的开发中越来越受重视。定理证明是计算机领域中形式化验证的重要研究课题,对保证软件的正确性和可靠性具有十分重要的意义。Isabelle是基于高阶逻辑的交互式定理证明工具,它具有丰富的类型系统,强大的规则库和灵活高效的命令集;它不仅支持多种对象逻辑,而且允许用户自定义新的逻辑。开发正确且高效的算法程序仍然是计算机科学中最具有挑战性的核心工作。PAR方法是薛锦云教授提出的基于分划和递推的算法程序设计方法;它是一种简单实用的支持算法程序开发全过程的形式化方法,并对于理解和证明算法程序十分有效,是算法程序设计和证明方法研究方面的重要突破。PAR平台是支撑PAR方法的CASE工具。使用定理证明工具对算法程序进行机械证明是一种发展趋势。本文分析了Isabelle定理证明器的系统结构、验证原理和核心技术;根据PAR方法/PAR平台开发算法程序的特点,探讨了如何运用Isabelle定理证明器形式化验证算法程序的工作流程,并对一些算法程序进行正确性验证;最后,阐述了如何使用Isabelle证明PAR平台中部分转换代码的正确性。本文的创新点体现在以下两个方面:1、提出了一种使用Isabelle定理证明器对算法程序进行机械验证的方法。该方法既克服了传统手工验证过程的繁琐性和易错性等缺点;又达到“提高验证效率和保证算法程序高可信”的目标,具有很好的实用价值。2、实现了Isabelle定理证明器和PAR方法/PAR平台的有机结合。一方面,算法程序的验证依赖于使用PAR方法开发的循环不变式;另一方面,使用Isabelle定理证明器验证了PAR平台中部分转换代码的正确性,从而保证了Apla程序到可执行程序转换的一致性。