基于Isabelle的DFS算法的自动验证.pdf

基于Isabelle 的DFS 算法的自动化验证 摘 要 形式化方法以严格的数学化和机械化方法为基础来规约、构建和验证计算系 统，是改善和确保计算系统质量的重要方法，其模型、技术和工具已延伸成为计 算思维的重要载体。形式化方法中，形式化推导是通过对问题程序规约进行精确 变换，最终得到算法程序。形式化验证是在对软件进行规约的基础上，验证软件 是否具有所期望的性质。软件形式化方法使软件系统的描述更加精确，以减少可 能的错误所带来的问题，提高软件的可靠性。 图结构在现实生活中应用非常广泛，图的数据结构广泛应用在公路运输网 络、地铁线路网络、网络节点优化等生活中的很多领域，另外计算机系统中的状 态执行等也是基于图数据结构的。因此，图的深度优先遍历算法在现代的各种软 件中应用十分频繁，这些软件的可靠性的高低很大程度取决于图的深度优先算法 是否正确完备。深度优先算法的可靠性验证使用传统的手工推导来验证已经不能 满足我们的需要了，数学定理证明工具Isabelle 与软件形式化方法的结合既可以 适应日益繁琐的软件验证，又可以避免手工推导验证所带来的失误。 Isabelle 是一种通用的且支持高阶逻辑的交互式定理证明器。它允许以正式 语言表达数学公式，并提供用于在逻辑演算中证明这些公式的工具。主要应用是 数学证明的形式化，尤其是形式化验证，其中包括证明计算机硬件或软件的正确 性以及证明计算机语言和协议的特性。 本文研究的内容主要是深入了解Isabelle 系统的验证原理和逻辑结构，探索 将形式化方法与Isabelle 定理证明器相结合应用于实际生产，在对比形式化方法 中的几种验证方法的优缺点后，选择使用Dij kstra 最弱前置谓词方法作为验证方 法。为了实现对深度优先遍历算法的验证，本文对Isabelle 系统的规则库中加入 了图的定义、深度优先遍历算法及其相关引理。并且结合Dij kstra 最弱前置谓词 方法完成了对图的深度优先遍历算法进行自动化验证。这些工作确保了深度优先 遍历算法的可靠性和简化了手工推导验证的繁琐程度。扩充的Isabelle 类型库为 以后的研究者丰富了图结构的定义。将形式化方法与证明工具相结合一定程度上 会促进形式化方法应用到实际生产中。 关键字：形式化方法 自动化验证 Isabelle 定理证明器 深度优先有哪些信誉好的足球投注网站算法 I Abstract Formal methods are based on strict mathematical and mechanized methods to reduce, construct, and verify computing systems. They are important methods to improve and ensure the quality of computing systems. Their models, technologies, and tools have become an important carrier of computing thinking. In the formal method, the formal derivation is to obtain the algorithm program through precise transformation of the problem program specification. Formal verification is based on the specification of the software to verify whether the software has the desired properties. The formal method of software makes the description of t