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

摘要：

矩阵是一种在计算机科学中应用广泛的数据结构,其运算正确性具有重要意义.矩阵求逆在矩阵形式化工作当中缺乏合理且实用的形式化工作.其原因在于,工程中现有的两种常见求逆方法的形式化均存在难点.第一种是基于伴随矩阵求解方法,难点在于无法形式化地表示n*n矩阵的子矩阵,导致构建余子式组成的矩阵十分困难,因此难以实现伴随矩阵求解逆矩阵形式化;第二种称作高斯约旦初等变换求解法,难点在于构造初等矩阵及其操作函数.若使用Coq归纳结构设计操作函数,即采用行优先填充二维表的思想,将舍弃列维度对二维表的描述信息,使得操作函数分支过多,需要设计复杂的归纳结构,导致后续形式化验证无法进行.文中提出了基于记录的矩阵函数构建法,使用行列两种维度同时描述矩阵,使得构造并证明初等矩阵成为可能,在此基础上实现了在Coq系统中基于高斯约旦消元法的矩阵求逆的形式化工作.以一种代价更小且时间复杂度更低的方式,实现了首个形式化验证下的软件逆矩阵函数库.

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

所属期刊栏目：50

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

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

页数：共7页

页码：848-854