代码协定（.NET Framework）

2025-06-19

注释

本文特定于 .NET Framework。它不适用于 .NET 的较新版本实现，包括 .NET 6 及更高版本。

代码协定提供了一种在 .NET Framework 代码中指定前置条件、后置条件和对象固定的方法。先决条件是输入方法或属性时必须满足的要求。后置条件描述方法或属性代码退出时的预期。对象固定符描述处于良好状态的类的预期状态。

注释

.NET 5+ 中不支持代码协定（包括 .NET Core 版本）。请考虑改用可为 NULL 的引用类型。

代码协定包括用于标记代码的类、用于编译时分析的静态分析器和运行时分析器。可以在命名空间中找到代码协定的 System.Diagnostics.Contracts 类。

代码协定的优点包括：

改进了测试：代码协定提供静态协定验证、运行时检查和文档生成。
自动测试工具：可以使用代码协定通过筛选出不满足先决条件的毫无意义的测试参数来生成更有意义的单元测试。
静态验证：静态检查器可以确定是否有任何协定冲突，而无需运行程序。它会检查隐式协定，例如空引用和数组边界，以及明确的契约。
参考文档：文档生成器使用合同信息扩充现有 XML 文档文件。还有可用于 Sandcastle 的样式表，以便生成的文档页包含协定部分。

所有 .NET Framework 语言都可以立即利用合同;无需编写特殊的分析程序或编译器。 Visual Studio 加载项允许指定要执行的代码协定分析级别。分析器可以确认协定格式正确（类型检查和名称解析），并且可以以公共中间语言（CIL）格式生成协定的编译形式。通过在 Visual Studio 中创建协定，你可以使用工具提供的标准 IntelliSense。

协定类中的大多数方法都是有条件编译的;也就是说，仅当使用指令定义特殊符号CONTRACTS_FULL时，编译器才会发出对这些方法的 #define 调用。 CONTRACTS_FULL允许在代码中编写协定，而无需使用#ifdef指令。可以生成不同的版本，其中一些包含协定，而另一些则不包含协定。

有关使用代码协定的工具和详细说明，请参阅 Visual Studio 市场网站上的代码协定。

前提条件

可以使用该方法 Contract.Requires 表达前置条件。在调用方法时，前置条件指定状态。它们通常用于指定有效的参数值。在前置条件中提及的所有成员必须至少与方法本身一样易于访问;否则，方法的所有调用方可能无法理解前置条件。条件的执行不得有副作用。失败先决条件的运行时行为由运行时分析器确定。

例如，以下前置条件表示该参数 x 必须为非 null。

Contract.Requires(x != null);

如果代码必须在前置条件失败时引发特定异常，则可以按如下所示使用泛型重载 Requires 。

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

旧版需要语句

大多数代码包含一些参数验证，形式为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);

自变量是指每次引发作为 true 的子类型的异常时必须为 T 的条件。

有一些异常类型很难在异常后置条件中使用。例如，使用类型ExceptionT要求该方法保证条件，而不考虑引发的异常类型，即使它是堆栈溢出或其他无法控制的异常。应仅将异常后置条件用于调用成员时可能引发的特定异常，例如，当对 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 以表示之前所有的 if 检查均为前置条件。

纯度

在协定中调用的所有方法都必须是纯的;也就是说，它们不得更新任何预先存在的状态。允许纯方法修改在进入纯方法后创建的对象。

代码协定工具目前假定以下代码元素是纯的：

标记为 PureAttribute 的方法。
使用 PureAttribute 标记的类型（该属性适用于所有类型的方法）。
属性 get 访问器。
运算符（其名称以“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

通过

代码协定 （.NET Framework）

前提 条件