程式代碼合約（.NET Framework）

備註

本文專屬於 .NET Framework。它不適用於較新的 .NET 實作，包括 .NET 6 和更新版本。

程式代碼合約提供在 .NET Framework 程式代碼中指定前置條件、後置條件和物件不因變數的方法。先決條件是輸入方法或屬性時必須符合的需求。後置條件描述方法或屬性代碼結束時的預期。物件不變量描述處於良好狀態之類別的預期狀態。

備註

.NET 5+ 不支援程式代碼合約（包括 .NET Core 版本）。請考慮改用可為 Null 的參考型別。

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

程式代碼合約的優點包括：

改善的測試：程式代碼合約提供靜態合約驗證、運行時間檢查和文件產生。
自動測試工具：您可以使用程式碼合約來篩選出不符合前置條件的無意義的測試自變數，以產生更有意義的單元測試。
靜態驗證：靜態檢查程式可以決定是否有任何合約違規，而不需要執行程式。它會檢查隱含合約，例如 Null 取值和陣列界限，以及明確合約。
參考檔：檔產生器會使用合約資訊來增強現有的 XML 檔檔。也有樣式表單可以與 Sandcastle 搭配使用，以便產生的文件頁面具有合約區段。

所有 .NET Framework 語言都可以立即利用合約;您不需要撰寫特殊的剖析器或編譯程式。 Visual Studio 增益集可讓您指定要執行的程式碼合約分析層級。分析器可以確認合約格式良好（類型檢查和名稱解析），而且可以產生以通用中繼語言（CIL）格式編譯的合約形式。在 Visual Studio 中撰寫合約可讓您利用工具所提供的標準 IntelliSense。

合約類別中的大部分方法都會有條件地編譯;也就是說，只有在您使用指示詞定義特殊符號CONTRACTS_FULL時，編譯程式才會發出對這些方法的 #define 呼叫。 CONTRACTS_FULL可讓您在程式碼中撰寫合約，而不使用 #ifdef 指示詞，您可以產生不同的版本，有些具有合約，有些則沒有合約。

如需使用程式代碼合約的工具和詳細指示，請參閱Visual Studio Marketplace 網站上的程式碼合約。

前提條件

您可以使用方法來表示前置條件 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 。後置條件表示必須滿足的方法正常終止時的條件。

Contract.Ensures(this.F > 0);

特殊事後條件

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

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

參數是每當拋出true的子類型的例外狀況時，必須滿足的T條件。

有一些例外狀況類型難以在例外後置條件中使用。例如，將Exception 使用為T 類型時，方法仍然必須保證條件，不論擲回的例外狀況類型為何，即使是堆疊溢位或其他無法控制的例外狀況也不例外。您應該僅針對呼叫成員時可能擲出的特定例外情況使用特殊後置條件，例如，在執行 InvalidTimeZoneException 方法呼叫時擲出 TimeZoneInfo。

特殊後置條件

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

您可以使用表達式 Contract.Result<T>()來參考後置條件中的方法傳回值，其中 T 會由方法的傳回型別所取代。當編譯程式無法推斷類型時，您必須明確提供它。例如，C# 編譯器無法推斷不帶任何參數的方法的類型，因此它需要下列後置條件：Contract.Ensures(0 <Contract.Result<int>()) 具有回傳類型 void 的方法不能在其後置條件中參考 Contract.Result<T>() 。
後置條件中的前置值是指方法或屬性開頭的表達式值。它會使用表達式 Contract.OldValue<T>(e)，其中 T 是的型別 e。每當編譯程式能夠推斷其類型時，您可以省略泛型類型自變數。（例如，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 方法，以根據 out 參數允許後置條件。
```
public void OutParam(out int x)
{
    Contract.Ensures(Contract.ValueAtReturn(out x) == 3);
    x = 3;
}
```
  OldValue如同方法，每當編譯程式能夠推斷其類型時，您可以省略泛型型別參數。合約重寫器會以參數的值 out 取代方法呼叫。方法 ValueAtReturn 可能只會出現在後置條件中。方法的自變數必須是 out 結構 out 參數的參數或欄位。後者在參考結構建構函式後置條件中的欄位時也很有用。
  
  備註
  
  目前，程式代碼合約分析工具不會檢查參數是否已 out 正確初始化，並忽略其在後置條件中的提及。因此，在上一個範例中，如果合約後面的行使用了x的值，而不是將值指派給一個整數，編譯程式就不會發出錯誤。不過，在未定義CONTRACTS_FULL預處理器符號的組建上（例如發行組建），編譯程式會發出錯誤。

不因變數

物件不變式是指每當用戶端可以看到該物件時，類別每個實例都必須滿足的條件。它們表示在什麼條件下，對象被視為正確。

以屬性標記 ContractInvariantMethodAttribute 來識別不因變數的方法。除了方法的呼叫 Invariant 序列之外，非變異方法不得包含任何程序代碼，每個方法都會指定個別的不變量，如下列範例所示。

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

不因變數是由CONTRACTS_FULL預處理器符號有條件地定義。執行階段檢查時，會在每個公共方法結束時檢驗不變式。如果非變異提及相同類別中的公用方法，則會停用該公用方法結尾通常會發生的非變異檢查。相反地，檢查只會發生在最外層方法呼叫該類別的結尾。如果因為對另一個類別上方法的呼叫而重新輸入類別，也會發生這種情況。不會檢查物件終結器與 IDisposable.Dispose 的實作中的不變異項。

使用方針

合約訂購

下表顯示撰寫方法合約時應該使用的元素順序。

`If-then-throw statements`	回溯相容的公開前置條件
Requires	所有公共前置條件。
Ensures	所有公共（一般）後置條件。
EnsuresOnThrow	所有公用例外後置條件。
Ensures	所有私有/內部（一般）後置條件。
EnsuresOnThrow	所有私有/內部的例外後置條件。
EndContractBlock	如果在沒有任何其他合約的情況下使用 `if`-`then`-`throw` 樣式前置條件，請呼叫EndContractBlock，以指出所有先前的檢查都是前置條件。

純度

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

程式代碼合約工具目前假設下列程式代碼元素是純粹的：

以 PureAttribute標記的方法。
以 PureAttribute 標記的類型（屬性會套用至所有型別的方法）。
取得存取子的屬性。
運算子（名稱以“op”開頭的靜態方法，且具有一個或兩個參數並且傳回類型不是void）。
其完整名稱開頭為「System.Diagnostics.Contracts.Contract」、“System.String”、“System.IO.Path” 或 “System.Type” 的任何方法。
只要委派類型本身具備PureAttribute屬性，任何叫用的委派都可以。委派型別 System.Predicate<T> 和 System.Comparison<T> 被視為純粹型別。

能見度

合約中提及的所有成員至少必須和其出現的方法一樣可見。例如，無法在公用方法的前置條件中提及私用字段;用戶端在呼叫方法之前，無法驗證這類合約。不過，如果欄位標示 ContractPublicPropertyNameAttribute為，則會豁免這些規則。

範例

下列範例顯示程式代碼合約的使用。

#define CONTRACTS_FULL

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);
    }
}

#Const CONTRACTS_FULL = True

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


    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


    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
End Class

意見反應

此頁面對您有幫助嗎？

Last updated on 2025-06-17