基于Coq的逆矩阵运算的形式化  

Formalization of Inverse Matrix Operation Based on Coq

作　　者：沈楠[1] 陈钢 SHEN Nan;CHEN Gang(College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210000,China)

机构地区：[1]南京航空航天大学计算机学院,南京210000

出　　处：《计算机科学》2023年第S01期848-854,共7页Computer Science

摘　　要：矩阵是一种在计算机科学中应用广泛的数据结构,其运算正确性具有重要意义。矩阵求逆在矩阵形式化工作当中缺乏合理且实用的形式化工作。其原因在于,工程中现有的两种常见求逆方法的形式化均存在难点。第一种是基于伴随矩阵求解方法,难点在于无法形式化地表示n*n矩阵的子矩阵,导致构建余子式组成的矩阵十分困难,因此难以实现伴随矩阵求解逆矩阵形式化;第二种称作高斯约旦初等变换求解法,难点在于构造初等矩阵及其操作函数。若使用Coq归纳结构设计操作函数,即采用行优先填充二维表的思想,将舍弃列维度对二维表的描述信息,使得操作函数分支过多,需要设计复杂的归纳结构,导致后续形式化验证无法进行。文中提出了基于记录的矩阵函数构建法,使用行列两种维度同时描述矩阵,使得构造并证明初等矩阵成为可能,在此基础上实现了在Coq系统中基于高斯约旦消元法的矩阵求逆的形式化工作。以一种代价更小且时间复杂度更低的方式,实现了首个形式化验证下的软件逆矩阵函数库。Matrix is a data structure widely used in computer science,and its correctness of operation is of great significance.In matrix formalization,there is no reasonable and practical formalization work.The reason lies in the difficulty in formalizing the two common inverse methods in engineering.The first method is based on the adjoint matrix solution method.The difficulty lies in that the submatrices of n*n matrix cannot be formally expressed,which makes it very difficult to construct the matrix composed of cosubformulas.Therefore,it is difficult to achieve the formalization of adjoint matrix inverse solution.The second method is called Gauss-Jordan elementary transformation method,the difficulty lies in the construction of elementary matrix and its operation function.If Coq is used to design the operation function of inductive structure,that is,the idea of filling two-dimensional table with rows first is adopted,the description information of two-dimensional table from column dimension will be discarded,so that the operation function branches too much and complex inductive structure needs to be designed,which leads to the failure of subsequent formal verification.In this paper,a record-based matrix function construction method is proposed,which describes the matrix in both column and column dimensions,making it possible to construct and prove the elementary matrix.On this basis,the formalization of matrix inversion in Coq system based on gaussian-Jordan elimination method is realized.And we implement the first software matrix inversion function library under formal verification in a way with lower cost and time complexity.

关 键 词：形式化验证 形式化工程数学 逆矩阵形式化 COQ 软件安全 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]