程式碼合約

發行項
08/12/2011

程式碼合約可讓您在程式碼中指定前置條件、後置條件和物件非變異。前置條件是進入方法或屬性時必須符合的需求。後置條件會描述方法或屬性程式碼結束時的預期。物件非變異會描述處於良好狀態之類別的預期狀態。

程式碼合約包括標記程式碼的類別、編譯階段分析的靜態分析器，以及執行階段分析器。您可以在 System.Diagnostics.Contracts 命名空間中找到程式碼合約的類別。

程式碼合約的優點包括：

改善的測試：程式碼合約會提供靜態合約驗證、執行階段檢查和文件產生。
自動測試工具：您可以使用程式碼合約，篩選出不滿足前置條件的無意義測試引數，藉以產生更有意義的單元測試。
靜態驗證：靜態檢查程式可以在不執行程式的情況下，判斷是否存在任何合約違規。它會檢查隱含合約 (例如 null 取值 (Dereference) 和陣列界限) 以及明確合約。
參考文件：文件產生器會使用合約資訊來擴充現有的 XML 文件檔。此外，還有一些可搭配 Sandcastle 使用的樣式表，讓產生的文件頁面具有合約區段。

所有 .NET Framework 語言都可以立即運用合約。您不需要撰寫特殊剖析器或編譯器。 Visual Studio 增益集可讓您指定要執行之程式碼合約分析的層級。這些分析器可以確認合約的語式正確 (型別檢查和名稱解析)，而且可以用 Microsoft Intermediate Language (MSIL) 格式來產生合約的編譯形式。在 Visual Studio 中撰寫合約可讓您運用此工具所提供的標準 IntelliSense。

合約類別中的大部分方法都是條件式編譯方法。也就是說，只有當您使用 #define 指示詞來定義特殊符號 CONTRACTS FULL 時，編譯器才會發出這些方法的呼叫。 CONTRACTS FULL 可讓您在程式碼中撰寫合約，而不需要使用 #ifdef 指示詞。您可以產生不同的組建，讓某些組建包含合約，而某些則不包含合約。

如需使用程式碼合約的工具和詳細指示，請參閱 MSDN DevLabs 網站上的程式碼合約 (英文)。

前置條件

您可以使用 Contract.Requires 方法來表示前置條件。前置條件會指定叫用方法時的狀態。它們通常是用來指定有效的參數值。在前置條件中提及的所有成員至少都必須與方法本身具有相同的可存取性。否則，方法的所有呼叫端可能無法了解前置條件。此條件必須沒有任何副作用。失敗前置條件的執行階段行為是由執行階段分析器所決定。

例如，下列前置條件表示 x 參數必須是非 null。

Contract.Requires( x != null );

如果您的程式碼必須在前置條件失敗時擲回特定例外狀況，您就可以依照下列方式使用 Requires 的泛型多載。

Contract.Requires<ArgumentNullException>( x != null, "x" );

舊版 Requires 陳述式

大部分程式碼會用 if-then-throw 程式碼形式來包含一些參數驗證。在下列情況中，合約工具會將這些陳述式辨識為前置條件：

這些陳述式出現在方法中的任何其他陳述式前面。
這類陳述式的完整集合後面接著明確 Contract 方法呼叫，例如 Requires、Ensures、EnsuresOnThrow 或 EndContractBlock 方法的呼叫。

當 if-then-throw 陳述式以這種形式出現時，這些工具就會將它們辨識為舊版 requires 陳述式。如果沒有任何其他合約接在 if-then-throw 序列後面，請使用 Contract.EndContractBlock 方法來結束程式碼。

if ( x == null ) throw new ...
Contract.EndContractBlock(); // All previous "if" checks are preconditions

請注意，上述測試中的條件是相反前置條件 (實際的前置條件是 x != null)。相反前置條件的限制相當嚴格：您必須依照上述範例撰寫此前置條件。也就是說，它不應該包含任何 else 子句，而且 then 子句的主體必須是單一 throw 陳述式。雖然 if 測試同時受限於純正和可視性規則 (請參閱用法方針)，不過 throw 運算式僅受限於純正規則。但是，擲回之例外狀況的型別必須與合約所在的方法具有相同的可視性。

後置條件

後置條件是方法終止時方法狀態的合約。後置條件是在結束方法之前檢查的。失敗後置條件的執行階段行為是由執行階段分析器所決定。

與前置條件不同的是，後置條件可以參考可視性較低的成員。用戶端可能無法了解或運用使用私用狀態之後置條件所表示的部分資訊，但是這並不會影響用戶端正確使用此方法的能力。

標準後置條件

您可以使用 Ensures 方法來表示標準後置條件。後置條件表示在方法正常終止時必須為 true 的條件。

Contract.Ensures( this .F > 0 );

例外後置條件

例外後置條件是指當方法擲回特定例外狀況時應該為 true 的後置條件。您可以使用 Contract.EnsuresOnThrow 方法來指定這些後置條件，如下列範例所示。

Contract.EnsuresOnThrow<T>( this.F > 0 );

其引數是每當擲回屬於 T 之子型別的例外狀況時，必須為 true 的條件。

某些例外狀況型別很難在例外後置條件中使用。例如，如果針對 T 使用 Exception 型別，不論所擲回的例外狀況型別為何，都會要求此方法保證條件，即使它是堆疊溢位或其他無法控制的例外狀況也一樣。您應該只針對呼叫成員時可能會擲回的特定例外狀況使用例外後置條件，例如，針對 TimeZoneInfo 方法呼叫擲回 InvalidTimeZoneException 時。

特殊後置條件

下列方法只能使用於後置條件中：

您可以在後置條件中使用運算式 Contract. Result<T>() 參考方法傳回值，其中 T 是由方法的傳回型別所取代。當編譯器無法推斷型別時，您就必須明確提供型別。例如，C# 編譯器無法針對不採用任何引數的方法推斷型別，因此需要下列後置條件：Contract.Ensures(0 < Contract.Result<int>())。傳回型別為 void 的方法無法在其後置條件中參考 Contract. Result<T>()。

後置條件中的前置狀態值會參考位於方法或屬性開頭之運算式的值。它會使用 Contract.OldValue<T>(e) 運算式，其中 e 的型別為 T。每當編譯器能夠推斷其型別時，您就可以省略泛型型別引數 (例如，C# 編譯器一定會推斷此型別，因為它採用了引數)。可出現在 e 中的項目以及舊運算式可出現的內容具有許多限制。舊運算式不得包含另一個舊運算式。最重要的是，舊運算式必須參考存在方法前置條件狀態中的值。換言之，只要方法的前置條件為 true，它就必須是可評估的運算式。下面是該項規則的許多執行個體。

此值必須存在方法的前置條件狀態中。為了參考物件的欄位，前置條件必須保證物件一定是非 null。

您不得在舊運算式中參考方法的傳回值：

Contract.OldValue(Contract.Result<int>() + x) // ERROR

您不得在舊運算式中參考 out 參數。
如果數量詞的範圍相依於方法的傳回值，舊運算式就不得相依於數量詞的繫結變數：
```
Contract. ForAll (0,Contract. Result<int>(),
i => Contract.OldValue(xs[i]) > 3 ); // ERROR
```

除非舊運算式當做方法呼叫的索引子或引數使用，否則它不得在 ForAll 或 Exists 呼叫中參考匿名委派的參數：

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

如果舊運算式的值相依於匿名委派的任何參數，除非此匿名委派是 ForAll 或 Exists 方法的引數，否則舊運算式不得出現在匿名委派的主體中：
```
Method( ... (T t) => Contract.OldValue(... t ...) ... ); // ERROR
```

Out 參數會呈現問題，因為合約出現在方法主體前面，而且大部分編譯器不允許在後置條件中使用 out 參數的參考。若要解決此問題，Contract 類別會提供 ValueAtReturn<T> 方法，以便允許使用以 out 參數為基礎的後置條件。

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

與 OldValue<T> 方法一樣，每當編譯器能夠推斷其型別時，您就可以省略泛型型別參數。合約重寫器會將方法呼叫取代成 out 參數的值。 ValueAtReturn<T> 方法只能出現在後置條件中。此方法的引數必須是 out 參數或結構 out 參數的欄位。在結構建構函式的後置條件中參考欄位時，後者也很有用。

注意事項
目前，程式碼合約分析工具不會檢查 out 參數是否正確初始化，因而忽略後置條件中所提及的這些參數。因此，在上述範例中，如果合約後面的程式碼行使用了 x 的值而非指派整數給它，編譯器就不會發出正確的錯誤。不過，在沒有定義 CONTRACTS FULL 前置處理器符號的組建 (例如發行組建) 中，編譯器將發出錯誤。

目前，程式碼合約分析工具不會檢查 out 參數是否正確初始化，因而忽略後置條件中所提及的這些參數。因此，在上述範例中，如果合約後面的程式碼行使用了 x 的值而非指派整數給它，編譯器就不會發出正確的錯誤。不過，在沒有定義 CONTRACTS FULL 前置處理器符號的組建 (例如發行組建) 中，編譯器將發出錯誤。

不變項目

物件非變異是指每當用戶端可以看見該物件時，對於每個類別執行個體而言應該要成立的條件。它們表示用來將物件視為正確的條件。

非變異方法的識別方式是使用 ContractInvariantMethodAttribute 屬性來標記。除了 Invariant 方法的一連串呼叫以外，這些非變異方法不得包含任何程式碼，而且每個呼叫都會指定個別非變異，如下列範例所示。

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

非變異是由 CONTRACTS FULL 前置處理器符號以條件方式定義。在執行階段檢查期間，系統會在每個公用方法的結尾檢查非變異。如果非變異提及相同類別中的公用方法，就會停用通常在公用方法結尾進行的非變異檢查。此時，這項檢查只會在該類別最外層的方法呼叫結尾進行。如果此類別由於另一個類別之方法的呼叫而重新進入，也會發生這種情況。若為物件完成項或實作 Dispose 方法的任何方法，就不會檢查非變異。

用法方針

合約排序

下表顯示當您撰寫方法合約時應該使用的項目順序。

If-then-throw statements	回溯相容公用前置條件
Requires	所有公用前置條件。
Ensures	所有公用 (一般) 後置條件。
EnsuresOnThrow	所有公用例外後置條件。
Ensures	所有私用/內部 (一般) 後置條件。
EnsuresOnThrow	所有私用/內部例外後置條件。
EndContractBlock	如果使用 if-then-throw 樣式的前置條件而沒有任何其他合約，請放置 EndContractBlock 的呼叫，表示所有先前的 if 檢查都是前置條件。

純正

在合約內部呼叫的所有方法都必須是純正方法。也就是說，它們不得更新任何預先存在的狀態。純正方法可以修改進入純正方法之後已經建立的物件。

程式碼合約工具目前會假設下列程式碼項目都是純正的：

使用 PureAttribute 標記的方法。
使用 PureAttribute (此屬性適用於此型別的所有方法) 標記的型別。
Property get 存取子。
運算子 (其名稱以 "op" 為開頭而且具有一個或兩個參數和一個非 void 傳回型別的靜態方法)。
其完整名稱以 "System.Diagnostics.Contracts.Contract"、"System.String"、"System.IO.Path" 或 "System.Type" 為開頭的任何方法。
任何叫用的委派，不過前提是委派型別本身是以 PureAttribute 屬性化。委派型別 System.Predicate<T> 和 System.Comparison<T> 都會被視為純正的。

可視性

在合約中提及的所有成員至少都必須與成員所在的方法具有相同的可視性。例如，公用方法的前置條件中不得提及私用欄位。用戶端無法在呼叫此方法之前驗證這類合約。不過，如果此欄位使用 ContractPublicPropertyNameAttribute 來標記，它就不受限於這些規則。

範例

下列範例將說明程式碼合約的使用方式。

Imports System
Imports System.Diagnostics.Contracts


' An IArray is an ordered collection of objects.    
<ContractClass(GetType(IArrayContract))> _
Public Interface IArray
    ' The Item property provides methods to read and edit entries in the array.

    Default Property Item(ByVal index As Integer) As [Object]


    ReadOnly Property Count() As Integer


    ' Adds an item to the list.  
    ' The return value is the position the new element was inserted in.
    Function Add(ByVal value As Object) As Integer

    ' Removes all items from the list.
    Sub Clear()

    ' Inserts value into the array at position index.
    ' index must be non-negative and less than or equal to the 
    ' number of elements in the array.  If index equals the number
    ' of items in the array, then value is appended to the end.
    Sub Insert(ByVal index As Integer, ByVal value As [Object])


    ' Removes the item at position index.
    Sub RemoveAt(ByVal index As Integer)
End Interface 'IArray

<ContractClassFor(GetType(IArray))> _
Friend MustInherit Class IArrayContract
    Implements IArray

    Function Add(ByVal value As Object) As Integer Implements IArray.Add
        ' Returns the index in which an item was inserted.
        Contract.Ensures(Contract.Result(Of Integer)() >= -1) '
        Contract.Ensures(Contract.Result(Of Integer)() < CType(Me, IArray).Count) '
        Return 0

    End Function 'IArray.Add

    Default Property Item(ByVal index As Integer) As Object Implements IArray.Item
        Get
            Contract.Requires(index >= 0)
            Contract.Requires(index < CType(Me, IArray).Count)
            Return 0 '
        End Get
        Set(ByVal value As [Object])
            Contract.Requires(index >= 0)
            Contract.Requires(index < CType(Me, IArray).Count)
        End Set
    End Property

    Public ReadOnly Property Count() As Integer Implements IArray.Count
        Get
            Contract.Requires(Count >= 0)
            Contract.Requires(Count <= CType(Me, IArray).Count)
            Return 0 '
        End Get
    End Property

    Sub Clear() Implements IArray.Clear
        Contract.Ensures(CType(Me, IArray).Count = 0)

    End Sub 'IArray.Clear


    Sub Insert(ByVal index As Integer, ByVal value As [Object]) Implements IArray.Insert
        Contract.Requires(index >= 0)
        Contract.Requires(index <= CType(Me, IArray).Count) ' For inserting immediately after the end.
        Contract.Ensures(CType(Me, IArray).Count = Contract.OldValue(CType(Me, IArray).Count) + 1)

    End Sub 'IArray.Insert


    Sub RemoveAt(ByVal index As Integer) Implements IArray.RemoveAt
        Contract.Requires(index >= 0)
        Contract.Requires(index < CType(Me, IArray).Count)
        Contract.Ensures(CType(Me, IArray).Count = Contract.OldValue(CType(Me, IArray).Count) - 1)

    End Sub 'IArray.RemoveAt
End Class 'IArrayContract

using System;
using System.Diagnostics.Contracts;

// An IArray is an ordered collection of objects.    
[ContractClass(typeof(IArrayContract))]
public interface IArray
{
    // The Item property provides methods to read and edit entries in the array.
    Object this[int index]
    {
        get;
        set;
    }

    int Count
    {
        get;

    }

    // Adds an item to the list.  
    // The return value is the position the new element was inserted in.
    int Add(Object value);

    // Removes all items from the list.
    void Clear();

    // Inserts value into the array at position index.
    // index must be non-negative and less than or equal to the 
    // number of elements in the array.  If index equals the number
    // of items in the array, then value is appended to the end.
    void Insert(int index, Object value);


    // Removes the item at position index.
    void RemoveAt(int index);
}

[ContractClassFor(typeof(IArray))]
internal abstract class IArrayContract : IArray
{
    int IArray.Add(Object value)
    {
        // Returns the index in which an item was inserted.
        Contract.Ensures(Contract.Result<int>() >= -1);
        Contract.Ensures(Contract.Result<int>() < ((IArray)this).Count);
        return default(int);
    }
    Object IArray.this[int index]
    {
        get
        {
            Contract.Requires(index >= 0);
            Contract.Requires(index < ((IArray)this).Count);
            return default(int);
        }
        set
        {
            Contract.Requires(index >= 0);
            Contract.Requires(index < ((IArray)this).Count);
        }
    }
    public int Count
    {
        get
        {
            Contract.Requires(Count >= 0);
            Contract.Requires(Count <= ((IArray)this).Count);
            return default(int);
        }
    }

    void IArray.Clear()
    {
        Contract.Ensures(((IArray)this).Count == 0);
    }

    void IArray.Insert(int index, Object value)
    {
        Contract.Requires(index >= 0);
        Contract.Requires(index <= ((IArray)this).Count);  // For inserting immediately after the end.
        Contract.Ensures(((IArray)this).Count == Contract.OldValue(((IArray)this).Count) + 1);
    }

    void IArray.RemoveAt(int index)
    {
        Contract.Requires(index >= 0);
        Contract.Requires(index < ((IArray)this).Count);
        Contract.Ensures(((IArray)this).Count == Contract.OldValue(((IArray)this).Count) - 1);
    }
}

共用方式為