一种基于Coq的高斯约旦消元矩阵求逆形式化验证方法

摘要

本发明公开了一种基于Coq的高斯约旦消元矩阵求逆形式化验证方法，具体包括以下步骤：(1)在定理证明器Coq中采用一种基于Record的映射表示法；(2)在定理证明器Coq中采用高斯约旦消元理论实现定义的形式化；(3)矩阵求逆运算正确性的形式化证明；(4)在Coq定理证明器中进行OCaml代码抽取。本发明利用定理证明器Coq严谨性和可靠性解决了传统方法不能精确验证矩阵求逆的弊端，相较于传统的软件测试方法，具有可靠性和严谨性的特点，适用于航空航天，信息加密，飞行控制等领域系统模型构建，确保其运行的安全性。