fbpx
维基百科

斷言 (程式)

十二月 31, 2023

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

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

x := 5; {x > 0} x := x + 1 {x > 1}

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

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

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

x = 5; x = x + 1; // {x > 1}

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

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

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

用途 编辑

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

契約式設計中的斷言 编辑

斷言可以當做是一種軟體的文档：斷言可以描述程式執行前預期的情形（先驗條件）以及執行後的預期的結果（後驗條件（英语：postcondition））。斷言也可以描述類別中的不變量。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 (程式標準版本)（英语：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，程式會立刻中止執行。

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

相關條目 编辑

參考資料 编辑

  1. ^ C.A.R. Hoare, An axiomatic basis for computer programming （页面存档备份，存于互联网档案馆）, Communications of the ACM, 1969.
  2. ^ Jon Jagger, Compile Time Assertions in C （页面存档备份，存于互联网档案馆）, 1999.
  3. ^ GNU, "GCC 4.3 Release Series — Changes, New Features, and Fixes （页面存档备份，存于互联网档案馆）"

外部連結 编辑

  • The benefits of programming with assertions （页面存档备份，存于互联网档案馆） by Philip Guo (Stanford University), 2008.
  • Java:

十二月 31, 2023
斷言, 程式, 此條目需要补充更多来源, 2015年7月19日, 请协助補充多方面可靠来源以改善这篇条目, 无法查证的内容可能會因為异议提出而被移除, 致使用者, 请搜索一下条目的标题, 来源搜索, 网页, 新闻, 书籍, 学术, 图像, 以检查网络上是否存在该主题的更多可靠来源, 判定指引, 在程式設計中, 斷言, assertion, 是一種放在程式中的一階邏輯, 如一個結果為真或是假的邏輯判斷式, 目的是為了標示與驗證程式開發者預期的結果, 當程式執行到斷言的位置時, 對應的斷言應該為真, 若斷言不為真時, . 此條目需要补充更多来源 2015年7月19日 请协助補充多方面可靠来源以改善这篇条目 无法查证的内容可能會因為异议提出而被移除 致使用者 请搜索一下条目的标题 来源搜索 斷言 程式 网页 新闻 书籍 学术 图像 以检查网络上是否存在该主题的更多可靠来源 判定指引 在程式設計中 斷言 assertion 是一種放在程式中的一階邏輯 如一個結果為真或是假的邏輯判斷式 目的是為了標示與驗證程式開發者預期的結果 當程式執行到斷言的位置時 對應的斷言應該為真 若斷言不為真時 程式會中止執行 並給出錯誤訊息 例如 以下的程式包括二個斷言 x 5 x gt 0 x x 1 x gt 1 x gt 0及x gt 1 當程式執行到二個斷言對應的位置時 斷言的內容均為真 程式設計者可以用斷言來標示程式 提供程式正確性的相關資訊 例如在一段程式前加入斷言 先驗條件 說明這段程式執行前預期的狀態 或在一段程式後加入斷言 後驗條件 英语 postcondition 說明這段程式執行後預期的結果 以下的範例使用東尼 霍爾在1969年論文中提出的斷言標示方式 1 x 5 x x 1 x gt 1 以上註解中的大括號表示為斷言 不是一般的註解 現有的主流程式語言不支援上述的標示方式 不過程式設計者仍可以用註解的方式標示斷言 標示此時應該成立的條件 只是此斷言沒有檢查機能 不成立時程式不會中止執行 許多現代的程式語言已支援有檢查機能的斷言 可能是執行期或其他時間檢查的陳述 若在執行期中有斷言不成立 會出現斷言失敗 一般會停止程式的執行 程式設計者可以專注在斷言失敗 邏輯不一致的部份 並設法修正 斷言的使用有助於程式設計者設計 開發及理解程式 目录 1 用途 1 1 契約式設計中的斷言 1 2 執行期檢查的斷言 1 3 在開發過程中使用斷言 1 4 靜態斷言 2 關閉斷言機能 3 和錯誤處理的比較 4 相關條目 5 參考資料 6 外部連結用途 编辑在開發Eiffel語言的程式時 斷言是設計過程中的一部份 像C語言或Java等程式語言 主要在執行期檢查斷言是否正確 也可以用靜態斷言的方式 在編譯期檢查斷言 不論是哪一種情形 都可以檢查斷言的有效性 也可以關閉斷言檢查的機能 契約式設計中的斷言 编辑 斷言可以當做是一種軟體的文档 斷言可以描述程式執行前預期的情形 先驗條件 以及執行後的預期的結果 後驗條件 英语 postcondition 斷言也可以描述類別中的不變量 Eiffel程式語言將斷言和程式整合 也可以自動將程式中的斷言抽出 形成程式的文件 這是契約式設計的重要特性 以下是一個Eiffel語言的程式 其中require及ensure分別標示程式的先驗條件及後驗條件 set hour a hour INTEGER Set hour to a hour require valid argument a hour gt 0 and a hour lt 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語言的斷言是在標準的開頭檔 a href Assert h html title Assert h assert h a 中定義 其斷言assert i assertion i 是一個巨集 若條件不成立時產生錯誤 並且中止程式執行 C 語言的斷言需配合開頭檔 a href Cassert html class mw redirect title Cassert cassert a 不過有些C 的函式庫也開頭檔 a href Assert h html title Assert h assert h a 上述斷言的缺點是可能有改變記憶體資料或是執行緒時序的風險 因此需小心的處理斷言 確認斷言在程式中沒有其他的副作用 程式結構中的斷言有助於在不使用第三方程式庫的情形下 應用測試驅動開發的開發方式 在開發過程中使用斷言 编辑 在軟體開發過程中 程式設計者一般會在斷言有效的情形下執行或測試程式 若出現斷言錯誤 程式設計者會立刻注意到此問題 許多斷言的實現方式會中止程式的執行 這功能方便程式設計者處理問題 若在錯誤出現後程式繼續執行 往往更不容易找到有問題程式的位置 斷言錯誤一般也會顯示一些資訊 例如錯誤程式的位置 也許包括堆疊追踪 若環境支持核心文件或是在調試工具中執行 可能還可以提供程式的完整狀態 程式設計者可以配合這些資訊來修正程式的錯誤 是在除錯過程中很有利的工具 靜態斷言 编辑 只在編譯期間檢查的斷言稱為靜態斷言 靜態斷言必需配合清楚的註解說明 在編譯期的模板超編程時 靜態斷言特別有用 靜態斷言也可以用在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 程式標準版本 英语 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 程式會立刻中止執行 比較理想的錯誤處理方式是配置到記憶體時另外由程式處理 例如伺服器可能有數個客戶端 可能有一些資源保留 尚未釋放 也可能有一些修改尚未寫入資料庫 此時較好的處理方法只讓單一的交易失敗 出現錯誤訊息 而不是直接中止程式的執行 相關條目 编辑邏輯斷言 斷言定義語言 英语 Assertion definition language 契约式设计 異常處理 霍尔逻辑 靜態程序分析 Java 建模语言 英语 Java Modeling Language Assert h參考資料 编辑 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 Programming With Assertions in Java 页面存档备份 存于互联网档案馆 取自 https zh wikipedia org w index php title 斷言 程式 amp oldid 75128403, 维基百科，wiki，书籍，书籍，图书馆，

文章

，阅读，下载，免费，免费下载，mp3，视频，mp4，3gp， jpg，jpeg，gif，png，图片，音乐，歌曲，电影，书籍，游戏，游戏。