計算機程式設計/契約式設計

這篇文章關於 DbC 比其兄弟更關注契約式設計。原因是 Eiffel 的 DbC（以及極少數其他語言的 DbC）提供了與語言所有方面的完整 DbC 的緊密整合，以及語言的定義。

契約式設計

»沒有我的抽象資料型別，不行！«

首先，契約式設計適用於模組、模組中的例程、子例程中的迴圈以及語句之間。異常也涉及其中。也就是說，你不能有部分契約。契約涉及在每個細化級別上的整個模組。

如果你建立了一個模組(!) 契約，契約的條款將應用於整個模組在其整個生命週期中。如果你使用一個有契約的模組，你就有義務遵守其可見規則。

模組有兩種檢視：客戶端檢視和供應商檢視。當你編寫一個子例程，並且該子例程呼叫包含在某個模組中的其他子例程時，你的子例程就變成了該模組的客戶端。客戶端看到模組契約的兩個部分：

模組的不變式，以及
模組子例程的前置條件和後置條件。

從客戶端的角度來看，模組本身被認為是供應商，它提供子例程。供應商看到更多模組，並新增一些內部契約條款，可以說。供應商必須提供，即編寫：

模組的不變式，
模組子例程的前置條件和後置條件，
迴圈不變式和迴圈變體，
檢查指令，
一致的異常處理。

所有這些都是斷言，或者，在異常的情況下，與斷言一致。

檢視此處每個語言支援的設施： w:契約式設計.

斷言

斷言的目的是雙重的：首先，它宣告（計算的）變數及其關係的預期值。其次，它有助於測試變數是否具有宣告的值，以及關係是否確實為真。作為程式的一部分，斷言可以用作變數及其關係的執行時檢查。但同時，斷言允許在程式執行之前對其進行推理。你使用斷言來證明一個模組、子例程、迴圈等是正確的。

每個斷言都是一個布林表示式，並且要麼為True，要麼為False。示例：

 $s=0$  or else  $g(s)=2*t$

示例中涉及兩個變數的兩個關係，一些值是計算出來的。兩個相等測試要麼為True，要麼為False，並且透過或連線起來，這是一個布林運算子。

如果將其應用於模組級別，斷言可以表達客戶端在呼叫模組子例程時必須滿足的要求。這些要求以子例程的前置條件的形式宣告，即涉及子例程形式引數以及可能模組的其他特徵的斷言。作為回報，子例程的後置條件描述了子例程將作為結果提供的服務。同樣，後置條件是使用涉及子例程結果以及可能模組的其他特徵的斷言來表達的。典型的子例程描述，模組契約的一部分，可能如下所示：

  pop
        --  remove the topmost item
     require
        has_items: not is_empty
     ensure
        one_less: count = old count - 1

子例程pop不接受引數，也不返回任何內容。但是，它修改了模組，一個棧。因此，前置條件和後置條件是引用模組其他特徵的斷言，is_empty 和 count。有用的名稱被附加到斷言以供參考。

為了完成契約，在模組級別添加了另一個斷言，模組不變式。模組不變式的關係透過說明在呼叫模組的子例程的每次呼叫之間保證了什麼，來告知客戶端模組的狀態。示例：

 invariant
    sensible_count: count >= 0

契約違反是指評估為False 的斷言。通常，當程式無法滿足其斷言時，會引發異常，因為程式顯然是錯誤的。然後使用語言提供的異常機制來處理這種情況，並由契約式設計要求的規則約束。

在某些情況下，可以在編譯時執行基於斷言的廣泛程式分析。這相當於機械地證明某些檢查是不必要的。然後可以從編譯後的程式中省略這些檢查。請參閱 w:SPARK 程式語言.

如果斷言為假，則程式中存在錯誤！

原因是程式沒有根據斷言產生應有的結果。以下是契約式設計中可能的斷言列表（C 表示對客戶端可見（模組外部），S 表示對供應商可見（模組內部））

模組不變式（C, S）: 模組不變式斷言模組初始化後什麼為真。它們還斷言在執行其任何子程式之前和之後，相同的真值成立。
前置條件（C, S）: 子程式的前置條件宣告在呼叫子程式之前必須為真。通常，它表達了（計算的）模組變數和子程式引數之間的關係。只有在前置條件為真時，子程式才能執行以滿足其後置條件。
後置條件（C, S）: 後置條件宣告子程式成功完成時（計算的）變數和關係將為真。
（迴圈變體）（S）: 迴圈變體是一個表示式（型別為自然數），其值在迴圈的每次迭代中都減小到零。通常使用迴圈中的一個變數來表達這種特性。迴圈變體保證了終止。
迴圈不變式（S）: 迴圈不變式表達一個關係，該關係在進入迴圈時或再次進入迴圈時為真。該關係將命名迴圈感興趣的變數。
檢查（S）: 當語句執行完畢後，它很可能透過賦值改變了若干變數的值。檢查表達了程式設計師對賦值後這些變數之間關係的期望。

子程式的前置條件 P 和後置條件 QS從 Hoare 三元組的意義上構建子程式

{至少為 P} S {保證為 Q}，

前提是在呼叫之前和之後模組不變式為 True！注意最後一個要求。模組必須處於已知良好狀態，因為前置條件和後置條件可能引用模組的狀態。

契約式設計不是輸入檢查

按照推斷，上面關於錯誤斷言的規則意味著斷言不能用來代替輸入驗證。當你不信任你的輸入時，請在條件語句中使用你的語言提供的工具，例如 Ada 中的 'Valid 屬性。例如，呼叫 Sqrt(x)，其中 x = -1.23，這是使用Sqrt的一個錯誤，違反了契約。呼叫者沒有在將 x 傳送到數學例程之前測試 x。

斷言不能代替條件語句

你能將各種數字傳遞給Sqrt，並只准備處理當Sqrt的前置條件評估為 false 時引發的異常嗎？換句話說，你能故意無視契約嗎？答案是否定的，至少有兩個原因。

如果一個模組已被證明是正確的，則斷言檢查可能已被關閉，期望客戶端會履行其契約義務。呼叫者的契約違反可能會被忽視，並可能產生巨大的錯誤計算。
如果被呼叫的子程式不是Sqrt，而是控制火車的速度，你不能只是傳遞無效輸入，直到它沒有使速度控制子程式因異常而失敗。更糟糕的是，請參閱 1。

示例：棧

（這個例子是用非常簡化的 Ada 符號給出的，知道 Ada 2005 中的 DbC 支援非常好，但有限制。想象一下，將 require、ensure 和 invariant 替換為標記為pre, post和inv的註釋，將使以下內容更接近 Eiffel 原版。使用你的語言提供的工具來表達斷言和異常處理。）

下面的感嘆號（`!'）只是一個符號。它們代表各個語言提供的工具。它們的含義只是契約的資訊。

generic
   type Item is private;
   --  any definite type that permits assignment

package Stack is

   --  last in first out storage, initially empty

   function is_empty return Boolean;
   --  is there an element on the stack?
   --  ! post: result = (count = 0)

   function count return Natural;
   --  number of items currently on the stack

   function top return Item;
   --  the topmost item
   --  ! pre: not is_empty

   procedure push(x: Item);
   --  add `x` on top of the stack
   --  ! post: count = old count + 1
   --  ! post: not is_empty
   --  ! post: top = x

   procedure pop;
   --  remove the topmost item
   --  ! pre: not is_empty
   --  ! post: count = old count - 1


   --  ! inv: count >= 0
   --  ! inv: (count = 0) = is_empty

end Stack;

請注意，到目前為止，模組中還沒有可執行語句。它只是一個包含契約式先決條件和後置條件以及模組不變式的包規範。然而，就該模組的客戶端而言，模組的契約是完整的。

top 函式的先決條件宣告堆疊上必須存在元素，否則它無法成功。為了表達這一點，它引用了同一個模組中的另一個函式 is_empty。注意模組不變式允許空堆疊。count 函式既沒有先決條件也沒有後置條件，但它在模組不變式中被提及。這意味著客戶端仍然可以預期 count 返回一個 >= 0 的值。

現在，如果 is_empty = False，那麼根據 count >= 0，count > 0 必須為真，因為not is_empty 當且僅當 count /= 0。

如果您最終使用語言定義中的斷言和規則證明軟體元件，那麼該元件就符合這些契約的意義。

模組的內部檢視，在本例中是包體，展示瞭如何在程式中放置斷言。重要的是要理解pragma assert 在 Ada 中，require 在 Eiffel 中，等等，與語言的異常處理機制緊密整合。這與您可能從 C 的 assert 中推測的情況不同。（示例堆疊的實現實際上是基於 Ada.Containers，類似於 Eiffel 的 STACK 類通常是如何實現的。它也可以基於 D 的 arrays，或者您選擇的任何語言。）

pragma Assertion_Policy(Check);
  ...
   s: Vector;
  ...
   function top return Item is
   begin
      pragma assert(not is_empty, "stack is empty");
      return s.Last_Element;
   end top;

考慮一下開啟或關閉斷言檢查的效果。斷言表達契約，它們不處理無效輸入。

異常和契約

如果先決條件為真，但正在執行的子程式中的某些語句引發了異常，會發生什麼？很有可能子程式無法再建立後置條件。它將失敗。但是，模組的狀態如何呢？

關於模組狀態的第一個答案由以下規則給出

當允許異常從子程式傳播時，必須首先建立模組不變式。

第二個答案可能不同，具體取決於語言。例如，Eiffel 的方式是在發生異常的情況下重試例程：如果異常被處理，並且子程式應該重試以滿足其後置條件，那麼它的先決條件和模組不變式必須首先被建立。（否則，系統無法在不違反契約的情況下像再次呼叫例程那樣工作。）

Ada 與其他一些語言一樣，具有巢狀塊，因此異常處理可以從塊的先決條件開始。因此，如果您設法恢復塊的先決條件，就可以重試該塊。例如，一個塊可以巢狀在迴圈內部。然後，您的處理程式將必須將滿足迴圈執行所需先決條件的值分配給變數。

繼承

待定

簡而言之，被覆蓋方法的先決條件是或運算的，後置條件是與運算的。

對於圍繞派生型別構建的模組，必須能夠用派生型別的物件替換父型別的物件，以便排程呼叫仍然可以依賴父類的契約。同樣，實際呼叫的特徵的後置條件必須暗示父特徵的後置條件。

一個缺陷

給定一個 OO 父型別 T，以及它的其中一個方法，

 type T is tagged private;

 function foo(x: T; n: Count) return Natural;
 -- ! pre: n >= 42

以及一個從 T 派生的型別 D，該型別的方法被覆蓋，

 type D is new T with private;
 
 overriding
 function foo(x: D; n: Count) return Natural;
 -- ! pre: n >= 66

想象一下，T 層次結構中某個型別的一個 OO 變數的引用。然後

 declare
     x: access T'Class := new D;
 begin
     x.foo(42);
 end;

誰該負責呢？

併發

待定

併發執行引入的一個新問題（到目前為止）是：假設

模組的例程應該代表多個呼叫者完成工作，
某個例程的“例項”可能會被另一個“例項”中斷

那麼，例如，在第一個呼叫啟動時模組狀態為真的情況可能在執行第二個呼叫更改了模組狀態後不再為真。這擴充套件到先決條件/後置條件檢查：由於例程的斷言很可能引用它們的模組狀態（以及一般可見的任何內容），因此它們可能會變得不一致。

第一個解決方案嘗試是使先決條件檢查、例程的執行以及後置條件檢查順序和排他。也就是說，只要一個呼叫者正在接受例程的服務，對該例程的其他呼叫將處於掛起狀態，直到該例程完成。

但此外，由於例程的斷言是關於模組狀態的，因此任何其他呼叫者呼叫的模組服務都應該被暫停。

另請參閱守衛、SCOOP、Ada（任務和受保護型別、同步介面）。

另請參閱

Gries, David (1981)，程式設計的科學。紐約

Findler, Robert Bruce；Latendresse, Mario；Felleisen, Matthias (2001)，行為契約和行為子型別。http://doi.acm.org/10.1145/503209.503240 或 http://www.ccs.neu.edu/scheme/pubs/fse01-flf.pdf

Hoare, C. A. R. (1969)，計算機程式設計的公理基礎。CACM，第 12 卷，第 10 號，第 576-583 頁。http://doi.acm.org/10.1145/357980.358001 ，http://doi.acm.org/10.1145/363235.363259

Liskov, Barbara H.；Wing, Jeannete M.，子型別的行為概念。 http://doi.acm.org/10.1145/197320.197383 或 http://www.cs.cmu.edu/afs/cs.cmu.edu/project/venari/papers/subtype-toplas/paper.ps

Meyer, Bertrand (1997)，面向物件軟體構建（OOSC2）。新澤西。第 11 章。

http://www.ecma-international.org/publications/standards/Ecma-367.htm

w:契約式設計

（當然，還有 Dijkstra）