斷言_(程式)

在程式設計中，**斷言**（assertion）是一種放在程式中的一階邏輯（如一個結果為真或是假的邏輯判斷式），目的是為了標示與驗證程式開發者預期的結果－當程式執行到斷言的位置時，對應的斷言應該為真。若斷言不為真時，程式會中止執行，並給出錯誤訊息。

例如，以下的程式包括二個斷言：

`x > 0` 及 `x > 1`，當程式執行到二個斷言對應的位置時，斷言的內容均為真。

程式設計者可以用斷言來標示程式，提供程式正確性的相關資訊。例如在一段程式前加入斷言（先驗條件），說明這段程式執行前預期的狀態。或在一段程式後加入斷言（後驗條件），說明這段程式執行後預期的結果。

以下的範例使用東尼・霍爾在 1969 年論文中提出的斷言標示方式。

以上註解中的大括號表示為斷言，不是一般的註解。現有的主流程式語言不支援上述的標示方式，不過程式設計者仍可以用註解的方式標示斷言，標示此時應該成立的條件，只是此斷言沒有檢查機能，不成立時程式不會中止執行。

許多現代的程式語言已支援有檢查機能的斷言，可能是執行期或其他時間檢查的陳述。若在執行期中有斷言不成立，會出現斷言失敗，一般會停止程式的執行。程式設計者可以專注在斷言失敗，邏輯不一致的部份，並設法修正。

斷言的使用有助於程式設計者設計、開發及理解程式。

## 用途

在開發 Eiffel 語言的程式時，斷言是設計過程中的一部份。像 C 語言或 Java 等程式語言，主要在執行期檢查斷言是否正確，也可以用靜態斷言的方式，在編譯期檢查斷言。不論是哪一種情形，都可以檢查斷言的有效性，也可以關閉斷言檢查的機能。

### 契約式設計中的斷言

斷言可以當做是一種軟體的文件：斷言可以描述程式執行前預期的情形（先驗條件）以及執行後的預期的結果（後驗條件）。斷言也可以描述類別中的不變數。Eiffel 程式語言將斷言和程式整合，也可以自動將程式中的斷言抽出，形成程式的檔案。這是契約式設計的重要特性。以下是一個 Eiffel 語言的程式，其中 `require` 及 `ensure` 分別標示程式的先驗條件及後驗條件。

斷言可以用敘述的方式放在程式中，也可以用註解的方式標示。不過斷言若用註解的方式標示，在斷言和程式未同步更新時比較容易讓設計者發現問題。有斷言敘述的程式會可以在每次程式執行時，自動檢查斷言是否成立，若斷言不成立時，就會輸出錯誤訊息。因此避免了程式和斷言未同步更新的問題。

### 執行期檢查的斷言

在程式執行時，可以用斷言檢查程式開發時的假設，確認這些假設是否成立。考慮以下的 Java 程式：

在 Java 語言中，`%` 為餘數的運算子，若其第一個運算元為負，其結果也為負值。程式設計者假設 `total` 為非負值，因此除以 2 的餘數只可能是 0 或是 1，使用斷言可以使這個假設變得明確，若 `countNumberOfUsers` 傳回負值，程式會出現錯誤。

此作法的最大好處是當程式出現錯誤時，程式立刻停止執行，而不會在較晚的時間才中止執行，而斷言錯誤時會回報錯誤程式碼的位置，因此程式設人計者可以很快找到錯誤所在的位置。

斷言有時也會放在程式未預期會執行到的部份。例如，若 `switch` 敘述中所有可能的狀態都有對應的 `case` 敘述，不會執行到 `default` 敘述，此時可以在 `default` 敘述中加入一個條件不會成立的斷言，當程式執行到 `default` 敘述時會立刻停止執行，而不會使程式繼續在一個錯誤的狀態下執行。

Java 語言在 1.4 版以後支援斷言機能，若程式執行時有設定對應旗標，斷言錯誤時會產生 `AssertionError`，若未設定對應旗標，則會省略斷言敘述。C 語言的斷言是在標準的開頭檔 `assert.h` 中定義，其斷言 `assert (_assertion_)` 是一個巨集，若條件不成立時產生錯誤，並且中止程式執行。C++ 語言的斷言需配合開頭檔 `cassert`，不過有些 C++ 的函式庫也開頭檔 `assert.h`。

上述斷言的缺點是可能有改變記憶體資料或是執行緒時序的風險，因此需小心的處理斷言，確認斷言在程式中沒有其他的副作用。

程式結構中的斷言有助於在不使用第三方程式庫的情形下，應用測試驅動開發的開發方式。

### 在開發過程中使用斷言

在軟體開發過程中，程式設計者一般會在斷言有效的情形下執行或測試程式。若出現斷言錯誤，程式設計者會立刻注意到此問題。許多斷言的實現方式會中止程式的執行，這功能方便程式設計者處理問題，若在錯誤出現後程式繼續執行，往往更不容易找到有問題程式的位置。斷言錯誤一般也會顯示一些資訊，例如錯誤程式的位置，也許包括堆疊追蹤，若環境支援核心檔案或是在除錯工具中執行，可能還可以提供程式的完整狀態，程式設計者可以配合這些資訊來修正程式的錯誤，是在除錯過程中很有利的工具。

### 靜態斷言

只在編譯期間檢查的斷言稱為靜態斷言，靜態斷言必需配合清楚的註解說明。

在編譯期的模板超程式設計時，靜態斷言特別有用。靜態斷言也可以用在 C 語言的程式中，當斷言不成立時，產生有錯誤的程式碼。例如以下就是一個定義靜態斷言的方法：

若 `(BOOLEAN CONDITION)` 的成果不為真，上述程式中會有二個相同的 case 標記，因此編譯器會出現錯誤。此處的布林運算式是要在編譯階段就可以確定的運算式，例如 `(sizeof(int)==4)` 等。此結構無法放在函式範圍以外，因此若要執行此斷言時，必需將此斷言放在一個函式以內。

另一個常使用的靜態斷言方式如下：

若 `(BOOLEAN CONDITION)` 的成果不為真，由於無法定義長度為負值的陣列，因此編譯器會出現錯誤。即使編譯器真的允許負值長度，後續的初始化字元應該也會使編譯器出現錯誤訊息。此處的布林運算式是要在編譯階段就可以確定的運算式，例如 `(sizeof(int)==4)` 等。

上述的方式都需要唯一不重覆的名稱。現代的編譯器支援 \_\_COUNTER\_\_的預處理器定義，在每次使用到此定義時，回傳一個每次會加一的數值，因此可以產生唯一不重覆的名稱。

C11 (程式標準版本) 及 C++11 可以用 `static_assert` 支援靜態斷言。

## 關閉斷言機能

大部份的程式語言可以用設定啟動或關閉所有的斷言，有時也可以啟動或關閉個別的斷言。一般會在開發過程中啟動斷言，在最後測試完成，要發行正式版本給客戶時會關閉斷言。在不考慮斷言副作用的前提下，關閉斷言不作檢查可以節省評估斷言需要的程式碼，在正常情形下程式仍有相同的結果。在異常的情形下，關閉斷言檢查會使得原來可能會停止的程式可以繼續執行，有時這會是比較可接受的結果。

C 語言及 C++ 可以利用預處理器在編譯階段完全關閉斷言。Java 語言若要啟動斷言，需要在運行期引擎中設定特定選項，若選項未設定，不會啟動斷言，不過斷言仍存在程式中，只有在用在運行期用 JIT 編譯器中進行最佳化，或是在編譯期使用 if (false) 的條件，才能排除斷言執行。

## 和錯誤處理的比較

有必要去區分斷言和錯誤處理程式的差異。斷言只用在標示一些邏輯上不可能或不應該出現的情形，若上述情形真的出現時，表示有些基本架構已出現問題。這和錯誤處理不同，大部份錯誤的條件都是有可能出現的，只是實務上出現頻率很低。斷言不宜作為通用的錯誤處理程式，因為斷言一般會中止程式的執行，程式無法恢復到沒有錯誤發生前的情形，而且斷言顯示的訊息只對程式設計者有幫助，對使用者的幫助不大。

考慮以下用斷言處理錯誤的程式。

作業系統不保證每一次執行 `malloc` 都會成功，若無法組態到記憶體，`malloc` 會傳回 `NULL` pointer，程式會立刻中止執行。

比較理想的錯誤處理方式是組態到記憶體時另外由程式處理。例如伺服器可能有數個客戶端，可能有一些資源保留，尚未釋放，也可能有一些修改尚未寫入資料庫。此時較好的處理方法只讓單一的交易失敗，出現錯誤訊息，而不是直接中止程式的執行。

## 相關條目

* 邏輯斷言
* 斷言定義語言
* 契約式設計
* 異常處理
* 霍爾邏輯
* 靜態程式分析
* Java 建模語言
* Assert.h

## 參考資料

## 外部連結

* _The benefits of programming with assertions （頁面存檔備份，存於網際網路檔案館）_ by Philip Guo (Stanford University), 2008.
* Java:
  * Programming With Assertions in Java （頁面存檔備份，存於網際網路檔案館）