代码协定Code Contracts

代码协定提供了在代码中指定前置条件、后置条件和对象固定的方法。Code contracts provide a way to specify preconditions, postconditions, and object invariants in your code. 前置条件是输入方法或属性时必须满足的要求。Preconditions are requirements that must be met when entering a method or property. 后置条件描述在方法或属性代码退出时的预期。Postconditions describe expectations at the time the method or property code exits. 对象固定描述处于良好状态的类的预期状态。Object invariants describe the expected state for a class that is in a good state.

代码协定包含用于标记代码的类、用于编译时分析的静态分析器以及运行时分析器。Code contracts include classes for marking your code, a static analyzer for compile-time analysis, and a runtime analyzer. 代码协定的类位于 System.Diagnostics.Contracts 命名空间。The classes for code contracts can be found in the System.Diagnostics.Contracts namespace.

代码协定包括以下优点:The benefits of code contracts include the following:

  • 改进测试:代码协定提供静态协定验证、运行时检查和文档生成。Improved testing: Code contracts provide static contract verification, runtime checking, and documentation generation.

  • 自动测试工具:可通过过滤掉不满足前置条件的无意义的测试参数,使用代码协定来生成更有意义的单元测试。Automatic testing tools: You can use code contracts to generate more meaningful unit tests by filtering out meaningless test arguments that do not satisfy preconditions.

  • 静态验证:静态检查器无需运行程序即可决定是否存在任何协定冲突。Static verification: The static checker can decide whether there are any contract violations without running the program. 它可检查隐式协定(如 null 取消引用和数组绑定)和显式协定。It checks for implicit contracts, such as null dereferences and array bounds, and explicit contracts.

  • 参考文档:文档生成器扩充具有协定信息的现有 XML 文档文件。Reference documentation: The documentation generator augments existing XML documentation files with contract information. 还提供了可与 Sandcastle 一起使用的样式表,因此,生成的文档页具有协定部分。There are also style sheets that can be used with Sandcastle so that the generated documentation pages have contract sections.

所有 .NET Framework 语言可立即使用协定;无需编写特定分析器或编译器。All .NET Framework languages can immediately take advantage of contracts; you do not have to write a special parser or compiler. Visual Studio 外接程序使你可以指定要执行的代码协定分析的级别。A Visual Studio add-in lets you specify the level of code contract analysis to be performed. 分析器可确认协定的格式是否标准(类型检查和名称解析),并且可以 Microsoft 中间语言 (MSIL) 格式生成约定的已编译形式。The analyzers can confirm that the contracts are well-formed (type checking and name resolution) and can produce a compiled form of the contracts in Microsoft intermediate language (MSIL) format. 通过在 Visual Studio 中创建协定,你可以使用工具提供的标准 IntelliSense。Authoring contracts in Visual Studio lets you take advantage of the standard IntelliSense provided by the tool.

协定类中的大多数方法都进行条件编译;即,编译器仅在你定义特殊符号 CONTRACTS_FULL 时才使用 #define 指令发出对这些方法的调用。Most methods in the contract class are conditionally compiled; that is, the compiler emits calls to these methods only when you define a special symbol, CONTRACTS_FULL, by using the #define directive. 借助 CONTRACTS_FULL,你无需需使用 #ifdef 指令就可将协定写入代码;还可生成两种不同的版本:一种带有协定,一种未带协定。CONTRACTS_FULL lets you write contracts in your code without using #ifdef directives; you can produce different builds, some with contracts, and some without.

有关使用代码协定的工具和详细说明,请参阅 Visual Studio marketplace 网站上的代码协定For tools and detailed instructions for using code contracts, see Code Contracts on the Visual Studio marketplace site.

PreconditionsPreconditions

可使用 Contract.Requires 方法表达前置条件。You can express preconditions by using the Contract.Requires method. 前置条件在方法被调用时指定状态。Preconditions specify state when a method is invoked. 它们通常用于指定有效的参数值。They are generally used to specify valid parameter values. 前置条件中提到的所有成员至少都必须与方法本身一样可以访问;否则,方法的调用方可能无法理解此前置条件。All members that are mentioned in preconditions must be at least as accessible as the method itself; otherwise, the precondition might not be understood by all callers of a method. 条件必须无副作用。The condition must have no side-effects. 运行时分析器确定前置条件失败时的运行时行为。The run-time behavior of failed preconditions is determined by the runtime analyzer.

例如,以下前置条件表示参数 x 必须为非 null。For example, the following precondition expresses that parameter x must be non-null.

Contract.Requires(x != null);

如果你的代码必须在前置条件失败时引发特定异常,可使用 Requires 的泛型重载,如下所示。If your code must throw a particular exception on failure of a precondition, you can use the generic overload of Requires as follows.

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

旧版需要语句Legacy Requires Statements

大多数代码包含一些参数验证,其形式为 if-then-throw 代码。Most code contains some parameter validation in the form of if-then-throw code. 在以下情况中,协定工具将这些语句识别为前置条件:The contract tools recognize these statements as preconditions in the following cases:

if-then-throw 语句显示为此形式时,工具会将其识别为旧的 requires 语句。When if-then-throw statements appear in this form, the tools recognize them as legacy requires statements. 如果 if-then-throw 序列后未接其他协定,则代码以 Contract.EndContractBlock 方法结束。If no other contracts follow the if-then-throw sequence, end the code with the Contract.EndContractBlock method.

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

请注意,上述测试中的条件是取反的前置条件。Note that the condition in the preceding test is a negated precondition. (实际的前提条件将为 x != null。)求反的前置条件受到严格限制:必须按前面的示例所示编写:也就是说,它不应包含任何 else 子句,then 子句的主体必须是单个 throw 语句。(The actual precondition would be x != null.) A negated precondition is highly restricted: It must be written as shown in the previous example; that is, it should contain no else clauses, and the body of the then clause must be a single throw statement. if 测试受纯度和可见性规则约束(请参阅使用准则),但 throw 表达式仅受纯度规则约束。The if test is subject to both purity and visibility rules (see Usage Guidelines), but the throw expression is subject only to purity rules. 但是,引发的异常类型必须与发生协定的方法同样可见。However, the type of the exception thrown must be as visible as the method in which the contract occurs.

PostconditionsPostconditions

后置条件是方法终止时的方法的状态协定。Postconditions are contracts for the state of a method when it terminates. 刚好退出方法前检查后置条件。The postcondition is checked just before exiting a method. 运行时分析器确定后置条件失败时的运行时行为。The run-time behavior of failed postconditions is determined by the runtime analyzer.

与前置条件不同,后置条件可能引用可见性较低的成员。Unlike preconditions, postconditions may reference members with less visibility. 客户端可能无法理解或利用后置条件使用私有状态表达的某些信息,但这不影响客户端正确使用方法的能力。A client may not be able to understand or make use of some of the information expressed by a postcondition using private state, but this does not affect the client's ability to use the method correctly.

标准后置条件Standard Postconditions

可使用 Ensures 方法表达标准后置条件。You can express standard postconditions by using the Ensures method. 后置条件表示方法正常终止时必须为 true 的条件。Postconditions express a condition that must be true upon normal termination of the method.

Contract.Ensures(this.F > 0);

异常后置条件Exceptional Postconditions

异常后置条件是在方法引发特定异常时应为 true 的后置条件。Exceptional postconditions are postconditions that should be true when a particular exception is thrown by a method. 可使用 Contract.EnsuresOnThrow 方法来指定这些后置条件,如下例所示。You can specify these postconditions by using the Contract.EnsuresOnThrow method, as the following example shows.

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

自变量是指每次引发作为 true 的子类型的异常时必须为 T 的条件。The argument is the condition that must be true whenever an exception that is a subtype of T is thrown.

有一些异常类型很难在异常后置条件中使用。There are some exception types that are difficult to use in an exceptional postcondition. 例如,若要使用 ExceptionT 类型,则无论引发的异常类型如何(即使是堆栈溢出或其他不可控制的异常),方法都必须保证条件。For example, using the type Exception for T requires the method to guarantee the condition regardless of the type of exception that is thrown, even if it is a stack overflow or other impossible-to-control exception. 应仅将异常后置条件用于调用成员时可能引发的特定异常,例如,当对 InvalidTimeZoneException 方法调用引发 TimeZoneInfo 时。You should use exceptional postconditions only for specific exceptions that might be thrown when a member is called, for example, when an InvalidTimeZoneException is thrown for a TimeZoneInfo method call.

特殊后置条件Special Postconditions

以下方法可能仅在后置条件中使用:The following methods may be used only within postconditions:

  • 通过使用表达式 Contract.Result<T>()(其中 T 替换为方法的返回类型),可引用后置条件中的方法返回值。You can refer to method return values in postconditions by using the expression Contract.Result<T>(), where T is replaced by the return type of the method. 编译器无法推断出类型时,必须显式提供此类型。When the compiler is unable to infer the type, you must explicitly provide it. 例如,C# 编译器无法推断不带任何参数的方法类型,因此它需要后置条件 Contract.Ensures(0 <Contract.Result<int>())。返回类型为 void 的方法无法引用后置条件中的 Contract.Result<T>()For example, the C# compiler is unable to infer types for methods that do not take any arguments, so it requires the following postcondition: Contract.Ensures(0 <Contract.Result<int>()) Methods with a return type of void cannot refer to Contract.Result<T>() in their postconditions.

  • 后置条件中的预状态值是指方法或属性开头的表达式的值。A prestate value in a postcondition refers to the value of an expression at the start of a method or property. 它使用表达式 Contract.OldValue<T>(e),其中 Te 的类型。It uses the expression Contract.OldValue<T>(e), where T is the type of e. 每次编译器可推断出类型时,都可发出泛型类型参数。You can omit the generic type argument whenever the compiler is able to infer its type. (例如, C#编译器始终会推断类型,因为它采用了参数。)e 和可能出现旧表达式的上下文有几个限制。(For example, the C# compiler always infers the type because it takes an argument.) There are several restrictions on what can occur in e and the contexts in which an old expression may appear. 旧表达式中不能包含其他旧表达式。An old expression cannot contain another old expression. 最重要的是,旧表达式必须引用方法前置条件状态中的一个值。Most importantly, an old expression must refer to a value that existed in the method's precondition state. 换言之,只要方法前置条件为 true,此表达式都必须可以进行计算。In other words, it must be an expression that can be evaluated as long as the method's precondition is true. 以下是此规则的几个实例。Here are several instances of that rule.

    • 方法的前置条件状态中必须存在值。The value must exist in the method's precondition state. 若要引用对象上的字段,前提条件必须保证对象始终为非 null。In order to reference a field on an object, the preconditions must guarantee that the object is always non-null.

    • 不能引用旧表达式中方法的返回值:You cannot refer to the method's return value in an old expression:

      Contract.OldValue(Contract.Result<int>() + x) // ERROR
      
    • 不能引用旧表达式中的 out 参数。You cannot refer to out parameters in an old expression.

    • 如果限定符的范围取决于方法的返回值,则旧表达式不能依赖限定符的绑定变量:An old expression cannot depend on the bound variable of a quantifier if the range of the quantifier depends on the return value of the method:

      Contract.ForAll(0, Contract.Result<int>(), i => Contract.OldValue(xs[i]) > 3); // ERROR
      
    • 旧表达式不能引用 ForAllExists 调用中的匿名委托的参数,除非它被用作方法调用的索引器或自变量:An old expression cannot refer to the parameter of the anonymous delegate in a ForAll or Exists call unless it is used as an indexer or argument to a method call:

      Contract.ForAll(0, xs.Length, i => Contract.OldValue(xs[i]) > 3); // OK
      Contract.ForAll(0, xs.Length, i => Contract.OldValue(i) > 3); // ERROR
      
    • 如果旧表达式的值取决于匿名委托的任一参数,匿名委托的主体中不能出现旧表达式,除非匿名委托是 ForAllExists 方法的参数:An old expression cannot occur in the body of an anonymous delegate if the value of the old expression depends on any of the parameters of the anonymous delegate, unless the anonymous delegate is an argument to the ForAll or Exists method:

      Method(... (T t) => Contract.OldValue(... t ...) ...); // ERROR
      
    • Out 参数出现问题,因为协定显示在方法主体之前,而大多数编译器不允许引用后置条件中的 out 参数。Out parameters present a problem because contracts appear before the body of the method, and most compilers do not allow references to out parameters in postconditions. 若要解决此问题,Contract 类需提供 ValueAtReturn 方法,它允许基于 out 参数的后置条件。To solve this problem, the Contract class provides the ValueAtReturn method, which allows a postcondition based on an out parameter.

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

      OldValue 方法一样,每次编译器能推断出类型时都可发出泛型类型参数。As with the OldValue method, you can omit the generic type parameter whenever the compiler is able to infer its type. 协定重写程序将方法调用替换为 out 参数的值。The contract rewriter replaces the method call with the value of the out parameter. ValueAtReturn 方法仅可在后置条件中出现。The ValueAtReturn method may appear only in postconditions. 方法的自变量必须为 out 参数或结构 out 参数的字段。The argument to the method must be an out parameter or a field of a structure out parameter. 在引用结构构造函数后置条件中的字段时,后者也非常有用。The latter is also useful when referring to fields in the postcondition of a structure constructor.

      备注

      目前,代码协定分析工具不会检查 out 参数是否正确初始化,并且忽略它在后置条件中的描述。Currently, the code contract analysis tools do not check whether out parameters are initialized properly and disregard their mention in the postcondition. 因此,在先前示例中,如果协定后面的行使用了 x 的值而不是为其分配一个整数,编译器不会发出正确错误。Therefore, in the previous example, if the line after the contract had used the value of x instead of assigning an integer to it, a compiler would not issue the correct error. 但是,在未定义 CONTRACTS_FULL 预处理器符号的版本(如 asa 发布版本)中,编译器将发出错误。However, on a build where the CONTRACTS_FULL preprocessor symbol is not defined (such asa release build), the compiler will issue an error.

固定协定Invariants

对象固定是指无论何时对象对客户端可见都应适合类的每个实例的条件。Object invariants are conditions that should be true for each instance of a class whenever that object is visible to a client. 它们表示对象被视为正确的条件。They express the conditions under which the object is considered to be correct.

固定协定方法的标识方式是以 ContractInvariantMethodAttribute 属性进行标记。The invariant methods are identified by being marked with the ContractInvariantMethodAttribute attribute. 除了 Invariant 方法的调用序列(其中每个调用指定一个固定协定),固定协定方法不可包含任何代码,如以下示例所示。The invariant methods must contain no code except for a sequence of calls to the Invariant method, each of which specifies an individual invariant, as shown in the following example.

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

固定协定由 CONTRACTS_FULL 预处理器符号有条件地进行定义。Invariants are conditionally defined by the CONTRACTS_FULL preprocessor symbol. 在运行时检查期间,每次公共方法结束都要检查固定协定。During run-time checking, invariants are checked at the end of each public method. 如果固定协定提到相同类中的公共方法,则将禁用通常在此公共方法结束时执行的固定协定检查。If an invariant mentions a public method in the same class, the invariant check that would normally happen at the end of that public method is disabled. 相反,仅在此方法的最外层方法调用结束时进行检查。Instead, the check occurs only at the end of the outermost method call to that class. 如果因调用其他类上的方法而重新输入类,也会发生此类情况。This also happens if the class is re-entered because of a call to a method on another class. 不会检查对象终结器和 IDisposable.Dispose 实现的固定条件。Invariants are not checked for an object finalizer and an IDisposable.Dispose implementation.

使用指南Usage Guidelines

协定顺序Contract Ordering

下表显示编写方法协定时应使用的元素顺序。The following table shows the order of elements you should use when you write method contracts.

If-then-throw statements 向后兼容的公共前置条件Backward-compatible public preconditions
Requires 所有公共前置条件。All public preconditions.
Ensures 所有的公共(正常)后置条件。All public (normal) postconditions.
EnsuresOnThrow 所有的公共(正常)后置条件。All public exceptional postconditions.
Ensures 所有的私有/内部(正常)后置条件。All private/internal (normal) postconditions.
EnsuresOnThrow 所有的私有/内部(正常)后置条件。All private/internal exceptional postconditions.
EndContractBlock 如果使用没有任何其他协定的 if-then-throw 样式前置条件,请调用 EndContractBlock 以表示之前所有的 if 检查均为前置条件。If using if-then-throw style preconditions without any other contracts, place a call to EndContractBlock to indicate that all previous if checks are preconditions.

纯度Purity

协定中调用的所有方法都必须是纯方法;即,它们不能更新任何预存在的状态。All methods that are called within a contract must be pure; that is, they must not update any preexisting state. 纯方法可修改输入纯方法后创建的对象。A pure method is allowed to modify objects that have been created after entry into the pure method.

目前代码协定工具假定以下代码元素为纯元素:Code contract tools currently assume that the following code elements are pure:

  • 标记有 PureAttribute 的方法。Methods that are marked with the PureAttribute.

  • 标记有 PureAttribute(此属性适用于所有类型的方法)的类型。Types that are marked with the PureAttribute (the attribute applies to all the type's methods).

  • 属性 get 访问器。Property get accessors.

  • 运算符(名称以“op”开头且具有一个或两个参数和非 void 返回类型的静态方法)。Operators (static methods whose names start with "op", and that have one or two parameters and a non-void return type).

  • 完全限定名以“System.Diagnostics.Contracts.Contract”、“System.String”、“System.IO.Path”或“System.Type”开头的所有方法。Any method whose fully qualified name begins with "System.Diagnostics.Contracts.Contract", "System.String", "System.IO.Path", or "System.Type".

  • 任何调用的委托,前提条件是委托类型本身具有 PureAttribute 属性。Any invoked delegate, provided that the delegate type itself is attributed with the PureAttribute. 委托类型 System.Predicate<T>System.Comparison<T> 被视为纯类型。The delegate types System.Predicate<T> and System.Comparison<T> are considered pure.

可见性Visibility

协定中提到的所有成员至少必须与包含它们的方法一样可见。All members mentioned in a contract must be at least as visible as the method in which they appear. 例如,公共方法的前置条件中不可提及私有字段;客户端在调用方法前不可验证此类协定。For example, a private field cannot be mentioned in a precondition for a public method; clients cannot validate such a contract before they call the method. 但是,如果字段标记有 ContractPublicPropertyNameAttribute,则不受这些规则限制。However, if the field is marked with the ContractPublicPropertyNameAttribute, it is exempt from these rules.

示例Example

下面的示例显示了代码协定的用法。The following example shows the use of code contracts.

#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