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

发布时间：2023-04-19 18:37

　　形式化方法以严格的数学化和机械化方法为基础来规约、构建和验证计算系统,是改善和确保计算系统质量的重要方法,其模型、技术和工具已延伸成为计算思维的重要载体。形式化方法中,形式化推导是通过对问题程序规约进行精确变换,最终得到算法程序。形式化验证是在对软件进行规约的基础上,验证软件是否具有所期望的性质。软件形式化方法使软件系统的描述更加精确,以减少可能的错误所带来的问题,提高软件的可靠性。图结构在现实生活中应用非常广泛,图的数据结构广泛应用在公路运输网络、地铁线路网络、网络节点优化等生活中的很多领域,另外计算机系统中的状态执行等也是基于图数据结构的。因此,图的深度优先遍历算法在现代的各种软件中应用十分频繁,这些软件的可靠性的高低很大程度取决于图的深度优先算法是否正确完备。深度优先算法的可靠性验证使用传统的手工推导来验证已经不能满足我们的需要了,数学定理证明工具Isabelle与软件形式化方法的结合既可以适应日益繁琐的软件验证,又可以避免手工推导验证所带来的失误。Isabelle是一种通用的且支持高阶逻辑的交互式定理证明器。它允许以正式语言表达数学公式,并提供用于在逻辑演算中证明这些公式的工具...

【文章页数】：48 页

【学位级别】：硕士

【文章目录】：
中文摘要
英文摘要
第1章 绪论
    1.1 研究背景
    1.2 国内外研究现状
    1.3 主要研究工作
第2章 Isabelle定理证明器
    2.1 定理证明器的分类
    2.2 Isabelle定理证明器的剖析
    2.3 Isabelle定理证明器的规则和策略
    2.4 本章小结
第3章 图结构的规则库和类型库在 Isabelle 中的扩充
    3.1 图结构扩充
    3.2 DFS的定义及其定理在Isabelle中的证明
    3.3 本章小结
第4章 基于Isabelle的 DFS算法的验证
    4.1 算法程序验证的方法
    4.2 DFS算法的自动化验证
    4.3 本章小结
总结
参考文献
致谢



本文编号：3793997