契約式編程不是一門嶄新的編程方法論。C/C++ 時代早已有之。Microsoft 在 .NET 4.0 中正式引入 契約式編程庫。博主以為契約式編程是一種相當不錯的編程思想，每一個開發人員都應該掌握。它不但 可以使開發人員的思維更清晰，而且對於提高程序性能很有幫助。值得一提的是，它對於並行程序設計 也有莫大的益處。
我們先看一段很簡單的，未使用契約式編程的代碼示例。
// .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;
}
}
}
上述代碼表示一個在 32 位有符號整型范圍內的有理數。數學上，有理數是一個整數 a 和一個非零 整數 b 的比，通常寫作 a/b，故又稱作分數(題外話：有理數這個翻譯真是夠奇怪)。由此，我們知道， 有理數的分母不能為 0 。所以，上述代碼示例的構造函數還需要寫些防御性代碼。通常 .NET 開發人員 會這樣寫：
// .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;
}
}
}
下面我們來看一下使用契約式編程的 .NET 4.0 代碼示例。為了更加方便的說明，博主在整個示例上 都加了契約，但此示例並非一定都加這些契約。
// .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);
}
}
詳細的解釋稍後再說。按理，既然契約式編程有那麼多好處，那在 C/C++ 世界應該很流行才對。為 什麼很少看到關於契約式編程的討論呢？看一下 C++ 的契約式編程示例就知道了。下面是 C++ 代碼示 例：
//typedef long int32_t;
#include <stdint.h>
template
inline 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..., 上述代碼充斥了大量的宏和條件編譯。對於習慣了 C# 優雅語法的 .NET 開發人員來說，它 們是如此丑陋。更重要的是，契約式編程在 C++ 世界並未被標准化，因此項目之間的定義和修改各不一 樣，給代碼造成很大混亂。這正是很少在實際中看到契約式編程應用的原因。但是在 .NET 4.0 中，契 約式編程變得簡單優雅起來。.NET 4.0 提供了契約式編程庫。實際上，.NET 4.0 僅僅是針對 C++ 宏和 條件編譯的再次抽象和封裝。它完全基於 CONTRACTS_FULL， CONTRACTS_PRECONDITIONS Symbol 和 System.Diagnostics.Debug.Assert 方法、System.Environment.FastFail 方法的封裝。
那麼，何謂契約式編程？
何謂契約式編程
契約是減少大型項目成本的突破性技術。它一般由 Precondition(前置條件)， Postcondition(後置 條件) 和 Invariant(不變量) 等概念組成。.NET 4.0 除上述概念之外，還增加了 Assert(斷言)， Assume(假設) 概念。這可以由枚舉 ContractFailureKind 類型一窺端倪。
契約的思想很簡單。它只是一組結果為真的表達式。如若不然，契約就被違反。那按照定義，程序中 就存在纰漏。契約構成了程序規格說明的一部分，只不過該說明從文檔挪到了代碼中。開發人員都知道 ，文檔通常不完整、過時，甚至不存在。將契約挪移到代碼中，就使得程序可以被驗證。
正如前所述，.NET 4.0 對宏和條件編譯進行抽象封裝。這些成果大多集中在 System.Diagnostics.Contracts.Contract 靜態類中。該類中的大多數成員都是條件編譯。這樣，我們 就不用再使用 #ifdef 和定義 CONTRACTS_FULL 之類的標記。更重要的是，這些行為被標准化，可以在 多個項目中統一使用，並根據情況是否生成帶有契約的程序集。
1. Assert
Assert(斷言)是最基本的契約。.NET 4.0 使用 Contract.Assert() 方法來特指斷言。它用來表示程 序點必須保持的一個契約。
Contract.Assert(this.privateField > 0);
Contract.Assert(this.x == 3, "Why isn’t the value of x 3?");
斷言有兩個重載方法，首參數都是一個布爾表達式，第二個方法的第二個參數表示違反契約時的異常 信息。
當斷言運行時失敗，.NET CLR 僅僅調用 Debug.Assert 方法。成功時則什麼也不做。
2. Assume
.NET 4.0 使用 Contract.Assume() 方法表示 Assume(假設) 契約。
Contract.Assume(this.privateField > 0);
Contract.Assume(this.x == 3, "Static checker assumed this");
Assume 契約在運行時檢測的行為與 Assert(斷言) 契約完全一致。但對於靜態驗證來說，Assume 契 約僅僅驗證已添加的事實。由於諸多限制，靜態驗證並不能保證該契約。或許最好先使用 Assert 契約 ，然後在驗證代碼時按需修改。
當 Assume 契約運行時失敗時， .NET CLR 會調用 Debug.Assert(false)。同樣，成功時什麼也不做 。
3. Preconditions
.NET 4.0 使用 Contract.Requires() 方法表示 Preconditions(前置條件) 契約。它表示方法被調 用時方法狀態的契約，通常被用來做參數驗證。所有 Preconditions 契約相關成員，至少方法本身可以 訪問。
Contract.Requires(x != null);
Preconditions 契約的運行時行為依賴於幾個因素。如果只隱式定義了 CONTRACTS PRECONDITIONS 標記，而沒有定義 CONTRACTS_FULL 標記，那麼只會進行檢測 Preconditions 契約，而不會檢測任何 Postconditions 和 Invariants 契約。假如違反了 Preconditions 契約，那麼 CLR 會調用 Debug.Assert(false) 和 Environment.FastFail 方法。
假如想保證 Preconditions 契約在任何編譯中都發揮作用，可以使用下面這個方法：
Contract.RequiresAlways(x != null);
為了保持向後兼容性，當已存在的代碼不允許被修改時，我們需要拋出指定的精確異常。但是在 Preconditions 契約中，有一些格式上的限定。如下代碼所示：
if (x == null) throw new ArgumentException("The argument can not be
null.");
Contract.EndContractBlock(); // 前面所有的 if 檢測語句皆是 Preconditions
契約
這種 Preconditions 契約的格式嚴格受限：它必須嚴格按照上述代碼示例格式。而且不能有 else 從句。此外，then 從句也只能有單個 throw 語句。最後必須使用 Contract.EndContractBlock() 方法 來標記 Preconditions 契約結束。
看到這裡，是不是覺得大多數參數驗證都可以被 Preconditions 契約替代？沒有錯，事實的確如此 。這樣這些防御性代碼完全可以在 Release 被去掉，從而不用做那些冗余的代碼檢測，從而提高程序性 能。但在面向驗證客戶輸入此類情境下，防御性代碼仍有必要。再就是，Microsoft 為了保持兼容性， 並沒有用 Preconditions 契約代替異常。
4. Postconditions
Postconditions 契約表示方法終止時的狀態。它跟 Preconditions 契約的運行時行為完全一致。但 與 Preconditions 契約不同，Postconditions 契約相關的成員有著更少的可見性。客戶程序或許不會 理解或使用 Postconditions 契約表示的信息，但這並不影響客戶程序正確使用 API 。
對於 Preconditions 契約來說，它則對客戶程序有副作用：不能保證客戶程序不違反 Preconditions 契約。
A. 標准 Postconditions 契約用法
.NET 4.0 使用 Contract.Ensures() 方法表示標准 Postconditions 契約用法。它表示方法正常終 止時必須保持的契約。
Contract.Ensures(this.F > 0);
B. 特殊 Postconditions 契約用法
當從方法體內拋出一個特定異常時，通常情況下 .NET CLR 會從方法體內拋出異常的位置直接跳出， 從而輾轉堆棧進行異常處理。假如我們需要在異常拋出時還要進行 Postconditions 契約驗證，我們可 以如下使用：
Contract.EnsuresOnThrows<T>(this.F > 0);
其中小括號內的參數表示當異常從方法內拋出時必須保持的契約，而泛型參數表示異常發生時拋出的 異常類型。舉例來說，當我們把 T 用 Exception 表示時，無論什麼類型的異常被拋出，都能保證 Postconditions 契約。哪怕這個異常是堆棧溢出或任何不能控制的異常。強烈推薦當異常是被調用 API 一部分時，使用 Contract.EnsuresOnThrows<T>() 方法。
C. Postconditions 契約內的特殊方法
以下要講的這幾個特殊方法僅限使用在 Postconditions 契約內。
方法返回值 在 Postconditions 契約內，可以通過 Contract.Result<T>() 方法表示，其中 T 表示方法返回類型。當編譯器不能推導出 T 類型時，我們必須顯式指出。比如，C# 編譯器就不能推 導出方法參數類型。
Contract.Ensures(0 < Contract.Result<int>());
假如方法返回 void ，則不必在 Postconditions 契約內使用 Contract.Result<T>() 。
前值(舊值) 在 Postconditions 契約內，通過 Contract.OldValue<T>(e) 表示舊有值，其 中 T 是 e 的類型。當編譯器能夠推導 T 類型時，可以忽略。此外 e 和舊有表達式出現上下文有一些 限制。舊有表達式只能出現在 Postconditions 契約內。舊有表達式不能包含另一個舊有表達式。一個 很重要的原則就是舊有表達式只能引用方法已經存在的那些舊值。比如，只要方法 Preconditions 契約 持有，它必定能被計算。下面是這個原則的一些示例：
方法的舊有狀態必定存在其值。比如 Preconditions 契約暗含 xs != null ，xs 當然可以被計算。 但是，假如 Preconditions 契約為 xs != null || E(E 為任意表達式)，那麼 xs 就有可能不能被計算 。
Contract.OldValue(xs.Length); // 很可能錯誤
方法返回值不能被舊有表達式引用。
Contract.OldValue(Contract.Result<int>() + x); // 錯誤
out 參數也不能被舊有表達式引用。
如果某些標記的方法依賴方法返回值，那麼這些方法也不能被舊有表達式引用。
Contract.ForAll(0, Contract.Result<int>(), i => Contract.OldValue(xs[i]) > 3); // 錯誤
舊有表達式不能在 Contract.ForAll() 和 Contract.Exists() 方法內引用匿名委托參數，除非舊有 表達式被用作索引器或方法調用參數。
Contract.ForAll(0, xs.Length, i => Contract.OldValue(xs[i]) > 3); // OK
Contract.ForAll(0, xs.Length, i => Contract.OldValue(i) > 3); // 錯誤
如果舊有表達式依賴於匿名委托的參數，那麼舊有表達式不能在匿名委托的方法體內。除非匿名委托 是 Contract.ForAll() 和 Contract.Exists() 方法的參數。
Foo( ... (T t) => Contract.OldValue(... t ...) ... ); // 錯誤
D. out 參數
因為契約出現在方法體前面，所以大多數編譯器不允許在 Postconditions 契約內引用 out 參數。 為了繞開這個問題，.NET 契約庫提供了 Contract.ValueAtReturn<T>(out T t) 方法。
public void OutParam(out int x)
{
Contract.Ensures(Contract.ValueAtReturn (out x) == 3);
x = 3;
}
跟 OldValue 一樣，當編譯器能推導出類型時，泛型參數可以被忽略。該方法只能出現在 Postconditions 契約。方法參數必須是 out 參數，且不允許使用表達式。
需要注意的是，.NET 目前的工具不能檢測確保 out 參數是否正確初始化，而不管它是否在 Postconditions 契約內。因此， x = 3 語句假如被賦予其他值時，編譯器並不能發現錯誤。但是，當 編譯 Release 版本時，編譯器將發現該問題。
5. Object Invariants
對象不變量表示無論對象是否對客戶程序可見，類的每一個實例都應該保持的契約。它表示對象處於 一個“良好”狀態。
在 .NET 4.0 中，對象的所有不變量都應當放入一個受保護的返回 void 的實例方法中。同時用 [ContractInvariantMethod]特性標記該方法。此外，該方法體內在調用一系列 Contract.Invariant() 方法後不能再有其他代碼。通常我們會把該方法命名為 ObjectInvariant 。
[ContractInvariantMethod]
protected void ObjectInvariant()
{
Contract.Invariant(this.y >= 0);
Contract.Invariant(this.x > this.y);
}
同樣，Object Invariants 契約的運行時行為和 Preconditions 契約、Postconditions 契約行為一 致。CLR 運行時會在每個公共方法末端檢測 Object Invariants 契約，但不會檢測對象終結器或任何實 現 System.IDisposable 接口的方法。
6. Contract 靜態類中的其他特殊方法
.NET 4.0 契約庫中的 Contract 靜態類還提供了幾個特殊的方法。它們分別是：
A. ForAll
Contract.ForAll() 方法有兩個重載。第一個重載有兩個參數：一個集合和一個謂詞。謂詞表示返回 布爾值的一元方法，且該謂詞應用於集合中的每一個元素。任何一個元素讓謂詞返回 false ，ForAll 停止迭代並返回 false 。否則， ForAll 返回 true 。下面是一個數組內所有元素都不能為 null 的契 約示例：
public T[] Foo<T>(T[] array)
{
Contract.Requires(Contract.ForAll (array, (T x) => x != null));
}
B. Exists
它和 ForAll 方法差不多。
7. 接口契約
因為 C#/VB 編譯器不允許接口內的方法帶有實現代碼，所以我們如果想在接口中實現契約，需要創 建一個幫助類。接口和契約幫助類通過一對特性來鏈接。如下所示：
[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 需要顯式如上述聲明從而把接口和接口方法相關聯起來。注意，我們不得不產生一個啞元返回 值。最簡單的方式就是返回 default(T)，不要使用 Contract.Result<T> 。
由於 .NET 要求顯式實現接口方法，所以在契約內引用相同接口的其他方法就顯得很笨拙。由 此，.NET 允許在契約方法之前，使用一個局部變量引用接口類型。如下所示：
[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); // 否則的話，就需要強制轉型 ((IFoo)this).Count
}
}
8. 抽象方法契約
同接口類似，.NET 中抽象類中的抽象方法也不能包含方法體。所以同接口契約一樣，需要幫助類來 完成契約。代碼示例不再給出。
9. 契約方法重載
所有的契約方法都有一個帶有 string 類型參數的重載版本。如下所示：
Contract.Requires(obj != null, "if obj is null, then missiles are fired!");
這樣當契約被違反時，.NET 可以在運行時提供一個信息提示。目前，該字符串只能是編譯時常量。但是 ，將來 .NET 可能會改變，字符串可以運行時被計算。但是，如果是字符串常量，靜態診斷工具可以選 擇顯示它。
10. 契約特性
A. ContractClass 和 ContractClassFor
這兩個特性，我們已經在接口契約和抽象方法契約裡看到了。ContractClass 特性用於添加到接口或 抽象類型上，但是指向的卻是實現該類型的幫助類。ContractClassFor 特性用來添加到幫助類上，指向 我們需要契約驗證的接口或抽象類型。
B. ContractInvariantMethod
這個特性用來標記表示對象不變量的方法。
C. Pure
Pure 特性只聲明在那些沒有副作用的方法調用者上。.NET 現存的一些委托可以被認為如此，比如 System.Predicate<T> 和 System.Comparison<T>。
D. RuntimeContracts
這是個程序集級別的特性(具體如何，俺也不太清楚)。
E. ContractPublicPropertyName
這個特性用在字段上。它被用在方法契約中，且該方法相對於字段來說，更具可見性。比如私有字段 和公共方法。如下所示：
[ContractPublicPropertyName("PublicProperty")]
private int field;
public int PublicProperty { get { ... } }
F. ContractVerification
這個特性用來假設程序集、類型、成員是否可被驗證執行。我們可以使用 [ContractVerification (false)] 來顯式標記程序集、類型、成員不被驗證執行。
.NET 契約庫目前的缺陷
接下來，講一講 .NET 契約庫目前所存在的一些問題。
值類型中的不變量是被忽略的，不發揮作用。
靜態檢測還不能處理 Contract.ForAll() 和 Contract.Exists() 方法。
C# 迭代器中的契約問題。我們知道 Microsoft 在 C# 2.0 中添加了 yield 關鍵字來幫助我們完成 迭代功能。它其實是 C# 編譯器做的糖果。現在契約中，出現了問題。編譯器產生的代碼會把我們寫的 契約放入到 MoveNext() 方法中。這個時侯，靜態檢測就不能保證能夠正確完成 Preconditions 契約。
Well，.NET 契約式編程到這裡就結束了。嗯，就到這裡了。
PS : .NET 契約庫雖然已經相當優雅。但博主以為，其跟 D 語言實現的契約式編程仍有一段距離。
PS : 有誰願意當俺的 Mentor 。您能夠享受這樣的權利和義務：地獄般恐怖的提問和騷擾。非不厭 其煩者勿擾。
