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

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

契約式設計

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

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

如果你設定了一個模組(!)契約，契約的條款將適用於整個模組在其整個生命週期中。如果你使用一個有契約的模組，你必須遵守其可見規則。

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

1. 模組的不變式和
2. 模組子例程的前置條件和後置條件。

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

1. 模組的不變式,
2. 模組子例程的前置條件和後置條件,
3. 迴圈不變式和迴圈變數,
4. 檢查指令
5. 一致的異常處理

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

檢查每個語言提供的支援功能：w:Design by contract.

斷言

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

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

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

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

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

  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 programming language.

---

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

---

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

模組不變式 (C, S)

模組不變式斷言模組初始化後什麼為真。它們還斷言在執行其任何子程式之前和之後，相同的真值保持不變。

前置條件 (C, S)

子程式的前置條件宣告在呼叫子程式之前什麼必須為真。通常，它表達（計算的）模組變數和子程式引數的關係。只有當前置條件為真時，子程式才能執行以滿足其後置條件。

後置條件 (C, S)

後置條件宣告子程式成功完成後，（計算的）變數和關係將為真。

(迴圈變數) (S)

迴圈變數是一個表示式（型別為 Natural），其值在迴圈的每次迭代中都減少到零。通常，迴圈中的一個變數被用來表達這個屬性。迴圈變數保證終止。

迴圈不變式 (S)

迴圈不變式表達一個關係，該關係在進入迴圈時或再次進入迴圈時為真。該關係將命名與迴圈相關的變數。

檢查 (S)

當一條語句執行完畢後，它很可能會透過賦值改變一個或多個變數的值。檢查表達了程式設計師對這些變數在賦值之後的關係的預期。

子程式的前置條件 P 和後置條件 QS從Hoare 三元組的角度來說，對子程式進行了限定

{至少 P} S {保證 Q},

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

契約式設計不是輸入檢查

從上面的關於錯誤斷言的規則中，可以推斷出，斷言不應作為輸入驗證的替代。當你不信任你的輸入時，請使用你的語言提供的條件語句中的方法，例如 Ada 中的'Valid屬性。例如，呼叫 Sqrt（x）其中 x = -1.23 是使用Sqrt的錯誤，違反了契約。呼叫者在將 x 傳送到數學例程之前，沒有對其進行測試。

斷言不能替代條件語句

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

1. 如果一個模組被證明是正確的，則可以關閉該模組的斷言檢查，預計客戶端將履行其契約義務。呼叫者違反契約可能會不被察覺，並可能導致嚴重錯誤的計算。
2. 如果呼叫的子程式不是Sqrt而是控制火車的速度，你不能一直傳遞無效的輸入，直到它碰巧沒有使速度控制子程式因異常而失敗。更糟糕的是，見 1。

示例：堆疊

(這個示例是用非常簡化的 Ada 符號表示的，因為知道 Ada 2005 中對 DbC 的語言支援相當好，尤其是在 Ada 2005 中，但有限。想象一下，將 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;

誰該負責？

併發

待定

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

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

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

第一個解決方案嘗試是使前置條件檢查、例程的執行和後置條件檢查順序且排他。也就是說，只要呼叫者由例程服務，對例程的其他呼叫就會處於掛起狀態，直到例程完成為止。

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

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

另請參閱

Gries, David (1981), The Science of Programming. New York

Findler, Robert Bruce; Latendresse, Mario; Felleisen, Matthias (2001), Behavioral Contracts and Behavioral Subtyping. http://doi.acm.org/10.1145/503209.503240 或 http://www.ccs.neu.edu/scheme/pubs/fse01-flf.pdf

Hoare, C. A. R. (1969), An Axiomatic Basis for Computer Programming. CACM, Vol.12, Number 10, pp. 576–583. http://doi.acm.org/10.1145/357980.358001 , http://doi.acm.org/10.1145/363235.363259

Liskov, Barbara H.; Wing, Jeannete M., A Behavioral Notion of Subtyping. 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), Object Oriented Software Construction (OOSC2). New Jersey. Chapter 11.

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

w:Design by contract

（當然，還有 Dijkstra）