形式化方法以严格的数学化和机械化方法为基础来规约、构建和验证计算系统,是改善和确保计算系统质量的重要方法,其模型、技术和工具已延伸成为计算思维的重要载体。形式化方法中,形式化推导是通过对问题程序规约进行精确变换,最终得到算法程序。形式化验证是在对软件进行规约的基础上,验证软件是否具有所期望的性质。软件形式化方法使软件系统的描述更加精确,以减少可能的错误所带来的问题,提高软件的可靠性。图结构在现实生活中应用非常广泛,图的数据结构广泛应用在公路运输网络、地铁线路网络、网络节点优化等生活中的很多领域,另外计算机系统中的状态执行等也是基于图数据结构的。因此,图的深度优先遍历算法在现代的各种软件中应用十分频繁,这些软件的可靠性的高低很大程度取决于图的深度优先算法是否正确完备。深度优先算法的可靠性验证使用传统的手工推导来验证已经不能满足我们的需要了,数学定理证明工具Isabelle与软件形式化方法的结合既可以适应日益繁琐的软件验证,又可以避免手工推导验证所带来的失误。Isabelle是一种通用的且支持高阶逻辑的交互式定理证明器。它允许以正式语言表达数学公式,并提供用于在逻辑演算中证明这些公式的工具。主要应用是数学证明的形式化,尤其是形式化验证,其中包括证明计算机硬件或软件的正确性以及证明计算机语言和协议的特性。本文研究的内容主要是深入了解Isabelle系统的验证原理和逻辑结构,探索将形式化方法与Isabelle定理证明器相结合应用于实际生产,在对比形式化方法中的几种验证方法的优缺点后,选择使用Dijkstra最弱前置谓词方法作为验证方法。为了实现对深度优先遍历算法的验证,本文对Isabelle系统的规则库中加入了图的定义、深度优先遍历算法及其相关引理。并且结合Dijkstra最弱前置谓词方法完成了对图的深度优先遍历算法进行自动化验证。这些工作确保了深度优先遍历算法的可靠性和简化了手工推导验证的繁琐程度。扩充的Isabelle类型库为以后的研究者丰富了图结构的定义。将形式化方法与证明工具相结合一定程度上会促进形式化方法应用到实际生产中。