一种基于定理证明器Coq的稀疏矩阵形式化验证方法

摘要

本发明公开了一种基于定理证明器Coq的稀疏矩阵形式化验证方法，通过在定理证明器Coq中对稀疏矩阵进行形式化定义并且验证了稀疏矩阵运算的主要性质，主要包括以下步骤:(1)稀疏矩阵的形式化定义；(2)稀疏矩阵生成的形式化定义；(3)稀疏矩阵取元素运算的形式化定义；(4)稀疏矩阵运算的形式化定义；(5)基本性质的形式化证明。本发明利用定理证明器Coq严谨性和可靠性解决了软件代码难以以传统数学方法验证稀疏矩阵变换以及运算正确性的弊端。