Page 310 - 《软件学报》2021年第6期

1884 Journal of Software 软件学报 Vol.32, No.6, June 2021

记录的矩阵形式化方法.第 3 节提出基于 Coq 记录的分块矩阵形式化方法.第 4 节对矩阵与分块矩阵形式化证
明中所遇到的困难进行总结和分析.最后总结全文.
1 背景知识

1.1 Coq定理证明器
Coq 定理证明器是基于高阶带类型λ演算的交互式高阶逻辑定理证明器,它不但表达能力强,而且具备多个
具有实用价值的证明机制,比如可扩充的重写机制、基于模块的形式化理论构建机制以及程序抽取机制等等.
这些优秀的特点,使得这一证明工具在学术界越来越受欢迎,成为当今最为流行的定理证明工具之一.
Coq 基于归纳构造演算,有着强大的数学模型基础和很好的扩展性.Coq 中的归纳类型扩展了传统设计语
言中有关类型定义的概念,这与大多函数式程序设计语言中的递归类型定义相似.基于模式匹配和递归,每个归
纳类型对应一个计算结构,对于含有递归类型参数(如自然数、表等)的目标证明通常采用归纳证明方法,归纳证
明的过程取决于该递归类型的归纳定义.每个归纳声明定义了一组数据值,这些值可以用声明过的构造子来构
造.例如:布尔值可以用 true 和 false 来构造,自然数可以用 0 或 S 应用到另一个自然数上来构造,而列表可以用
nil 或者将 cons 应用到一个自然数和另一个列表上来构造.对于归纳类型进行归纳证明原理与数学归纳法类似,
以表类型为例证明步骤:1) 首先,证明当表 list1 为 nil 时 P list1 成立;2) 然后,证明当表 list1 为 cons n list1′时 P
list 成立.其中,n 是列表头元素,list1′是某个更小的列表,假设 P list1′成立.利用归纳证明所证明的引理能够保证
该引理内存在的情况都满足引理内容.
与许多其他编程语言(C,Java,Pascal 等)相似,我们可以在 Coq 中定义块机制,在块(section)内部,我们可以声
明或定义局部变量,并控制他们的作用域.在 Coq 系统中,各个 Section 都有相应作用范围,系统分别使用“Section
id”和“End id”表示 Section 的开始和结束.Section 可以嵌套,在其内部我们可以使用关键字“Parameter”和
“Variable”来进行全局声明和局部声明;在 Section 结束之后,局部变量会从当前上下文中消失.而在 Section 内部,
使用到这些变量的定义以及引理,都会增加局部变量类型作为参数.
Coq 提供了程序抽取功能,可以将经过认证的程序提取为 Ocaml,Haskell 或者 Scheme 之类的语言.在程序
抽取时,可将 Coq 中指定类型按一定规则映射到指定语言如 Ocaml 含有的类型之上.
1.2 相关工作

定理证明技术已成为当今软件工程领域中一种非常重要的形式化技术,该技术已经广泛应用于数学定理
证明、协议验证以及硬软件的安全特性验证,是人们解决软件系统正确性、可靠性的重要方法.
在基于定理证明器的矩阵形式化研究中,已存在部分相关工作:在 Isabelle/HOL 和 Coq 中,已有向量的形式
化 [6−8] ;Mizar 中描述了向量空间以及线性变换特征值 [9,10] ;Harrison 则在 HOL Light 中对欧几里德空间实向量以
及矩阵正交变换进行了较完整的形式化 [11] .在首都师范大学施智平团队中也开展了部分有关矩阵形式化的工
作:刘振科等人提出了函数矩阵理论在 HOL4 中的形式化 [12] ;康西楠在 HOL4 中已有的矩阵基本性质的基础上
给出矩阵变换形式化理论 [13] ;杨秀梅等人在 HOL4 中对向量和函数矩阵进行形式化,并对其连续性、微分以及
[3]
积分性质进行验证 [14] ;马振威提出了基于 Coq 记录的矩阵形式化方法 .
在矩阵形式化的研究中,首先要解决的一个关键问题是矩阵在定理证明器中的表示方法.一种是把矩阵定
义成从下标集合到元素集合的函数映射,基于 Isabelle/HOL 系统的研究工作主要采用了这种方法.这种方法的
优点在于比较容易证明矩阵的各种性质.在 Coq 的 ssreflect 库中包含的矩阵库也使用该方法的思路定义二维矩
阵 [15] ,将矩阵定义为由自然数矩阵生成实数的函数.但该实现比较复杂,并且不易理解以及使用.这类利用函数
来实现矩阵形式化的方法有一个缺点,即没有很好的对应计算机软件中的矩阵计算函数,也就是说,这些方法从
数学上证明了各种矩阵性质,却没有很好的验证软件中的矩阵函数的性质.
在基于 Lambda 演算的定理证明器中(比如 HOL/ISABELLE,Coq),可以用表 list 来表示矩阵,并在表的基础
上定义矩阵操作函数,并进行矩阵性质的证明.但是表本身没有长度限制,表类型也没有反映出指定长度或大小