[转]代码协定

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

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

代码协定的优点包括：

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

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

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

有关使用代码协定的详细说明和工具，请参见 MSDN DevLabs 网站上的e Code Contracts。

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。