代码协定

项目
08/12/2011

代码协定提供一种使用代码指定前置条件、后置条件和对象固定条件的方式。前置条件是在输入方法或属性时必须满足的要求。后置条件描述方法或属性代码退出时的预期。对象固定条件描述正常状态下的类的预期状态。

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

代码协定的优点包括：

改进测试：代码协定提供静态协定验证、运行时检查和文档生成。
自动测试工具：可以使用代码协定来筛选掉不满足前置条件的没有意义的测试参数，从而生成更有意义的单元测试。
静态验证：静态检查器可以在不运行程序的情况下确定是否存在任何违反协定的情况。它会检查隐式协定（如 null 取消引用和数组绑定）和显式协定。
引用文档：文档生成器在现有的 XML 文档文件增加协定信息。还提供了可与 Sandcastle 一起使用的样式表，以便生成的文档页具有协定节。

所有 .NET Framework 语言都可以立即使用协定；您不必编写特殊的分析器或编译器。利用 Visual Studio 外接程序，您可以指定要执行的代码协定分析的级别。分析器可以确认协定的格式正确（执行类型检查和名称解析），并且可以使用 Microsoft 中间语言 (MSIL) 格式生成编译格式的协定。通过在 Visual Studio 中创作协定，您可以利用该工具提供的标准 IntelliSense。

协定类中的大多数方法都是在一定条件下编译的；也就是说，只有在使用 #define 指令定义特殊符号 CONTRACTS FULL 时，编译器才会发出对这些方法的调用。可以利用 CONTRACTS FULL 通过代码编写协定，而不必使用 #ifdef 指令；可以产生不同的生成，有些生成包含协定，有些不包含协定。

有关工具的信息以及使用代码协定的详细说明，请参见 MSDN DevLabs 网站上的代码协定。

Preconditions

可以使用 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 表达式只受纯正性规则的限制。但是，引发的异常类型必须与包含协定的方法具有相同的可见性。

Postconditions

后置条件是针对方法终止时的状态的协定。在即将退出方法之前检查后置条件。失败的后置条件的运行时行为由运行时分析器确定。

与前置条件不同，后置条件可以引用可见性更低的成员。客户端可能无法理解或利用后置条件使用私有状态表示的某些信息，但这不会影响客户端正确使用方法的能力。

标准后置条件

可以使用 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# 编译器无法推断出不采用任何参数的方法的类型，因此需要下面的后置条件：返回类型为 void 的 Contract.Ensures(0 < Contract.Result<int>()) 方法无法在其后置条件中引用 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<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 预处理器符号的版本（如发布版本），则编译器将发出错误。

固定条件

对象固定条件是指每当对象对客户端可见时对于类的每个实例都应为 true 的条件。它们表示用于判断对象是否正确的条件。

固定条件方法通过标记 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);
    }
}

通过