小村软件有限公司
日本語 English 한국어 繁體中文 简体中文 العربية
联系我们
菜单

SPARK形式化验证入门 ── 从Ada的契约走向数学证明

· · Ada, SPARK, 形式化验证, GNATprove, 契约式设计, 高完整性, 编程语言, 高可靠性

1. 前言 ── 超越「运行后确认」的方法

保证软件质量最常见的方法就是测试。

测试：确认在选定的输入下能正确运行

然而，测试有其极限。输入的组合是无限的，仅靠测试无法证明「在所有输入下都正确」。

这时登场的就是形式化验证(Formal Verification)。

形式化验证：用数学方式证明性质对所有输入都成立

上一篇文章「Ada语言的魅力」介绍了Ada的整体概貌，也简单提到了SPARK。

本文将聚焦于运用SPARK进行形式化验证的实务，整理以下内容：

SPARK是什么。与Ada的关系如何
契约（Pre/Post）该怎么写
如何用GNATprove进行证明
如何设计循环不变式
如何用数据流契约（Global/Depends）管理副作用
证明等级（Stone～Platinum）的阶段式落地策略
如何融入实际项目

目标是通过实际的代码示例，体验从测试迈向证明的进阶过程。

另外，本文出现的代码片段，已按章节整理成文件，作为参考代码集公开在GitHub上。

ada-spark-formal-verification - komurasoft-blog-samples (GitHub)

2. SPARK是什么 ── Ada的部分语言，也是通往证明世界的入口

SPARK是Ada的子集（部分语言）。

作为子集，其中有明确的意图。

Ada的全部功能 → 表达力很强，但对所有功能做形式化验证并不现实
SPARK        → 只聚焦于可验证的功能，让证明变得可行

SPARK主要限制的项目如下：

通过指针（访问类型）进行动态内存管理 → 以所有权模型控制
自由使用异常处理器                    → 有限制地允许
递归数据结构                          → 因难以证明而受限
自由使用任务                          → 以Ravenscar Profile限制

听到「限制」可能会觉得束手束脚。但这些限制正是换取可证明性的代价。

SPARK的工具集以AdaCore提供的GNATprove为核心。

GNATprove的运作流程：
1. 解析用SPARK写成的Ada代码
2. 将契约（Pre/Post）与断言转换为Why3中间语言
3. 交给Z3、CVC4、Alt-Ergo等自动证明器尝试证明
4. 将结果以源代码上的消息汇报

重要的是，SPARK是构建在Ada之上的。

SPARK代码 = Ada代码 + 契约注解

换言之，SPARK就是日常Ada开发的延伸，不需要重新学习特殊语法。

3. 安装GNATprove与第一次证明

首先要准备能运行GNATprove的环境。

使用Alire的话，可以用下面的命令创建支持SPARK的项目。

alr init --bin spark_demo
cd spark_demo

由于GNATprove随GNAT编译器一起提供，只要是能用alr build构建的环境，就能直接使用gnatprove命令。

先以返回绝对值的函数作为第一个证明对象。

package Simple_Proof with SPARK_Mode is

   function Abs_Value (X : Integer) return Integer
     with Post => Abs_Value'Result >= 0;

end Simple_Proof;

package body Simple_Proof with SPARK_Mode is

   function Abs_Value (X : Integer) return Integer is
   begin
      if X < 0 then
         return -X;
      else
         return X;
      end if;
   end Abs_Value;

end Simple_Proof;

整理一下值得注意的重点：

在包规约与包体两边都加上with SPARK_Mode
用Post条件声明「结果为0以上」这个性质
用'Result属性引用函数的返回值

对这段代码运行GNATprove。

gnatprove -P spark_demo.gpr

结果如下：

SUMMARY
-------
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
simple_proof.adb:5:15: info: range check proved
simple_proof.adb:6:16: info: range check proved
simple_proof.ads:3:19: info: postcondition proved

postcondition proved这条消息，意味着已证明对于所有Integer输入，返回值均为0以上。

这次体验，就是通往SPARK的入口。

4. 以契约进行设计的基础 ── Pre与Post的写法

SPARK的证明，从编写契约开始。

契约是Ada 2012的语言功能，但在SPARK中，它会成为证明的输入。

procedure Transfer (From, To : in out Account; Amount : Positive)
  with Pre  => From.Balance >= Amount,
       Post => From.Balance = From.Balance'Old - Amount
                and then
                To.Balance = To.Balance'Old + Amount;

整理Pre与Post的设计方针：

Pre（事前条件）：
  调用方的责任
  「只要满足这个条件调用，就保证Post成立」
  要足够宽松（让调用方能够满足），但也要视需要保持足够严谨

Post（事后条件）：
  实现方的责任
  「调用结束后的世界状态会是这样」
  可用'Old属性引用调用前的值
  太强会让实现变得局促，太弱则无法证明有用的性质

也一并整理常见的错误与对策。

错误1：Pre太强
  Pre => X > 0 and X < 100 and X /= 50 and ...
  → 要确认这是否是调用方永远都能满足的条件
  → 不要因为测试能通过，就把Pre收得太窄

错误2：Post太弱
  Post => True
  → 什么都没保证，证明就失去意义

错误3：忘记把副作用写进Post
  Post => Result = X * 2  （漏看了全局变量的更新）
  → 用Global/Depends契约明示副作用（第9章）

5. 溢出证明 ── 保证数值计算的安全性

在SPARK的证明中，实务上获益最大的其中一项就是防止溢出。

请看下面这段代码。

procedure Increment (X : in out Integer)
  with SPARK_Mode,
       Pre  => X < Integer'Last,
       Post => X = X'Old + 1;

关键在于Pre => X < Integer'Last。有了这个契约，GNATprove就能证明加法运算不会溢出。

若没有这个契约，GNATprove会针对溢出的可能性发出警告。

medium: overflow check might fail

更复杂的计算也是同样的道理。

function Average (A, B : Integer) return Integer
  with SPARK_Mode,
       Pre  => (if A >= 0 and B >= 0 then A <= Integer'Last - B
                elsif A < 0 and B < 0 then A >= Integer'First - B),
       Post => (if A <= B then A <= Average'Result and Average'Result <= B
                else B <= Average'Result and Average'Result <= A);

Pre看起来很复杂，但这其实是把「A与B的和不会溢出」这个条件，按符号情况分别列出而已。

重点：
  溢出证明的本质，就是在做加法/乘法之前，用Pre声明
  「结果会落在类型范围内」这个条件
  看起来麻烦，但只要写一次，就再也不用为溢出错误所苦

6. 循环不变式 ── 证明循环的性质

形式化验证中最困难的部分之一，就是循环的证明。

由于循环可能执行任意次数，测试无法覆盖所有情况。SPARK使用循环不变式（Loop Invariant）来进行证明。

function Sum_Of_Naturals (N : Natural) return Natural
  with SPARK_Mode,
       Post => Sum_Of_Naturals'Result = (N * (N + 1)) / 2;

function Sum_Of_Naturals (N : Natural) return Natural is
   Result : Natural := 0;
begin
   for I in 1 .. N loop
      Result := Result + I;
      pragma Loop_Invariant (Result = (I * (I + 1)) / 2);
   end loop;
   return Result;
end Sum_Of_Naturals;

设计循环不变式需要下列思路：

1. 写出在循环每次迭代开始时都成立的性质
2. 选择能在循环最后一次迭代结束后导出所需Post条件的性质
3. 不变式要用数学式表达到该时点为止的计算结果

接着再看一个数组搜索的例子。

function Find (Arr : Array_Of_Integer; Target : Integer) return Natural
  with SPARK_Mode,
       Post => (if Find'Result = 0 then
                  (for all K in Arr'Range => Arr (K) /= Target)
                else
                  Arr (Find'Result) = Target);

function Find (Arr : Array_Of_Integer; Target : Integer) return Natural is
begin
   for I in Arr'Range loop
      if Arr (I) = Target then
         return I;
      end if;
      pragma Loop_Invariant
        (for all K in Arr'First .. I => Arr (K) /= Target);
   end loop;
   return 0;
end Find;

这里的不变式是「到目前为止检查过的范围内不存在Target」。

循环不变式设计原则：
  用数学式表达「循环跑到第n次时，能说明什么」
  在数组循环中，常见的形式是「对于已处理的范围，~成立」
  不变式太强就证不出来，太弱则无法导出Post
  取得这个平衡，正是循环证明真正考验功力的地方

7. 断言指令 ── 写在代码中的局部性质

除了契约（Pre/Post）之外，SPARK也可以在代码中途写断言（Assert）。

procedure Divide (A, B : Integer; Q, R : out Integer)
  with SPARK_Mode,
       Pre  => B /= 0,
       Post => A = Q * B + R and R >= 0 and R < abs (B);

procedure Divide (A, B : Integer; Q, R : out Integer) is
begin
   Q := A / B;
   R := A rem B;

   pragma Assert (A = Q * B + R);
   pragma Assert (R >= 0);
   pragma Assert (R < abs (B));
end Divide;

整理各种编译指示（pragma）的使用区分：

Pre/Post：       子程序进出口的约定
Assert：         代码特定位置应该成立的性质
Loop_Invariant： 循环每次迭代都保持的性质
Loop_Variant：   用来证明循环必定会结束的递减量

Assert的应用场景如下：

确认复杂计算的中间结果
确认if/else分支后的状态
确认过程调用后返回值的性质
为后续的证明提供辅助引理

8. 数据流契约 ── Global与Depends

SPARK的强大功能之一，就是数据流契约。

用来明示子程序所读取/写入的全局变量。

package Counter_Unit with SPARK_Mode is

   Count : Natural := 0;

   procedure Increment
     with Global => (In_Out => Count);

   procedure Reset
     with Global => (Output => Count);

   function Get_Value return Natural
     with Global => (Input => Count);

end Counter_Unit;

Global契约有以下3种模式：

Input：  只读（适合函数）
Output： 只写（适合初始化）
In_Out： 读写皆有（适合更新）

此外，变量之间的依赖关系可以用Depends表达。

procedure Transfer
  (From, To : in out Account_Type)
  with Global => (Input => Exchange_Rate),
       Depends => (From =>+ (From, Exchange_Rate),
                   To   =>+ (To, Exchange_Rate));

=>+的意思是「除了先前的值之外，也依赖这些输入」。

数据流契约的优点：
  1. 一眼就能看出「这个函数会碰到什么」
  2. 可在编译期检测出非预期的副作用
  3. 成为变量信息流分析的输入
  4. 有助于在大型系统中将数据流向可视化

9. 证明等级 ── 从Stone到Platinum的阶段式落地

SPARK有一个证明等级（Proof Level）的概念。

如果想一次就完全证明所有代码，往往容易半途放弃。因此SPARK提供了逐步提升证明严谨程度的策略。

Stone（等级0）：
  只检查契约语法与类型的一致性
  应该最先达到的等级

Bronze（等级1）：
  Stone + 证明没有读取未初始化的变量
  基本正确性的保证

Silver（等级2）：
  Bronze + 证明不会发生运行时错误（越界、溢出、除以零）
  最实用的目标

Gold（等级3）：
  Silver + 证明Pre/Post条件
  完整功能正确性的保证

Platinum（等级4）：
  Gold + 证明数据的非依赖性、信息流
  适用于注重安全性的系统

实务上的落地策略如下：

第1阶段：让整个项目通过Stone等级
  → 找出契约写错的地方

第2阶段：让重要模块达到Silver等级
  → 消灭溢出与越界访问
  → 实务上大多数的错误都能在这一步防范

第3阶段：让核心逻辑达到Gold等级
  → 用数学方式保证功能正确性
  → 证明算法的正确性

第4阶段：若有安全性需求则进一步到Platinum
  → 检测信息泄露路径

10. 实务证明流程 ── 减少反复修改的工作流程

介绍在日常中使用GNATprove的工作流程。

1. 设计类型与规格
   确定范围约束、类型不变式

2. 编写契约（Pre/Post）
   在实现之前，先把规格表达为契约

3. 通过编译
   用GNAT解决编译错误

4. 以Stone等级运行GNATprove
   gnatprove -P proj.gpr --level=0

5. 确认警告，必要时修正契约
   特别注意初始化的疏漏

6. 以Silver等级为目标
   gnatprove -P proj.gpr --level=2
   消灭运行时错误

7. 若有循环，加入不变式
   若无法证明，确认不变式是否不足

8. 以Gold等级证明功能正确性
   gnatprove -P proj.gpr --level=3

以下是常见的「无法证明」情况及其对策。

情况1：「medium: postcondition might fail」
  → Post条件太强，或Pre条件太弱
  → 或者是循环不变式不足

情况2：「medium: overflow check might fail」
  → 用Pre条件限制数值范围
  → 或缩小类型本身的范围

情况3：「medium: array index check might fail」
  → 用不变式证明循环范围落在数组范围内
  → 使用for I in Arr'Range（有助于SPARK自动识别范围）

情况4：「prover timeout」
  → 证明器超时。用不变式分阶段拆解
  → 把函数拆得更小

11. SPARK与测试的搭配使用 ── 理解彼此的互补关系

形式化验证与测试并非对立，而是互补的关系。

SPARK的证明：
  对所有输入该性质皆成立
  只针对写在契约中的性质
  无法证明的情况，交由人工确认或测试处理

测试：
  对选定的输入确认实际运行情况
  也能发现契约中未写出的隐含前提
  能确认与运行环境的交互

以下是搭配使用的模式：

1. 用SPARK保证Silver等级（无运行时错误）
2. 用单元测试确认具体输入输出的正确性
3. 用Gold等级证明核心逻辑
4. 针对无法证明的部分集中编写测试

Ada有一个名为AUnit的单元测试框架。用SPARK固化类型与契约，再用AUnit测试行为，这种组合相当实用。

12. 阅读GNATprove的结果 ── 消息的解读

GNATprove的输出有以下3种等级。

info：    证明成功
medium：  无法证明（警告）。需要人工确认
high：    证明失败（错误）。很可能违反契约

以下是常见的消息及其含义。

「postcondition proved」           Post条件已被证明
「range check proved」             范围检查已被证明
「overflow check proved」          已证明不会发生溢出
「index check proved」             数组下标的范围已被证明
「divide by zero check proved」    已证明不会发生除以零

「might fail」                     无法证明
「cannot prove」                   证明器未能完成证明
「prover timeout」                 未在限制时间内完成证明

出现might fail时的处理步骤如下。

1. 阅读代码，判断是否真的可能失败
2. 若可能失败，修正代码
3. 若理应不会失败，强化契约（Pre/不变式）
4. 若仍无法证明，用pragma Assume声明为假设
   （但要注意，Assume是未经证明的假设）

13. 如何融入实际项目

以下是在现有项目中引入SPARK时较为现实的做法。

1. 从新代码开始
   不要试图一次把现有代码整体SPARK化
   从新编写的模块开始启用SPARK_Mode

2. 以Silver为目标
   Gold（完整功能证明）虽然理想，但先从Silver（无运行时错误）开始
   即使只是防止溢出，实务上的价值也非常大

3. 从接口开始编写契约
   在实现之前，先在包规约（.ads）中编写契约
   规格若已固定，任何实现者都能写出满足契约的代码

4. 融入CI/CD
   将gnatprove加入CI流水线
   证明失败时中止构建（或发出警告）

5. 积累证明报告
   用gnatprove --report=all生成报告
   追踪未证明项目的变化趋势

在混杂C/C++现有代码的项目中，下列阶段式做法相当有效。

1. 新模块用Ada/SPARK编写
2. 通过Interfaces.C与C/C++对接
3. 将重要的数据结构与验证逻辑迁移到SPARK
4. 逐步扩大SPARK的范围

14. SPARK的局限与注意事项

SPARK并非万能。诚实理解其局限，才能通往正确的应用方式。

可证明的范围：
  SPARK能证明的仅限于「写在契约中的性质」
  契约中的漏洞（忘记写的性质）不会被证明
  例：即使在Post中证明了已排序，若忘记写「不具破坏性」
  就无法保证原始元素被保留下来

证明器的局限：
  有些复杂的性质，自动证明器无法证明
  这时就需要依靠手动证明（如Coq）
  不过，在实务范围内，自动证明大多已经足够

语言的限制：
  大量使用指针的代码无法SPARK化
  动态内存分配的证明有限
  递归数据结构的证明较为困难

开发者的熟练度：
  编写契约需要训练
  循环不变式的设计特别需要时间才能掌握
  必须有整个团队的技能提升计划

15. 结语 ── 让证明成为日常开发的一部分

以上整理了SPARK形式化验证的实务内容。

SPARK是Ada的子集，聚焦于可证明的功能
契约（Pre/Post）成为证明的输入，可直接沿用Ada 2012的契约
GNATprove执行自动证明，并在源代码层面汇报结果
用循环不变式证明循环的性质
用Global/Depends明示数据流，管理副作用
可通过证明等级（Stone～Platinum）逐步提升严谨程度
先以Silver等级（无运行时错误）为目标，是较实用的做法
测试与证明并非对立，而是互补

或许有人会先入为主地认为「形式化验证很难，只适合特殊的项目」。

然而，如今SPARK与GNATprove的组合，已经达到下面这个层次。

1. 编写契约。这本质上与编写类型或测试是同样的设计工作
2. 运行gnatprove。感觉就跟编译差不多
3. 查看结果，修正代码或契约

这个循环，跟平常一边看编译器的错误消息一边修正代码的开发流程，其实没有任何不同。

不同之处在于，编译器保证的是「语法正确」，而GNATprove保证的是「在所有输入下都正确」。

上一篇文章介绍过的Ada口号——「错误不是用来找的，而是用类型与契约让它写不出来」——通过SPARK进入了下一个阶段。

错误的不存在，是由证明来保证的。

请先在一个小函数上加上SPARK_Mode与Post，然后运行gnatprove试试看。

当你看到postcondition proved那条绿色消息时，对软件质量保证的看法应该会为之改变。

参考资料

相关文章

共享相同标签的最新文章。可以围绕相近的主题进一步加深理解。

常见问题

汇总了咨询这一主题时常见的问题。

SPARK是什么？和Ada是什么关系？
SPARK是Ada的子集（部分语言），设计目的是让程序的性质可以用数学方式证明。它限制了指针的动态内存管理、自由使用异常等功能，以换取可证明性。SPARK代码就是Ada代码加上契约注解，因此属于日常Ada开发的延伸，不需要重新学习特殊语法。工具方面以AdaCore提供的GNATprove为核心，它会将契约转换为Why3中间语言，再交给Z3等自动证明器尝试证明。
形式化验证与测试有什么区别？
测试确认的是「对于选定的输入能正确运行」，形式化验证则是用数学方式证明「对于所有输入该性质都成立」。由于输入的组合是无限的，仅靠测试无法证明在所有输入下都正确。不过两者并非对立而是互补：用SPARK保证Silver等级（无运行时错误），再用单元测试确认具体的输入输出，并针对无法证明的部分集中编写测试，这种搭配方式相当实用。
SPARK的证明等级（Stone～Platinum）是什么？
这是逐步提高证明严谨程度的概念。Stone只检查契约语法与类型的一致性，Bronze证明没有读取未初始化的变量，Silver证明不会发生运行时错误（越界、溢出、除以零），Gold通过证明Pre/Post条件达成完整的功能正确性，Platinum则再加上信息流的证明，是注重安全性的等级。实务上，先以Silver等级为目标被视为最实用的做法。
当GNATprove无法完成证明时该怎么办？
按消息类型分别处理。「postcondition might fail」的原因是Post条件太强、Pre条件太弱，或循环不变式不足。「overflow check might fail」可以用Pre条件限制数值范围，或缩小类型本身的范围。「array index check might fail」要用不变式证明循环范围落在数组范围内。「prover timeout」可以用不变式将证明分阶段拆解，或把函数拆得更小。第一步永远是阅读代码，判断是否真的可能失败。

作者简介

本文作者的个人简介页面。

Go Komura

小村软件有限公司 代表

以 Windows 软件开发、技术咨询与故障排查为中心，擅长难以复现的故障调查，以及既有资产仍在运行的项目。

联系我们
返回博客列表