基于Coq记录的矩阵形式化方法

摘要：

矩阵在工程系统中有广泛的应用,矩阵运算的正确性对工程系统的可靠性有重要影响.Coq是一种基于带类型λ演算的功能强大的高阶定理证明器.虽然Coq类型系统能够很好地描述可变大小的动态数据类型,但是对于固定大小的类似向量和矩阵的数据类型,其缺乏满意的描述机制.Coq库中也没有向量库或矩阵库,因此在使用Coq来对涉及矩阵的定理或算法进行形式化验证时十分复杂.针对这些问题,文中提出了一种基于Record类型的矩阵实现方法并定义了一组基本的矩阵函数,证明了它们的基本性质.基于文中提供的矩阵类型和相关引理可以比较轻松地完成飞行控制转换矩阵的验证.同其他矩阵实现方法相比,所提方法不仅在实现上相对简洁,在使用上也更加简单、方便.

关键词：Coq、矩阵、形式化验证、定理证明、记录类型

所属期刊栏目：46

分类号：TP311(计算技术、计算机技术)

资助基金：南京航空航天大学研究生创新基地实验室开放基金kfjj20171610;中央高校基本科研业务费专项资金资助

在线出版日期：2019-07-29（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：139-145