契約式設計（Dbc）以及其在C語言中的應用

轉載時請表明出處

作者聯系方式：[email protected]

一、前言

  本周教育訓練中接觸到了契約式設計，查閱了許多資料後仍然是一知半解，與同僚和大學導師交流了後，受到了啟發，本文記錄總結了個人對契約式設計的學習感悟。

二、什麼是契約式設計？

1、概述

  契約式設計/契約式編碼（Design by Contract(DbC)，以下簡稱 DbC ）是一種設計計算機軟體的方法。這種方法描述了，軟體設計者應該為軟體元件定義正式的、準确的、可驗證的接口規範，它擴充了抽象資料類型對于先驗條件、後驗條件和不變式的一般定義。這些規範稱為“契約”，它是一個比喻，類似于商業契約/合同的條件和職責，對于以上概念，下文會詳細描寫。

注：Dbc起源于Eiffel語言，但它的應用範圍與語言無關。

2、目的

  Dbc的主要目的是希望程式員能夠在設計程式時明确地規定一個子產品單元（具體到面向對象，就是一個類的執行個體）在調用某個操作前後應當屬于何種狀态。Dbc不是一種程式設計範型，它是一種設計風格，一種文法規範。

3、思路

  契約式設計強調三個概念：先驗條件，後驗證條件和不變式。

• 先驗條件：對于函數來講，期望所有調用它的子產品都保證一定的進入條件，這樣它就不用去處理不滿足先驗條件的情況，先驗條件發生在每個函數的最開始。
• 後驗條件：保證退出時給出特定的屬性，也就是說函數保證能做到的事情，函數完成時的狀态，函數有這一事實表示它會結束，不會無休止的循環，後驗條件發生在每個函數的最後。
• 不變式：在進入時假定，并在退出時保持一些特定的屬性，不變式實際上是前置條件和後置條件的交集，違反這些操作會導緻程式抛出異常。從調用者的角度來看，該條件總是為真，在函數的内部處理過程中，不變項可以為變，但在函數結束後，控制傳回調用者時，不變項必須為真。

4、六大原則

（1）區分指令和查詢。查詢傳回一個結果，但不改變對象的可見性質。指令改變對象的狀态，但不一定傳回結果。

（2）将基本查詢同派生查詢分開。派生查詢可以用基本查詢來定義。

（3） 針對每個派生查詢，設定一個後驗條件，使用一個或多個基本查詢的結果來定義它。這樣我們隻要知道基本查詢的值，也就能知道派生查詢的值。

（4） 對于每個指令都撰寫一個後驗條件，規定每個基本查詢的值。結合“用基本查詢定義派生查詢”的原則，我們已經能夠知道每個指令的全部可視效果。

（5）對于每個查詢和指令，采用一個合适的先驗條件。先驗條件限定了客戶調用查詢和指令的時機。

（6） 撰寫不變式來定義對象的恒定特性。類是某種抽象的展現，應當将注意力集中在最重要的屬性上，以幫助讀者建立關于類抽象的正确概念模型。

三、為什麼要使用Dbc（重要性）

• 獲得更優秀的設計：Dbc鼓勵程式員思考諸如“函數的先驗條件是什麼”這樣的問題，這樣有助于程式員理清概念，函數獲得了更清晰的描述，同時限制了函數得調用，對非法調用得結果也很清楚。
• 保證系統健壯性：系統地運用異常 當例程被非法使用（先驗條件失敗）或者例程沒有遵循契約的規定（後驗條件或者不變式失敗）時，就會發生異常。
• 更有效得組織子產品間通信：盡可能準确地規定子產品彼此通信得責任和權力。
• 提高可靠性：編寫契約可以幫助開發者更好地了解代碼，契約有助于測試（契約可以随時關閉或者啟用）。
• 簡化調試：契約能把錯誤牢牢地定位，開發期間的支援 由于斷言判斷為假而在運作時展現出來的錯誤将被精确地定位。

• …

  等等。

四、如何在程式設計中使用Dbc（C語言）

  上文簡單描述了Dbc的定義、它的核心概念以及大緻的思路，可以看出在平時程式設計的時候很多程式員都在或多或少地做一些這些工作。比如在函數定義開始時判斷給定的指針參數是否不能為NULL，或者程式退出時釋放臨時配置設定的記憶體塊。但在具體細節則基本依靠個人習慣，有人喜歡調用方檢查，有人則喜歡被調用方檢查。

  Eiffel與這些實踐的不同之處在于它是唯一一種以文法形式将先驗條件、後驗條件和不變式規定為被調用方代碼中獨立文法塊的語言，其關鍵字分别require、ensure、invariant。

  以下例子為Eiffel語言，來自：http://www.eiffel.com/developers/design_by_contract_in_detail.html

  功能描述：定義一個範型類DICTIONARY [ELEMENT]的put方法；

  先驗條件：目前的元素個數count小于容量capacity，鍵值key不是空字元串；

  後驗條件：字典中存在元素x；使用健值key擷取的元素是x；操作後元素個數count等于操作前元素個數old count加一；

  不變式：元素個數count大于0，小于容量capacity；

class DICTIONARY [ELEMENT]                
    feature
put (x: ELEMENT; key: STRING) is                
         -- Insert x so that it will be retrievable               
         -- through key.              
require
count <= capacity
not key.empty
        ensure  
has (x)        
item (key) = x  
count = old count + 1
    end  
     ... Interface specifications of other features ...                  
invariant  
0 <= count  
          count <= capacity  
end
           

  将其改寫為C語言，如下所示：

#include "stdio.h"
#include "assert.h"

/* 動态數組元素結構體（假設） */
typedef struct _element_t {
 int x;
 char* key;
} element_t;

bool_t put(darray_t* darray, int x, const char* key) {
 /* 先驗條件(require) */
 assert(darray->size >= 0 && darray->size < darray->capacity);

 /* 不變式（invariant） */
 assert(darray->size >= 0 && darray->size < darray->capacity);

 /* put操作 */
 uint32_t old_count = darray->size;
 element_t elm;
 elm.x = x;
 elm.key = TKMEM_CALLOC(1, tk_strlen(key) + 1);
 tk_strcpy(elm.key, key);
 darray_push(darray, &elm);

 /* 後驗條件（ensure） */
 element_t* elm_find = darray_find(darray, &elm);
 assert(elm_find != NULL && elm_find->x == x && tk_str_eq(elm_find->key, key) && darray->size == old_count + 1);

 /* 不變式（invariant） again */
 assert(darray->size >= 0 && darray->size < darray->capacity);
    
 return TRUE;
}
           

注：

以上代碼調用了AWTK中的部分庫函數，如有不懂請在評論提問，或者私信。

AWTK的github倉庫：https://github.com/zlgopen/awtk

五、總結

  通過以上的學習，可以看出Dbc的本意其實很簡單，就是在設計程式中加入斷言。而所謂斷言，實際就是必須為真的假設，隻有這些假設為真，程式才可以做到正确無誤。Dbc的主要斷言就包括以上所講的先驗條件，後驗證條件和不變式。

  最後，在此感謝與我讨論交流的同僚和抽空回答我問題的大學導師。