Isabelle定理证明器的剖析及其在PAR方法/PAR平台中的应用

论文摘要

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

论文目录

• 摘要
• Abstract
• 第一章 绪论
• 1.1 研究背景和意义
• 1.2 相关研究情况
• 1.3 主要研究工作
• 第二章 形式化方法和PAR 方法
• 2.1 形式化方法
• 2.1.1 形式化方法的研究内容
• 2.1.2 形式化方法的分类
• 2.1.3 形式化方法的能力和局限
• 2.1.4 形式化方法在高可信软件开发中的重要性
• 2.2 PAR 方法
• 2.2.1 PAR 方法/PAR 平台简介
• 2.2.2 算法设计语言Radl
• 2.2.3 抽象程序设计语言Apla
• 第三章 Isabelle 定理证明器的剖析
• 3.1 定理证明器的分类
• 3.2 Isabelle 定理证明器的剖析
• 3.2.1 Isabelle 定理证明器的特点
• 3.2.2 Isabelle 定理证明器的系统结构
• 3.2.3 Isabelle 定理证明器的理论
• 3.2.4 Isabelle 定理证明器的证明方法
• 3.3 Isabelle 定理证明器的规则/策略
• 3.3.1 规则
• 3.3.2 策略
• 第四章 Isabelle 在PAR 方法/PAR 平台中的应用
• 4.1 PAR 方法开发算法程序
• 4.2 算法程序正确性的证明方法
• 4.2.1 Floyd 的归纳断言法
• 4.2.2 Hoare 公理方法
• 4.2.3 Dijkstra 最弱前置谓词方法
• 4.3 Isabelle 验证使用PAR 方法/PAR 平台开发的算法程序
• 4.3.1 Isabelle 验证算法程序的工作流程
• 4.3.2 数组和算法程序的验证
• 4.3.3 数组段最小和算法程序的验证
• 4.3.4 Hanoi 塔非递归算法程序的验证
• 4.3.5 二叉树遍历非递规算法程序的验证
• 4.4 Isabelle 验证 PAR 平台中部分的转换代码
• 4.4.1 选择语句转换规则的验证
• 4.4.2 循环语句转换规则的验证
• 第五章 总结与展望
• 5.1 工作总结
• 5.2 下一步工作目标
• 参考文献
• 致谢
• 攻读学位期间参与的科研项目
• 攻读学位期间发表（完成）的学术论文目录