代码契约组件使用详解

InfoQ 于不久前发表了.NET 代码契约组件提供下载的新闻。这个组件是对.NET 的重要补充，这次我们将提供更为详细的内容。

如果要在.NET 4.0 发布之前使用代码契约，我们可以在 Visual Studio 项目中引用程序集 Microsoft.Contracts.dll，该程序集安装在 %PROGRAMFILES%/Microsoft/Contracts/PublicAssemblies 目录下。.NET 4.0 会在 mscorlib.dll 中包含契约组件。我们可以指定契约验证，可在编译时（静态）或在运行时（动态）执行校验。契约包含几种类型：前置条件（Preconditions）、后置条件（Postconditions）、对象不变量（Object Invariants）、断言（Assertions）、假定（Assumptions）、量词（Quantifiers）、接口契约（Interface Contracts）和抽象方法契约（Abstract Method Contracts）。

前置条件使用 Contract.Requires() 进行定义，如果在编译时使用了符号（Symbol）CONTRACTS_FULL 或 CONTRACTS_PRECONDITIONS，那么 IL 中就会包含其编译结果。例如：

 
Contract.Requires( x ! = null );

如下所示，前置条件通常作为方法体中的参数验证，如下所示：

 
public Rational( int numerator, int denominator) {<br></br>    Contract.Requires( denominator ! = 0 );<br></br>    this .numerator = numerator;<br></br>    this .denominator = denominator;<br></br>}

如果不符合 Contract.Requires() 指定的条件，就会调用 Debug.Assert(false)，然后调用 Environment.FailFast()。如果不管在编译时使用哪个符号，您都希望程序集中包含前置条件，那么可以使用 Contract.RequiresAlways()。

当方法结束时，后置条件表示其结果需要满足的契约。它通过 Contract.Ensures() 方法指定，如下例所示：

 
public int Denominator {<br></br>    get {<br></br>        Contract.Ensures( Contract.Result<int></int>() != 0 );<br></br>        return this .denominator;<br></br>    }<br></br>}

虽然似乎在返回结果之前就指定了条件，实际它还是会在返回结果之后，调用者得到结果之前进行验证。

对象不变量则为每个实例指定条件。

 
[ContractInvariantMethod]<br></br>protected void ObjectInvariant () {<br></br>    Contract. Invariant ( this .denominator ! = 0 );<br></br>}<br></br>

至于其他类型的契约，断言表示为 Contract.Assert()，假定则表示为 Contract.Assume()。一个失败的 Assert() 会调用 Debug.Assert(false)。假定与运行时断言相似，不同之处在于静态检验的方式。假定用于指定“期望”应该符合的条件，而由于某些限制，该条件无法得到编译器的验证。

接口契约为接口指定条件。它们使用在关联于接口的独立类上，因为接口方法只能声明，而不能拥有方法体。对于抽象方法契约同样如此。

以下为一个使用契约的类：

可用链接： InfoQ 关于代码契约的新闻，代码契约下载（MSI），代码契约的在线文档（PDF），微软研究院的代码契约网站。

查看英文原文： Details on Using Code Contracts