1. 程式人生 > >.NET 4.0 中的契約式程式設計

.NET 4.0 中的契約式程式設計

契約式程式設計不是一門嶄新的程式設計方法論。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 。您能夠享受這樣的權利和義務:地獄般恐怖的提問和騷擾。非不厭其煩者勿擾。