详解.NET 4.0 中的契约式编程结合例子(2)

3. Preconditions

.NET 4.0 使用 Contract.Requires() 方法表示 Preconditions(前置条件) 契约。它表示方法被调用时方法状态的契约，通常被用来做参数验证。所有 Preconditions 契约相关成员，至少方法本身可以访问。

Contract.Requires(x != null);

Preconditions 契约的运行时行为依赖于几个因素。如果只隐式定义了 CONTRACTS PRECONDITIONS 标记，而没有定义 CONTRACTS_FULL 标记，那么只会进行检测 Preconditions 契约，而不会检测任何 Postconditions 和 Invariants 契约。假如违反了 Preconditions 契约，那么 CLR 会调用 Debug.Assert(false) 和 Environment.FastFail 方法。

假如想保证 Preconditions 契约在任何编译中都发挥作用，可以使用下面这个方法：

Contract.RequiresAlways(x != null);

为了保持向后兼容性，当已存在的代码不允许被修改时，我们需要抛出指定的精确异常。但是在 Preconditions 契约中，有一些格式上的限定。如下代码所示：

if (x == null) throw new ArgumentException("The argument can not be null.");
Contract.EndContractBlock();    // 前面所有的 if 检测语句皆是 Preconditions 契约

这种 Preconditions 契约的格式严格受限：它必须严格按照上述代码示例格式。而且不能有 else 从句。此外，then 从句也只能有单个 throw 语句。最后必须使用 Contract.EndContractBlock() 方法来标记 Preconditions 契约结束。

看到这里，是不是觉得大多数参数验证都可以被 Preconditions 契约替代？没有错，事实的确如此。这样这些防御性代码完全可以在 Release 被去掉，从而不用做那些冗余的代码检测，从而提高程序性能。但在面向验证客户输入此类情境下，防御性代码仍有必要。再就是，Microsoft 为了保持兼容性，并没有用 Preconditions 契约代替异常。

4. Postconditions

Postconditions 契约表示方法终止时的状态。它跟 Preconditions 契约的运行时行为完全一致。但与 Preconditions 契约不同，Postconditions 契约相关的成员有着更少的可见性。客户程序或许不会理解或使用 Postconditions 契约表示的信息，但这并不影响客户程序正确使用 API 。

对于 Preconditions 契约来说，它则对客户程序有副作用：不能保证客户程序不违反 Preconditions 契约。

A. 标准 Postconditions 契约用法

.NET 4.0 使用 Contract.Ensures() 方法表示标准 Postconditions 契约用法。它表示方法正常终止时必须保持的契约。

Contract.Ensures(this.F > 0);

B. 特殊 Postconditions 契约用法

当从方法体内抛出一个特定异常时，通常情况下 .NET CLR 会从方法体内抛出异常的位置直接跳出，从而辗转堆栈进行异常处理。假如我们需要在异常抛出时还要进行 Postconditions 契约验证，我们可以如下使用：

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

其中小括号内的参数表示当异常从方法内抛出时必须保持的契约，而泛型参数表示异常发生时抛出的异常类型。举例来说，当我们把 T 用 Exception 表示时，无论什么类型的异常被抛出，都能保证 Postconditions 契约。哪怕这个异常是堆栈溢出或任何不能控制的异常。强烈推荐当异常是被调用 API 一部分时，使用 Contract.EnsuresOnThrows<T>() 方法。

C. Postconditions 契约内的特殊方法

以下要讲的这几个特殊方法仅限使用在 Postconditions 契约内。

方法返回值 在 Postconditions 契约内，可以通过 Contract.Result<T>() 方法表示，其中 T 表示方法返回类型。当编译器不能推导出 T 类型时，我们必须显式指出。比如，C# 编译器就不能推导出方法参数类型。

Contract.Ensures(0 < Contract.Result<int>());

假如方法返回 void ，则不必在 Postconditions 契约内使用 Contract.Result<T>() 。

前值(旧值)  在 Postconditions 契约内，通过 Contract.OldValue<T>(e) 表示旧有值，其中 T 是 e 的类型。当编译器能够推导 T 类型时，可以忽略。此外 e 和旧有表达式出现上下文有一些限制。旧有表达式只能出现在 Postconditions 契约内。旧有表达式不能包含另一个旧有表达式。一个很重要的原则就是旧有表达式只能引用方法已经存在的那些旧值。比如，只要方法 Preconditions 契约持有，它必定能被计算。下面是这个原则的一些示例：

• 方法的旧有状态必定存在其值。比如 Preconditions 契约暗含 xs != null ，xs 当然可以被计算。但是，假如 Preconditions 契约为 xs != null || E(E 为任意表达式)，那么 xs 就有可能不能被计算。

Contract.OldValue(xs.Length);  // 很可能错误

• 方法返回值不能被旧有表达式引用。

Contract.OldValue(Contract.Result<int>() + x);  // 错误

• out 参数也不能被旧有表达式引用。
• 如果某些标记的方法依赖方法返回值，那么这些方法也不能被旧有表达式引用。

Contract.ForAll(0, Contract.Result<int>(), i => Contract.OldValue(xs[i]) > 3);  // 错误

• 旧有表达式不能在 Contract.ForAll() 和 Contract.Exists() 方法内引用匿名委托参数，除非旧有表达式被用作索引器或方法调用参数。

Contract.ForAll(0, xs.Length, i => Contract.OldValue(xs[i]) > 3);  // OK

Contract.ForAll(0, xs.Length, i => Contract.OldValue(i) > 3);  // 错误

• 如果旧有表达式依赖于匿名委托的参数，那么旧有表达式不能在匿名委托的方法体内。除非匿名委托是 Contract.ForAll() 和 Contract.Exists() 方法的参数。

Foo( ... (T t) => Contract.OldValue(... t ...) ... ); // 错误

D. out 参数

因为契约出现在方法体前面，所以大多数编译器不允许在 Postconditions 契约内引用 out 参数。为了绕开这个问题，.NET 契约库提供了 Contract.ValueAtReturn<T>(out T t) 方法。

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

跟 OldValue 一样，当编译器能推导出类型时，泛型参数可以被忽略。该方法只能出现在 Postconditions 契约。方法参数必须是 out 参数，且不允许使用表达式。

需要注意的是，.NET 目前的工具不能检测确保 out 参数是否正确初始化，而不管它是否在 Postconditions 契约内。因此， x = 3 语句假如被赋予其他值时，编译器并不能发现错误。但是，当编译 Release 版本时，编译器将发现该问题。

5. Object Invariants

对象不变量表示无论对象是否对客户程序可见，类的每一个实例都应该保持的契约。它表示对象处于一个“良好”状态。

在 .NET 4.0 中，对象的所有不变量都应当放入一个受保护的返回 void 的实例方法中。同时用[ContractInvariantMethod]特性标记该方法。此外，该方法体内在调用一系列 Contract.Invariant() 方法后不能再有其他代码。通常我们会把该方法命名为 ObjectInvariant 。

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

同样，Object Invariants 契约的运行时行为和 Preconditions 契约、Postconditions 契约行为一致。CLR 运行时会在每个公共方法末端检测 Object Invariants 契约，但不会检测对象终结器或任何实现 System.IDisposable 接口的方法。

6. Contract 静态类中的其他特殊方法

.NET 4.0 契约库中的 Contract 静态类还提供了几个特殊的方法。它们分别是：

A. ForAll

Contract.ForAll() 方法有两个重载。第一个重载有两个参数：一个集合和一个谓词。谓词表示返回布尔值的一元方法，且该谓词应用于集合中的每一个元素。任何一个元素让谓词返回 false ，ForAll 停止迭代并返回 false 。否则， ForAll 返回 true 。下面是一个数组内所有元素都不能为 null 的契约示例：

public T[] Foo<T>(T[] array)
{
    Contract.Requires(Contract.ForAll(array, (T x) => x != null));
}

B. Exists

它和 ForAll 方法差不多。