程序验证与模型检验
程序验证
基本概念
一个语言 A 的验证器 V 被定义为
语言 A
在形式语言理论中，语言 A 是一个字符串集合
A 指定了什么样的输入字符串是“合法”的，它定义了一个问题或特性，并且用于描述一个问题的解集，可以用逻辑表达式、代数表达式等数学语言来描述
这里的语言是一个抽象的数学对象，它并不特指自然语言，而是任何形式化的字符串集合
在自动机理论中，语言通常由某种形式化规则定义。这里的“语言”沿用传统定义，表示可以被某种形式化系统识别的字符串集合
而在计算复杂性理论中，一个语言 A 通常对应于一个决策问题。判定一个字符串 w 是否属于语言 A，等同于解决一个具体的问题
验证器 V
V 是一个算法，用于确定某个给定字符串 w 是否属于语言 A
V 的设计是基于 A 的定义，也就是说 V 了解 A 所定义的性质，并被编写成可以检查某个 w 是否具有这些性质的程序
V 可以是一个形式化验证工具、一个SAT求解器、一个模型检测器，或一个测试框架，等等。
模型/待检验对象 w
w 有多种表现形式，可以是一段待验证的算法或程序，一个系统的抽象模型，一个系统或算法的一组具体输入数据，等等
证明/反例 c
c 的作用是为 V 提供附加的信息来辅助判断一个字符串 w 是否属于 A
验证不同的 w 是否属于 A，可能要对应寻找不同的 c
c 不一定是必须的，需不需要c 取决于问题的具体上下文和问题的复杂性。对于 NP 类问题，c 是关键的，而对于 P 类问题，c 可能不需要
c 可以是一个形式化证明过程，确保 w 属于 A，也可以是一个反例，说明 w 不属于 A
例子
我想验证一段排序算法代码的正确性
设计规约
我希望排序后数组中的每个元素都应小于或等于后一个元素
A: \quad i,j (\text{if} \ \ i < j \ \ \text{then} \ \ arr[i]≤arr[j])
构建模型
代码的行为就是模型 w，验证代码的正确性就是验证 w 是否属于规约 A，即是否有 w \in A
构建反例或证明
我构造了一个测试样例集，这些测试样例也许就存在一个反例 c_1 能证明我的算法不正确
或者，我将代码逻辑抽象到数学层次，对其使用形式化语言进行描述，使用数学工具（命题逻辑、数学归纳法等）对算法的正确性给出了证明 c_2
验证
我采用自动化测试框架作为验证器 V_1
V_1 依次抽取测试样例输入给 w，验证 w 的输出。如果存在一个反例 c_1，V_1 将告知我 w \notin A（这样的 V_1 能证伪，但不能证明）
我采用交互式的定理证明辅助工具作为验证器 V_2
V_2 检验我的证明过程是否有推理错误、是否完整，如果考察通过说明我的证明无误，则算法的正确性得以被证明
模型检验
基本概念
计算机系统的设计、规约以及验证往往是使用逻辑语言来描述如下关系
\mathcal{M} 是系统的某种情况或模型
\phi 是一个规范，用一个逻辑的公式来表示 \mathcal{M} 应该满足某种约束
\mathcal{M} \models \phi 表示 \mathcal{M} 满足 \phi
逻辑语言的选择
如何统一化定义 \mathcal{M} 和 \phi？使用同一种逻辑来描述 \mathcal{M} 和 \phi？
经典逻辑（命题逻辑、一阶逻辑、高阶逻辑等）可以来描述 \mathcal{M} 和 \phi
但是命题逻辑的描述能力太弱，只能处理基本的真假关系
一阶逻辑和高阶逻辑的表达能力强大，但同时也带来更高的复杂性，使得验证过程更困难
重新定义 \phi
使用时序逻辑（线性时序逻辑 LTL、计算树逻辑 CTL）来描述系统行为随时间变化的逻辑
重新定义 \mathcal{M}
使用状态转换系统对系统进行建模：\mathcal{M} = (S, \to, L)
- S 是系统状态的集合
- \to 是状态转换关系，表示从状态 s \in S 到下一个状态 s′ \in S 的转换关系
- L 是状态标签函数，是 S 到 \mathcal{P}(\text{Atoms}) 的映射，\text{Atoms} 是系统的基本原子命题，\mathcal{P}(\text{Atoms}) 表示原子命题集合的子集。表示：当处于状态图中的哪个状态时，对应着哪些原子命题为真
例子
为了检验一个系统 P 是否满足某个性质，通常需要按照以下步骤进行
- 先选择模型检查器
- 再使用模型检查器的规约语言对系统 P 进行建模，得到模型 \mathcal{M}
- 使用模型检查器的规约语言对属性进行编码，得到逻辑公式 \phi
- 最后将 \mathcal{M} 和 \phi 输入给模型检查器