斷言 (程式)
![本頁使用了標題或全文手工轉換](http://images.weserv.nl/?url=//upload.wikimedia.org/wikipedia/commons/thumb/c/cd/Zh_conversion_icon_m.svg/35px-Zh_conversion_icon_m.svg.png)
此條目需要補充更多來源。 (2015年7月19日) |
在程式設計中,斷言(assertion)是一種放在程式中的一階邏輯(如一個結果為真或是假的邏輯判斷式),目的是為了標示與驗證程式開發者預期的結果-當程式執行到斷言的位置時,對應的斷言應該為真。若斷言不為真時,程式會中止執行,並給出錯誤訊息。
例如,以下的程式包括二個斷言:
x := 5;
{x > 0}
x := x + 1
{x > 1}
x > 0
及x > 1
,當程式執行到二個斷言對應的位置時,斷言的內容均為真。
程式設計者可以用斷言來標示程式,提供程式正確性的相關資訊。例如在一段程式前加入斷言(先驗條件),說明這段程式執行前預期的狀態。或在一段程式後加入斷言(後驗條件),說明這段程式執行後預期的結果。
以下的範例使用東尼·霍爾在1969年論文中提出的斷言標示方式[1]。
x = 5;
x = x + 1;
// {x > 1}
以上註解中的大括號表示為斷言,不是一般的註解。現有的主流程式語言不支援上述的標示方式,不過程式設計者仍可以用註解的方式標示斷言,標示此時應該成立的條件,只是此斷言沒有檢查機能,不成立時程式不會中止執行。
許多現代的程式語言已支援有檢查機能的斷言,可能是執行期或其他時間檢查的陳述。若在執行期中有斷言不成立,會出現斷言失敗,一般會停止程式的執行。程式設計者可以專注在斷言失敗,邏輯不一致的部份,並設法修正。
斷言的使用有助於程式設計者設計、開發及理解程式。
用途
在開發Eiffel語言的程式時,斷言是設計過程中的一部份。像C語言或Java等程式語言,主要在執行期檢查斷言是否正確,也可以用靜態斷言的方式,在編譯期檢查斷言。不論是哪一種情形,都可以檢查斷言的有效性,也可以關閉斷言檢查的機能。
契約式設計中的斷言
斷言可以當做是一種軟體的文件:斷言可以描述程式執行前預期的情形(先驗條件)以及執行後的預期的結果(後驗條件)。斷言也可以描述類別中的不變數。Eiffel程式語言將斷言和程式整合,也可以自動將程式中的斷言抽出,形成程式的檔案。這是契約式設計的重要特性。以下是一個Eiffel語言的程式,其中require
及ensure
分別標示程式的先驗條件及後驗條件。
set_hour (a_hour: INTEGER)
-- Set `hour' to `a_hour'
require
valid_argument: a_hour >= 0 and a_hour <= 23
do
hour := a_hour
ensure
hour_set: hour = a_hour
end
斷言可以用敘述的方式放在程式中,也可以用註解的方式標示。不過斷言若用註解的方式標示,在斷言和程式未同步更新時比較容易讓設計者發現問題。有斷言敘述的程式會可以在每次程式執行時,自動檢查斷言是否成立,若斷言不成立時,就會輸出錯誤訊息。因此避免了程式和斷言未同步更新的問題。
執行期檢查的斷言
在程式執行時,可以用斷言檢查程式開發時的假設,確認這些假設是否成立。考慮以下的Java程式:
int total = countNumberOfUsers();
if (total % 2 == 0) {
// total is even
} else {
// total is odd and non-negative
assert(total % 2 == 1);
}
在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語言的程式中,當斷言不成立時,產生有錯誤的程式碼。例如以下就是一個定義靜態斷言的方法:
#define COMPILE_TIME_ASSERT(pred) switch(0){case 0:case pred:;}
COMPILE_TIME_ASSERT( BOOLEAN CONDITION );
若(BOOLEAN CONDITION)
的成果不為真,上述程式中會有二個相同的case標記,因此編譯器會出現錯誤。此處的布林運算式是要在編譯階段就可以確定的運算式,例如(sizeof(int)==4)
等。此結構無法放在函式範圍以外,因此若要執行此斷言時,必需將此斷言放在一個函式以內。
另一個常使用的靜態斷言方式如下[2]:
static char const static_assertion[ (BOOLEAN CONDITION)
? 1 : -1
] = {'!'};
若(BOOLEAN CONDITION)
的成果不為真,由於無法定義長度為負值的陣列,因此編譯器會出現錯誤。即使編譯器真的允許負值長度,後續的初始化字元應該也會使編譯器出現錯誤訊息。此處的布林運算式是要在編譯階段就可以確定的運算式,例如(sizeof(int)==4)
等。
上述的方式都需要唯一不重覆的名稱。現代的編譯器支援__COUNTER__的預處理器定義,在每次使用到此定義時,回傳一個每次會加一的數值,因此可以產生唯一不重覆的名稱[3]。
C11 (程式標準版本)及C++11可以用static_assert
支援靜態斷言。
關閉斷言機能
大部份的程式語言可以用設定啟動或關閉所有的斷言,有時也可以啟動或關閉個別的斷言。一般會在開發過程中啟動斷言,在最後測試完成,要發行正式版本給客戶時會關閉斷言。在不考慮斷言副作用的前提下,關閉斷言不作檢查可以節省評估斷言需要的程式碼,在正常情形下程式仍有相同的結果。在異常的情形下,關閉斷言檢查會使得原來可能會停止的程式可以繼續執行,有時這會是比較可接受的結果。
C語言及C++可以利用預處理器在編譯階段完全關閉斷言。Java語言若要啟動斷言,需要在運行期引擎中設定特定選項,若選項未設定,不會啟動斷言,不過斷言仍存在程式中,只有在用在運行期用JIT編譯器中進行最佳化,或是在編譯期使用if(false)的條件,才能排除斷言執行。
和錯誤處理的比較
有必要去區分斷言和錯誤處理程式的差異。斷言只用在標示一些邏輯上不可能或不應該出現的情形,若上述情形真的出現時,表示有些基本架構已出現問題。這和錯誤處理不同,大部份錯誤的條件都是有可能出現的,只是實務上出現頻率很低。斷言不宜作為通用的錯誤處理程式,因為斷言一般會中止程式的執行,程式無法恢復到沒有錯誤發生前的情形,而且斷言顯示的訊息只對程式設計者有幫助,對使用者的幫助不大。
考慮以下用斷言處理錯誤的程式。
int *ptr = malloc(sizeof(int) * 10);
assert(ptr);
// use ptr
...
作業系統不保證每一次執行malloc
都會成功,若無法組態到記憶體,malloc
會傳回NULL
pointer,程式會立刻中止執行。
比較理想的錯誤處理方式是組態到記憶體時另外由程式處理。例如伺服器可能有數個客戶端,可能有一些資源保留,尚未釋放,也可能有一些修改尚未寫入資料庫。此時較好的處理方法只讓單一的交易失敗,出現錯誤訊息,而不是直接中止程式的執行。
相關條目
參考資料
- ^ C.A.R. Hoare, An axiomatic basis for computer programming (頁面存檔備份,存於網際網路檔案館), Communications of the ACM, 1969.
- ^ Jon Jagger, Compile Time Assertions in C (頁面存檔備份,存於網際網路檔案館), 1999.
- ^ GNU, "GCC 4.3 Release Series — Changes, New Features, and Fixes (頁面存檔備份,存於網際網路檔案館)"
外部連結
- The benefits of programming with assertions (頁面存檔備份,存於網際網路檔案館) by Philip Guo (Stanford University), 2008.
- Java: