.NET 4.0 代碼契約組件深度解析 (靜態/動態驗證/介面契約)

.NET 4.0 將代碼契約整合進 `mscorlib.dll` (位於 `System.Diagnostics.Contracts`)，提供**編譯時靜態分析**與**運行時動態驗證**雙重保障。本文詳細分類七大契約類型，並給出完整類別實現範例。

七大契約類型分類

核心用法代碼範例

1. 前置條件：參數驗證

public Rational(int numerator, int denominator) {
    Contract.Requires(denominator != 0); // 僅定義 CONTRACTS_FULL 時生效
    Contract.RequiresAlways(numerator >= 0); // 無視編譯開關
    this.numerator = numerator;
    this.denominator = denominator;
}

2. 後置條件：返回值保證

public int Denominator {
    get {
        Contract.Ensures(Contract.Result<int>() != 0); // 返回值契約
        return this.denominator;
    }
}

雖寫在 `get` 開頭，實際在**返回給調用者前**驗證。

3. 物件不變量

[ContractInvariantMethod]
protected void ObjectInvariant() {
    Contract.Invariant(this.denominator != 0);
    Contract.Invariant(this.numerator >= 0);
}

• 方法必須 `void`、無參數、標註 `[ContractInvariantMethod]`。
• 所有 public 方法退出時自動檢查 (含屬性 getter/setter)。

4. 斷言與假定

void Process(Data d) {
    Contract.Assert(d != null); // 失敗 → Debug.Assert(false) → Environment.FailFast()
    Contract.Assume(d.IsValid); // 靜態分析器假設為真，運行時不檢查
    // ...
}

5. 介面契約 (為介面方法添加契約)

[ContractClass(typeof(ICalculatorContract))]
public interface ICalculator {
    int Add(int x, int y);
}

[ContractClassFor(typeof(ICalculator))]
internal sealed class ICalculatorContract : ICalculator {
    public int Add(int x, int y) {
        Contract.Requires(x >= 0);
        Contract.Requires(y >= 0);
        Contract.Ensures(Contract.Result<int>() >= 0);
        return default; // 僅為契約，不實際執行
    }
}

完整類別範例：Rational (有理數)

using System.Diagnostics.Contracts;

public struct Rational {
    private readonly int numerator, denominator;

    public Rational(int numerator, int denominator) {
        Contract.Requires(denominator != 0);
        this.numerator = numerator;
        this.denominator = denominator;
    }

    public int Numerator {
        get {
            Contract.Ensures(Contract.Result<int>() == this.numerator);
            return numerator;
        }
    }

    public int Denominator {
        get {
            Contract.Ensures(Contract.Result<int>() != 0);
            return denominator;
        }
    }

    [ContractInvariantMethod]
    private void ObjectInvariant() {
        Contract.Invariant(denominator != 0);
    }

    public static Rational operator +(Rational a, Rational b) {
        Contract.Ensures(Contract.Result<Rational>().Denominator != 0);
        return new Rational(a.numerator * b.denominator + b.numerator * a.denominator,
                           a.denominator * b.denominator);
    }
}

啟用驗證配置

1. 運行時驗證：專案屬性 → Code Contracts → **Runtime Checking** → Full / Pre/Post / None。
2. 靜態分析：專案屬性 → Code Contracts → **Static Checking** → 勾選啟用 (需安裝 Code Contracts 擴展，VS2010+ 內建)。
3. 符號定義：`CONTRACTS_FULL` 控制 `Requires`/`Ensures`/`Invariant`/`Assert` 編入 IL；`CONTRACTS_PRECONDITIONS` 僅控制 `Requires`。

最佳實踐

1. 公開 API 全覆蓋：所有 public 成員加前置/後置條件。
2. 區分 Requires/RequiresAlways：效能敏感用 `Requires`，安全關鍵用 `RequiresAlways`。
3. 不變量封裝內部一致性：私有欄位約束集中在 `ObjectInvariant`。
4. 介面契約獨立組件：契約類標記 `internal sealed`，不污染公開 API。
5. CI 整合靜態分析：建置伺服器啟用靜態檢查，編譯期攔截違約。

代碼契約將「文檔化假設」昇級為「可驗證規約」，是構建高可靠 .NET 類庫的核心基礎設施。