.NET 4.0 契約式程式設計完整指南：Precondition、Postcondition、Invariant 與靜態驗證

什麼是契約式程式設計？

**「契約 = 方法/類別必須為真的條件集合」**。源自 Eiffel 語言 (Bertrand Meyer)，核心三要素：

• Precondition (前置條件)：呼叫端必須滿足 (參數驗證)
• Postcondition (後置條件)：方法結束時保證成立 (回傳值、狀態)
• Invariant (不變量)：物件生命週期中永遠成立的條件

.NET 4.0 透過 System.Diagnostics.Contracts.Contract 靜態類別標準化此模型，並整合 **靜態驗證器 (Static Checker)** 與 **運行期檢查**。

為什麼 C++ 契約失敗而 .NET 成功？

核心 API 速查表

實戰範例：有理數類別

using System.Diagnostics.Contracts;

public class RationalNumber
{
    private int _numerator;
    private int _denominator;

    public RationalNumber(int numerator, int denominator)
    {
        // Precondition: 分母不可為 0
        Contract.Requires(denominator != 0, "Denominator cannot be zero.");
        _numerator = numerator;
        _denominator = denominator;
    }

    public int Denominator
    {
        get
        {
            // Postcondition: 取得值時保證非 0
            Contract.Ensures(Contract.Result<int>() != 0);
            return _denominator;
        }
    }

    // Object Invariant: 物件內部永遠滿足分母非 0
    [ContractInvariantMethod]
    private void ObjectInvariant()
    {
        Contract.Invariant(_denominator != 0);
    }
}

後置條件進階特殊方法

OldValue 使用限制 (重要)

• 僅能用於 Ensures / EnsuresOnThrows 內。
• 不可巢狀：OldValue(OldValue(x)) ❌
• 不可存取回傳值：OldValue(Contract.Result<int>()) ❌
• 不可存取 out 參數：OldValue(outParam) ❌
• ForAll/Exists 謂詞內不可存取謂詞參數：ForAll(0, n, i => OldValue(arr[i])) ✅ (索引器參數)；ForAll(0, n, i => OldValue(i)) ❌

介面與抽象方法契約

介面/抽象方法無方法本體，需**契約類別**配合雙屬性：

[ContractClass(typeof(IAccountContract))]
public interface IAccount
{
    int Balance { get; }
    void Deposit(int amount);
}

[ContractClassFor(typeof(IAccount))]
sealed class IAccountContract : IAccount
{
    public int Balance
    {
        get
        {
            Contract.Ensures(Contract.Result<int>() >= 0);
            return default(int); // 必須提供 dummy return
        }
    }

    public void Deposit(int amount)
    {
        Contract.Requires(amount > 0);
        // 若需呼叫介面其他成員：
        IAccount self = this;
        Contract.Requires(self.Balance < 10000);
    }
}

契約屬性總覽

靜態驗證器 (Static Checker) - 關鍵價值

• **編譯期發現 Bug**：未執行程式即偵測 Precondition 違規、Invariant 破壞。
• 整合 Visual Studio 建置流程 (需安裝 Code Contracts 擴充套件)。
• 輸出警告/錯誤列表，可點擊跳轉原始碼。
• 支援 [ContractVerification(false)] 逐步導入舊專案。

已知限制 (NET 4.0 版本)

效能與部署策略

1. Debug 建置：啟用所有契約檢查 (Pre/Post/Invariant/Assert)。
2. Release 建置：預設僅保留 Requires (前置條件)；可組態保留更多。
3. 公開 API：使用 RequiresAlways 確保參數驗證永不移除。
4. 內部邏輯：用 Requires，Release 可移除提升效能。

與 D 語言契約比較

D 語言原生 in/out/invariant 區塊，語法更優雅、編譯器深度整合。.NET 契約雖為庫級實現，但配合**靜態驗證器**已達實用水準，且優勢在於**生態整合** (VS、CI/CD、文檔生成)。

結語

契約式程式設計將「文檔中的規範」搬進「可驗證的程式碼」。.NET 4.0 提供成熟工具鏈：Contract.Requires/Ensures/Invariant + 靜態驗證器。建議：**公開 API 必加 Precondition、核心領域模型加 Invariant、關鍵演算法加 Postcondition**，逐步建立「有契約的代碼庫」，大幅降低防禦性程式碼、提早攔截邏輯錯誤、改善團隊溝通精度。

1. 上一篇文章： LINQ to SQL N 層架構查詢 (上)：自訂實體回傳與資料傳輸載體設計
2. 下一篇文章： 分散式事務深度解析 (三)：System.Transactions 依賴事務與 TransactionScope 完整實戰

關於.NET

[你必須知道的.NET] 第七回：品味類型——從通用類型系統 (CTS) 開始

想要真正駕馭 .NET，必須從類型系統的基石——通用類型系統

WF 4.0 基礎篇(十)：集合操作活動完整教學

前言 WF 4.0 提供四大集合操作活動：AddToColl

ASP.NET Web API 非同步檔案上傳下載完整實作：EasyUI 前端整合與後端儲存

ASP.NET Web API 非同步檔案上傳下載完整實作

C# 經典面試題：i = i++ 究竟等於多少？後置遞增/前置遞增底層執行順序深度解析

題目 int i = 0; Console.WriteLin