契约式编程

契约的思想很简单。它只是一组结果为真的表达式。如若不然，契约就被违反。那按照定义，程序中就存在纰漏。契约构成了程序规格说明的一部分，只不过该说明从文档挪到了代码中。开发人员都知道，文档通常不完整、过时，甚至不存在。将契约挪移到代码中，就使得程序可以被验证。

正如前所述，.NET 4.0 对宏和条件编译进行抽象封装。这些成果大多集中在 System.Diagnostics.Contracts.Contract 静态类中。该类中的大多数成员都是条件编译。这样，我们就不用再使用 #ifdef 和定义 CONTRACTS_FULL 之类的标记。更重要的是，这些行为被标准化，可以在多个项目中统一使用，并根据情况是否生成带有契约的程序集。

1. Assert

Assert(断言)是最基本的契约。.NET 4.0 使用 Contract.Assert() 方法来特指断言。它用来表示程序点必须保持的一个契约。

Contract.Assert(this.privateField > 0); Contract.Assert(this.x == 3, "Why isn’t the value of x 3?");

 

断言有两个重载方法，首参数都是一个布尔表达式，第二个方法的第二个参数表示违反契约时的异常信息。

当断言运行时失败，.NET CLR 仅仅调用 Debug.Assert 方法。成功时则什么也不做。

2. Assume

.NET 4.0 使用 Contract.Assume() 方法表示 Assume(假设) 契约。

Contract.Assume(this.privateField > 0); Contract.Assume(this.x == 3, "Static checker assumed this");

Assume 契约在运行时检测的行为与 Assert(断言) 契约完全一致。但对于静态验证来说，Assume 契约仅仅验证已添加的事实。由于诸多限制，静态验证并不能保证该契约。或许最好先使用 Assert 契约，然后在验证代码时按需修改。

当 Assume 契约运行时失败时， .NET CLR 会调用 Debug.Assert(false)。同样，成功时什么也不做。

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 方法差不多。

7. 接口契约

因为 C#/VB 编译器不允许接口内的方法带有实现代码，所以我们如果想在接口中实现契约，需要创建一个帮助类。接口和契约帮助类通过一对特性来链接。如下所示：

[ContractClass(typeof(IFooContract))] interface IFoo { int Count { get; } void Put(int value); } [ContractClassFor(typeof(IFoo))] sealed class IFooContract : IFoo { int IFoo.Count { get { Contract.Ensures(Contract.Result<int>() >= 0); return default(int); // dummy return } } void IFoo.Put(int value) { Contract.Requires(value >= 0); } }

.NET 需要显式如上述声明从而把接口和接口方法相关联起来。注意，我们不得不产生一个哑元返回值。最简单的方式就是返回 default(T)，不要使用 Contract.Result<T> 。

由于 .NET 要求显式实现接口方法，所以在契约内引用相同接口的其他方法就显得很笨拙。由此，.NET 允许在契约方法之前，使用一个局部变量引用接口类型。如下所示：

[ContractClassFor(typeof(IFoo))] sealed class IFooContract : IFoo { int IFoo.Count { get { Contract.Ensures(Contract.Result<int>() >= 0); return default(int); // dummy return } } void IFoo.Put(int value) { IFoo iFoo = this; Contract.Requires(value >= 0); Contract.Requires(iFoo.Count < 10); // 否则的话，就需要强制转型 ((IFoo)this).Count } }

8. 抽象方法契约

 

同接口类似，.NET 中抽象类中的抽象方法也不能包含方法体。所以同接口契约一样，需要帮助类来完成契约。代码示例不再给出。

9. 契约方法重载

所有的契约方法都有一个带有 string 类型参数的重载版本。如下所示：

Contract.Requires(obj != null, "if obj is null, then missiles are fired!");

 

这样当契约被违反时，.NET 可以在运行时提供一个信息提示。目前，该字符串只能是编译时常量。但是，将来 .NET 可能会改变，字符串可以运行时被计算。但是，如果是字符串常量，静态诊断工具可以选择显示它。

10. 契约特性

A. ContractClass 和 ContractClassFor

这两个特性，我们已经在接口契约和抽象方法契约里看到了。ContractClass 特性用于添加到接口或抽象类型上，但是指向的却是实现该类型的帮助类。ContractClassFor 特性用来添加到帮助类上，指向我们需要契约验证的接口或抽象类型。

B. ContractInvariantMethod

这个特性用来标记表示对象不变量的方法。

C. Pure

Pure 特性只声明在那些没有副作用的方法调用者上。.NET 现存的一些委托可以被认为如此，比如 System.Predicate<T> 和 System.Comparison<T>。

D. RuntimeContracts

这是个程序集级别的特性(具体如何，俺也不太清楚)。

E. ContractPublicPropertyName

这个特性用在字段上。它被用在方法契约中，且该方法相对于字段来说，更具可见性。比如私有字段和公共方法。如下所示：

[ContractPublicPropertyName("PublicProperty")] private int field; public int PublicProperty { get { ... } }

 

F. ContractVerification

这个特性用来假设程序集、类型、成员是否可被验证执行。我们可以使用 [ContractVerification(false)] 来显式标记程序集、类型、成员不被验证执行。

.NET 契约库目前的缺陷

 

接下来，讲一讲 .NET 契约库目前所存在的一些问题。

值类型中的不变量是被忽略的，不发挥作用。

静态检测还不能处理 Contract.ForAll() 和 Contract.Exists() 方法。

C# 迭代器中的契约问题。我们知道 Microsoft 在 C# 2.0 中添加了 yield 关键字来帮助我们完成迭代功能。它其实是 C# 编译器做的糖果。现在契约中，出现了问题。编译器产生的代码会把我们写的契约放入到 MoveNext() 方法中。这个时侯，静态检测就不能保证能够正确完成 Preconditions 契约。

Well，.NET 契约式编程到这里就结束了。嗯，就到这里了。

PS : .NET 契约库虽然已经相当优雅。但博主以为，其跟 D 语言实现的契约式编程仍有一段距离。

PS : 有谁愿意当俺的 Mentor 。您能够享受这样的权利和义务：地狱般恐怖的提问和骚扰。非不厌其烦者勿扰。