契約式編程不是一門(mén)嶄新的編程方法論。C/C++ 時(shí)代早已有之。Microsoft 在 .NET 4.0 中正式引入契約式編程庫(kù)。博主以為契約式編程是一種相當(dāng)不錯(cuò)的編程思想，每一個(gè)開(kāi)發(fā)人員都應(yīng)該掌握。它不但可以使開(kāi)發(fā)人員的思維更清晰，而且對(duì)于提高程序性能很有幫助。值得一提的是，它對(duì)于并行程序設(shè)計(jì)也有莫大的益處。

我們先看一段很簡(jiǎn)單的，未使用契約式編程的代碼示例。

// .NET 代碼示例public class RationalNumber{    private int numberator;    private int denominator;    public RationalNumber(int numberator, int denominator)    {        this.numberator = numberator;        this.denominator = denominator;    }    public int Denominator    {        get        {            return this.denominator;        }    }}

上述代碼表示一個(gè)在 32 位有符號(hào)整型范圍內(nèi)的有理數(shù)。數(shù)學(xué)上，有理數(shù)是一個(gè)整數(shù) a 和一個(gè)非零整數(shù) b 的比，通常寫(xiě)作 a/b，故又稱作分?jǐn)?shù)(題外話：有理數(shù)這個(gè)翻譯真是夠奇怪)。由此，我們知道，有理數(shù)的分母不能為 0 。所以，上述代碼示例的構(gòu)造函數(shù)還需要寫(xiě)些防御性代碼。通常 .NET 開(kāi)發(fā)人員會(huì)這樣寫(xiě)：

// .NET 代碼示例public class RationalNumber{    private int numberator;    private int denominator;    public RationalNumber(int numberator, int denominator)    {        if (denominator == 0)            throw new ArgumentException("The second argument can not be zero.");        this.numberator = numberator;        this.denominator = denominator;    }    public int Denominator    {        get        {            return this.denominator;        }    }}

下面我們來(lái)看一下使用契約式編程的 .NET 4.0 代碼示例。為了更加方便的說(shuō)明，博主在整個(gè)示例上都加了契約，但此示例并非一定都加這些契約。

// .NET 代碼示例public class RationalNumber{    private int numberator;    private int denominator;    public RationalNumber(int numberator, int denominator)    {        Contract.Requires(denominator != 0, "The second argument can not be zero.");        this.numberator = numberator;        this.denominator = denominator;    }    public int Denominator    {        get        {            Contract.Ensures(Contract.Result<int>() != 0);            return this.denominator;        }    }    [ContractInvariantMethod]    protected void ObjectInvariant()    {        Contract.Invariant(this.denominator != 0);    }}

詳細(xì)的解釋稍后再說(shuō)。按理，既然契約式編程有那么多好處，那在 C/C++ 世界應(yīng)該很流行才對(duì)。為什么很少看到關(guān)于契約式編程的討論呢？看一下 C++ 的契約式編程示例就知道了。下面是 C++ 代碼示例：

//typedef long int32_t;#include templateinline void CheckInvariant(T& argument){#ifdef CONTRACT_FULL    argument.Invariant();#endif}public class RationalNumber{private:    int32_t numberator;    int32_t denominator;public:    RationalNumber(int32_t numberator, int32_t denominator)    {#ifdef CONTRACT_FULL        ASSERT(denominator != 0);        CheckInvaraint(*this);#endif        this.numberator = numberator;        this.denominator = denominator;#ifdef CONTRACT_FULL        CheckInvaraint(*this);#endif    }public:    int32_t GetDenominator()    {#ifdef CONTRACT_FULL        // C++ Developers like to use struct type.        class Contract        {            int32_t Result;            Contract()            {            }            ~Contract()            {            }        }#endif#ifdef CONTRACT_FULL        Contract contract = new Contract();        contract.Result = denominator;        CheckInvairant(*this);#endif        return this.denominator;#ifdef CONTRACT_FULL        CheckInvaraint(*this);#endif    }protected:#ifdef CONTRACT_FULL    virtual void Invariant()    {        this.denominator != 0;    }#endif}

Woo..., 上述代碼充斥了大量的宏和條件編譯。對(duì)于習(xí)慣了 C# 優(yōu)雅語(yǔ)法的 .NET 開(kāi)發(fā)人員來(lái)說(shuō)，它們是如此丑陋。更重要的是，契約式編程在 C++ 世界并未被標(biāo)準(zhǔn)化，因此項(xiàng)目之間的定義和修改各不一樣，給代碼造成很大混亂。這正是很少在實(shí)際中看到契約式編程應(yīng)用的原因。但是在 .NET 4.0 中，契約式編程變得簡(jiǎn)單優(yōu)雅起來(lái)。.NET 4.0 提供了契約式編程庫(kù)。實(shí)際上，.NET 4.0 僅僅是針對(duì) C++ 宏和條件編譯的再次抽象和封裝。它完全基于 CONTRACTS_FULL， CONTRACTS_PRECONDITIONS Symbol 和 System.Diagnostics.Debug.Assert 方法、System.Environment.FastFail 方法的封裝。

那么，何謂契約式編程？

何謂契約式編程

契約是減少大型項(xiàng)目成本的突破性技術(shù)。它一般由 Precondition(前置條件)， Postcondition(后置條件) 和 Invariant(不變量) 等概念組成。.NET 4.0 除上述概念之外，還增加了 Assert(斷言)，Assume(假設(shè)) 概念。這可以由枚舉 ContractFailureKind 類型一窺端倪。

契約的思想很簡(jiǎn)單。它只是一組結(jié)果為真的表達(dá)式。如若不然，契約就被違反。那按照定義，程序中就存在紕漏。契約構(gòu)成了程序規(guī)格說(shuō)明的一部分，只不過(guò)該說(shuō)明從文檔挪到了代碼中。開(kāi)發(fā)人員都知道，文檔通常不完整、過(guò)時(shí)，甚至不存在。將契約挪移到代碼中，就使得程序可以被驗(yàn)證。

正如前所述，.NET 4.0 對(duì)宏和條件編譯進(jìn)行抽象封裝。這些成果大多集中在 System.Diagnostics.Contracts.Contract 靜態(tài)類中。該類中的大多數(shù)成員都是條件編譯。這樣，我們就不用再使用 #ifdef 和定義 CONTRACTS_FULL 之類的標(biāo)記。更重要的是，這些行為被標(biāo)準(zhǔn)化，可以在多個(gè)項(xiàng)目中統(tǒng)一使用，并根據(jù)情況是否生成帶有契約的程序集。

1. Assert

Assert(斷言)是最基本的契約。.NET 4.0 使用 Contract.Assert() 方法來(lái)特指斷言。它用來(lái)表示程序點(diǎn)必須保持的一個(gè)契約。

Contract.Assert(this.privateField > 0);Contract.Assert(this.x == 3, "Why isn’t the value of x 3?");

斷言有兩個(gè)重載方法，首參數(shù)都是一個(gè)布爾表達(dá)式，第二個(gè)方法的第二個(gè)參數(shù)表示違反契約時(shí)的異常信息。

當(dāng)斷言運(yùn)行時(shí)失敗，.NET CLR 僅僅調(diào)用 Debug.Assert 方法。成功時(shí)則什么也不做。

2. Assume

.NET 4.0 使用 Contract.Assume() 方法表示 Assume(假設(shè)) 契約。

Contract.Assume(this.privateField > 0);Contract.Assume(this.x == 3, "Static checker assumed this");

Assume 契約在運(yùn)行時(shí)檢測(cè)的行為與 Assert(斷言) 契約完全一致。但對(duì)于靜態(tài)驗(yàn)證來(lái)說(shuō)，Assume 契約僅僅驗(yàn)證已添加的事實(shí)。由于諸多限制，靜態(tài)驗(yàn)證并不能保證該契約。或許最好先使用 Assert 契約，然后在驗(yàn)證代碼時(shí)按需修改。

當(dāng) Assume 契約運(yùn)行時(shí)失敗時(shí)， .NET CLR 會(huì)調(diào)用 Debug.Assert(false)。同樣，成功時(shí)什么也不做。

3. Preconditions

.NET 4.0 使用 Contract.Requires() 方法表示 Preconditions(前置條件) 契約。它表示方法被調(diào)用時(shí)方法狀態(tài)的契約，通常被用來(lái)做參數(shù)驗(yàn)證。所有 Preconditions 契約相關(guān)成員，至少方法本身可以訪問(wèn)。

Contract.Requires(x != null);

Preconditions 契約的運(yùn)行時(shí)行為依賴于幾個(gè)因素。如果只隱式定義了 CONTRACTS PRECONDITIONS 標(biāo)記，而沒(méi)有定義 CONTRACTS_FULL 標(biāo)記，那么只會(huì)進(jìn)行檢測(cè) Preconditions 契約，而不會(huì)檢測(cè)任何 Postconditions 和 Invariants 契約。假如違反了 Preconditions 契約，那么 CLR 會(huì)調(diào)用 Debug.Assert(false) 和 Environment.FastFail 方法。

假如想保證 Preconditions 契約在任何編譯中都發(fā)揮作用，可以使用下面這個(gè)方法：

Contract.RequiresAlways(x != null);

為了保持向后兼容性，當(dāng)已存在的代碼不允許被修改時(shí)，我們需要拋出指定的精確異常。但是在 Preconditions 契約中，有一些格式上的限定。如下代碼所示：

if (x == null) throw new ArgumentException("The argument can not be null.");Contract.EndContractBlock();    // 前面所有的 if 檢測(cè)語(yǔ)句皆是 Preconditions 契約

這種 Preconditions 契約的格式嚴(yán)格受限：它必須嚴(yán)格按照上述代碼示例格式。而且不能有 else 從句。此外，then 從句也只能有單個(gè) throw 語(yǔ)句。最后必須使用 Contract.EndContractBlock() 方法來(lái)標(biāo)記 Preconditions 契約結(jié)束。

看到這里，是不是覺(jué)得大多數(shù)參數(shù)驗(yàn)證都可以被 Preconditions 契約替代？沒(méi)有錯(cuò)，事實(shí)的確如此。這樣這些防御性代碼完全可以在 Release 被去掉，從而不用做那些冗余的代碼檢測(cè)，從而提高程序性能。但在面向驗(yàn)證客戶輸入此類情境下，防御性代碼仍有必要。再就是，Microsoft 為了保持兼容性，并沒(méi)有用 Preconditions 契約代替異常。

4. Postconditions

Postconditions 契約表示方法終止時(shí)的狀態(tài)。它跟 Preconditions 契約的運(yùn)行時(shí)行為完全一致。但與 Preconditions 契約不同，Postconditions 契約相關(guān)的成員有著更少的可見(jiàn)性。客戶程序或許不會(huì)理解或使用 Postconditions 契約表示的信息，但這并不影響客戶程序正確使用 API 。

對(duì)于 Preconditions 契約來(lái)說(shuō)，它則對(duì)客戶程序有副作用：不能保證客戶程序不違反 Preconditions 契約。

A. 標(biāo)準(zhǔn) Postconditions 契約用法

.NET 4.0 使用 Contract.Ensures() 方法表示標(biāo)準(zhǔn) Postconditions 契約用法。它表示方法正常終止時(shí)必須保持的契約。

Contract.Ensures(this.F > 0);

B. 特殊 Postconditions 契約用法

當(dāng)從方法體內(nèi)拋出一個(gè)特定異常時(shí)，通常情況下 .NET CLR 會(huì)從方法體內(nèi)拋出異常的位置直接跳出，從而輾轉(zhuǎn)堆棧進(jìn)行異常處理。假如我們需要在異常拋出時(shí)還要進(jìn)行 Postconditions 契約驗(yàn)證，我們可以如下使用：

Contract.EnsuresOnThrows(this.F > 0);

其中小括號(hào)內(nèi)的參數(shù)表示當(dāng)異常從方法內(nèi)拋出時(shí)必須保持的契約，而泛型參數(shù)表示異常發(fā)生時(shí)拋出的異常類型。舉例來(lái)說(shuō)，當(dāng)我們把 T 用 Exception 表示時(shí)，無(wú)論什么類型的異常被拋出，都能保證 Postconditions 契約。哪怕這個(gè)異常是堆棧溢出或任何不能控制的異常。強(qiáng)烈推薦當(dāng)異常是被調(diào)用 API 一部分時(shí)，使用 Contract.EnsuresOnThrows() 方法。

C. Postconditions 契約內(nèi)的特殊方法

以下要講的這幾個(gè)特殊方法僅限使用在 Postconditions 契約內(nèi)。

方法返回值 在 Postconditions 契約內(nèi)，可以通過(guò) Contract.Result() 方法表示，其中 T 表示方法返回類型。當(dāng)編譯器不能推導(dǎo)出 T 類型時(shí)，我們必須顯式指出。比如，C# 編譯器就不能推導(dǎo)出方法參數(shù)類型。

Contract.Ensures(0 < Contract.Result<int>());

假如方法返回 void ，則不必在 Postconditions 契約內(nèi)使用 Contract.Result() 。

前值(舊值)  在 Postconditions 契約內(nèi)，通過(guò) Contract.OldValue(e) 表示舊有值，其中 T 是 e 的類型。當(dāng)編譯器能夠推導(dǎo) T 類型時(shí)，可以忽略。此外 e 和舊有表達(dá)式出現(xiàn)上下文有一些限制。舊有表達(dá)式只能出現(xiàn)在 Postconditions 契約內(nèi)。舊有表達(dá)式不能包含另一個(gè)舊有表達(dá)式。一個(gè)很重要的原則就是舊有表達(dá)式只能引用方法已經(jīng)存在的那些舊值。比如，只要方法 Preconditions 契約持有，它必定能被計(jì)算。下面是這個(gè)原則的一些示例：

• 方法的舊有狀態(tài)必定存在其值。比如 Preconditions 契約暗含 xs != null ，xs 當(dāng)然可以被計(jì)算。但是，假如 Preconditions 契約為 xs != null || E(E 為任意表達(dá)式)，那么 xs 就有可能不能被計(jì)算。

Contract.OldValue(xs.Length);  // 很可能錯(cuò)誤

• 方法返回值不能被舊有表達(dá)式引用。

Contract.OldValue(Contract.Result<int>() + x);  // 錯(cuò)誤

• out 參數(shù)也不能被舊有表達(dá)式引用。
• 如果某些標(biāo)記的方法依賴方法返回值，那么這些方法也不能被舊有表達(dá)式引用。

Contract.ForAll(0, Contract.Result<int>(), i => Contract.OldValue(xs[i]) > 3);  // 錯(cuò)誤

• 舊有表達(dá)式不能在 Contract.ForAll() 和 Contract.Exists() 方法內(nèi)引用匿名委托參數(shù)，除非舊有表達(dá)式被用作索引器或方法調(diào)用參數(shù)。

Contract.ForAll(0, xs.Length, i => Contract.OldValue(xs[i]) > 3);  // OK

Contract.ForAll(0, xs.Length, i => Contract.OldValue(i) > 3);  // 錯(cuò)誤

• 如果舊有表達(dá)式依賴于匿名委托的參數(shù)，那么舊有表達(dá)式不能在匿名委托的方法體內(nèi)。除非匿名委托是 Contract.ForAll() 和 Contract.Exists() 方法的參數(shù)。

Foo( ... (T t) => Contract.OldValue(... t ...) ... ); // 錯(cuò)誤

D. out 參數(shù)

因?yàn)槠跫s出現(xiàn)在方法體前面，所以大多數(shù)編譯器不允許在 Postconditions 契約內(nèi)引用 out 參數(shù)。為了繞開(kāi)這個(gè)問(wèn)題，.NET 契約庫(kù)提供了 Contract.ValueAtReturn(out T t) 方法。

public void OutParam(out int x){    Contract.Ensures(Contract.ValueAtReturn(out x) == 3);    x = 3;}

跟 OldValue 一樣，當(dāng)編譯器能推導(dǎo)出類型時(shí)，泛型參數(shù)可以被忽略。該方法只能出現(xiàn)在 Postconditions 契約。方法參數(shù)必須是 out 參數(shù)，且不允許使用表達(dá)式。

需要注意的是，.NET 目前的工具不能檢測(cè)確保 out 參數(shù)是否正確初始化，而不管它是否在 Postconditions 契約內(nèi)。因此， x = 3 語(yǔ)句假如被賦予其他值時(shí)，編譯器并不能發(fā)現(xiàn)錯(cuò)誤。但是，當(dāng)編譯 Release 版本時(shí)，編譯器將發(fā)現(xiàn)該問(wèn)題。

5. Object Invariants

對(duì)象不變量表示無(wú)論對(duì)象是否對(duì)客戶程序可見(jiàn)，類的每一個(gè)實(shí)例都應(yīng)該保持的契約。它表示對(duì)象處于一個(gè)“良好”狀態(tài)。

在 .NET 4.0 中，對(duì)象的所有不變量都應(yīng)當(dāng)放入一個(gè)受保護(hù)的返回 void 的實(shí)例方法中。同時(shí)用[ContractInvariantMethod]特性標(biāo)記該方法。此外，該方法體內(nèi)在調(diào)用一系列 Contract.Invariant() 方法后不能再有其他代碼。通常我們會(huì)把該方法命名為 ObjectInvariant 。

[ContractInvariantMethod]protected void ObjectInvariant(){    Contract.Invariant(this.y >= 0);    Contract.Invariant(this.x > this.y);}

同樣，Object Invariants 契約的運(yùn)行時(shí)行為和 Preconditions 契約、Postconditions 契約行為一致。CLR 運(yùn)行時(shí)會(huì)在每個(gè)公共方法末端檢測(cè) Object Invariants 契約，但不會(huì)檢測(cè)對(duì)象終結(jié)器或任何實(shí)現(xiàn) System.IDisposable 接口的方法。

6. Contract 靜態(tài)類中的其他特殊方法

.NET 4.0 契約庫(kù)中的 Contract 靜態(tài)類還提供了幾個(gè)特殊的方法。它們分別是：

A. ForAll

Contract.ForAll() 方法有兩個(gè)重載。第一個(gè)重載有兩個(gè)參數(shù)：一個(gè)集合和一個(gè)謂詞。謂詞表示返回布爾值的一元方法，且該謂詞應(yīng)用于集合中的每一個(gè)元素。任何一個(gè)元素讓謂詞返回 false ，F(xiàn)orAll 停止迭代并返回 false 。否則， ForAll 返回 true 。下面是一個(gè)數(shù)組內(nèi)所有元素都不能為 null 的契約示例：

public T[] Foo(T[] array){    Contract.Requires(Contract.ForAll(array, (T x) => x != null));}

B. Exists

它和 ForAll 方法差不多。

7. 接口契約

因?yàn)?C#/VB 編譯器不允許接口內(nèi)的方法帶有實(shí)現(xiàn)代碼，所以我們?nèi)绻朐诮涌谥袑?shí)現(xiàn)契約，需要?jiǎng)?chuàng)建一個(gè)幫助類。接口和契約幫助類通過(guò)一對(duì)特性來(lái)鏈接。如下所示：

[ContractClass(typeof(IFooContract))]interface IFoo{    int Count { get; }    void Put(int value);}[ContractClassFor(typeof(IFoo))]sealed class IFooContract : IFoo{    int IFoo.Count    {        get        {            Contract.Ensures(Contract.Result<int>() >= 0);            return default(int);    // dummy return        }    }    void IFoo.Put(int value)    {        Contract.Requires(value >= 0);    }}

.NET 需要顯式如上述聲明從而把接口和接口方法相關(guān)聯(lián)起來(lái)。注意，我們不得不產(chǎn)生一個(gè)啞元返回值。最簡(jiǎn)單的方式就是返回 default(T)，不要使用 Contract.Result 。

由于 .NET 要求顯式實(shí)現(xiàn)接口方法，所以在契約內(nèi)引用相同接口的其他方法就顯得很笨拙。由此，.NET 允許在契約方法之前，使用一個(gè)局部變量引用接口類型。如下所示：

[ContractClassFor(typeof(IFoo))]sealed class IFooContract : IFoo{    int IFoo.Count    {        get        {            Contract.Ensures(Contract.Result<int>() >= 0);            return default(int);    // dummy return        }    }    void IFoo.Put(int value)    {        IFoo iFoo = this;        Contract.Requires(value >= 0);        Contract.Requires(iFoo.Count < 10); // 否則的話，就需要強(qiáng)制轉(zhuǎn)型 ((IFoo)this).Count    }}

8. 抽象方法契約

同接口類似，.NET 中抽象類中的抽象方法也不能包含方法體。所以同接口契約一樣，需要幫助類來(lái)完成契約。代碼示例不再給出。

9. 契約方法重載

所有的契約方法都有一個(gè)帶有 string 類型參數(shù)的重載版本。如下所示：

Contract.Requires(obj != null, "if obj is null, then missiles are fired!");

這樣當(dāng)契約被違反時(shí)，.NET 可以在運(yùn)行時(shí)提供一個(gè)信息提示。目前，該字符串只能是編譯時(shí)常量。但是，將來(lái) .NET 可能會(huì)改變，字符串可以運(yùn)行時(shí)被計(jì)算。但是，如果是字符串常量，靜態(tài)診斷工具可以選擇顯示它。

10. 契約特性

A. ContractClass 和 ContractClassFor

這兩個(gè)特性，我們已經(jīng)在接口契約和抽象方法契約里看到了。ContractClass 特性用于添加到接口或抽象類型上，但是指向的卻是實(shí)現(xiàn)該類型的幫助類。ContractClassFor 特性用來(lái)添加到幫助類上，指向我們需要契約驗(yàn)證的接口或抽象類型。

B. ContractInvariantMethod

這個(gè)特性用來(lái)標(biāo)記表示對(duì)象不變量的方法。

C. Pure

Pure 特性只聲明在那些沒(méi)有副作用的方法調(diào)用者上。.NET 現(xiàn)存的一些委托可以被認(rèn)為如此，比如 System.Predicate 和 System.Comparison。

D. RuntimeContracts

這是個(gè)程序集級(jí)別的特性(具體如何，俺也不太清楚)。

E. ContractPublicPropertyName

這個(gè)特性用在字段上。它被用在方法契約中，且該方法相對(duì)于字段來(lái)說(shuō)，更具可見(jiàn)性。比如私有字段和公共方法。如下所示：

[ContractPublicPropertyName("PublicProperty")]private int field;public int PublicProperty { get { ... } }

F. ContractVerification

這個(gè)特性用來(lái)假設(shè)程序集、類型、成員是否可被驗(yàn)證執(zhí)行。我們可以使用 [ContractVerification(false)] 來(lái)顯式標(biāo)記程序集、類型、成員不被驗(yàn)證執(zhí)行。

.NET 契約庫(kù)目前的缺陷

接下來(lái)，講一講 .NET 契約庫(kù)目前所存在的一些問(wèn)題。

• 值類型中的不變量是被忽略的，不發(fā)揮作用。
• 靜態(tài)檢測(cè)還不能處理 Contract.ForAll() 和 Contract.Exists() 方法。
• C# 迭代器中的契約問(wèn)題。我們知道 Microsoft 在 C# 2.0 中添加了 yield 關(guān)鍵字來(lái)幫助我們完成迭代功能。它其實(shí)是 C# 編譯器做的糖果。現(xiàn)在契約中，出現(xiàn)了問(wèn)題。編譯器產(chǎn)生的代碼會(huì)把我們寫(xiě)的契約放入到 MoveNext() 方法中。這個(gè)時(shí)侯，靜態(tài)檢測(cè)就不能保證能夠正確完成 Preconditions 契約。

Well，.NET 契約式編程到這里就結(jié)束了。嗯，就到這里了。

PS : .NET 契約庫(kù)雖然已經(jīng)相當(dāng)優(yōu)雅。但博主以為，其跟 D 語(yǔ)言實(shí)現(xiàn)的契約式編程仍有一段距離。

PS : 有誰(shuí)愿意當(dāng)俺的 Mentor 。您能夠享受這樣的權(quán)利和義務(wù)：地獄般恐怖的提問(wèn)和騷擾。非不厭其煩者勿擾。

NET技術(shù)：.NET 4.0 中的契約式編程，轉(zhuǎn)載需保留來(lái)源！

鄭重聲明：本文版權(quán)歸原作者所有，轉(zhuǎn)載文章僅為傳播更多信息之目的，如作者信息標(biāo)記有誤，請(qǐng)第一時(shí)間聯(lián)系我們修改或刪除，多謝。