小村軟體有限公司
日本語 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那則綠色訊息時，對軟體品質保證的看法應該會為之改變。

參考資料

相關文章

共用相同標籤的最新文章。能以相近的主題延伸理解。

Ada 的安全並行處理 ── 任務與保護物件實戰指南

本文是 Ada 語言內建並行處理機制──任務(task)與保護物件(protected object)的實戰入門文章。內容涵蓋會合(entry/accept)、選擇性接受(select)、生產者消費者模式、保護物件實現的排他控制、帶屏障的保護入口、附逾時的呼叫，以及任務優先...

閱讀文章

相關主題

與本文相近的主題頁面。以本文為起點，可進一步連到相關服務與其他文章。

常見問題

整理諮詢這個主題時常見的問題。

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 軟體開發、技術諮詢與故障調查為中心，在難以重現的故障調查與既有資產仍在運作的專案上具有優勢。

聯絡我們
回到部落格一覽