基于Record类型的矩阵形式化

发布时间：2022-08-13 10:54

　　矩阵在理论数学、工程数学以及计算机科学中都有着广泛的应用。例如飞行控制系统的设计中,矩阵被用于飞行器受力状况的描述,运动学方程的推导,以及飞行控制算法的设计。因此,矩阵算法和矩阵数学推导的正确性对这类安全关键系统的可靠性有着极大的影响。形式化方法是保障计算机系统安全可靠的一种重要方法,其中定理证明技术可用于数学公式和计算机算法的验证,是最严格、最强力的验证手段。Coq就是这样一个交互式的高阶定理证明器,它基于归纳构造演算的基本理论,具有很强的表达能力,支持丰富的逻辑系统。Coq可用于表达规范说明,构造满足规范说明的程序模型,以及对可信性要求很高的程序进行形式化验证。虽然Coq中有着丰富的定理库,但是,现有的矩阵形式化方面的几种方案却不尽人意,基于List的方案表达能力受限,基于依赖类型List的方案复杂难验证,基于函数的方案只是验证了矩阵理论,不能构造出具有具体数据的矩阵,也不能用于实际矩阵的推导验证,并且不利于从描述中提取可执行程序。本文提出了一种基于Record类型的矩阵形式化方法,它具有描述上的简明性、证明上的简单性、使用上的简便性以及程序抽取的可行性等诸方面的综合性优势。本文主... 

【文章页数】：78 页

【学位级别】：硕士

【文章目录】：
摘要
abstract
注释表
第一章 绪论
    1.1 研究背景
    1.2 研究现状
        1.2.1 HOL中的矩阵形式化
        1.2.2 基于元组的矩阵形式化
        1.2.3 基于List的矩阵形式化
        1.2.4 基于依赖类型的List的矩阵形式化
        1.2.5 基于函数的矩阵形式化
    1.3 研究的工作和意义
    1.4 本文安排
第二章 背景知识
    2.1 形式化验证工具
        2.1.1 模型检测工具
        2.1.2 定理证明工具
    2.2 Coq定理证明器
        2.2.1 Coq系统结构
        2.2.2 Coq中的数据类型及语法
        2.2.3 Coq中的证明方法
    2.3 Coq标准库及第三方库
        2.3.1 Coq标准库
        2.3.2 mathcomp库
        2.3.3 Coquelicot库
    2.4 Coq相关应用
    2.5 本章小结
第三章 基于Record类型的矩阵实现
    3.1 向量的定义与验证
        3.1.1 向量的定义
        3.1.2 向量运算及基本性质
    3.2 矩阵的定义与验证
        3.2.1 矩阵的定义
        3.2.2 矩阵运算及基本性质
    3.3 本章小结
第四章 具体类型矩阵形式化
    4.1 实数矩阵
    4.2 复数矩阵
    4.3 实数函数矩阵
        4.3.1 函数域
        4.3.2 函数矩阵
        4.3.3 二重积分
        4.3.4 函数矩阵微积分
    4.4 本章小结
第五章 飞行控制系统中坐标系转换矩阵验证实例
    5.1 转换矩阵的验证
    5.2 运动学方程验证
    5.3 本章小结
第六章 总结与展望
    6.1 研究工作总结
    6.2 未来工作展望
参考文献
致谢
在学期间的研究成果及发表的学术论文



本文编号：3676894