学步园

代码契约的核心静态类System.Diagnostics.Contracts.Contract http://msdn.microsoft.com/zh-cn/library/system.diagnostics.contracts.contract.aspx

 public static class Contract
    {
// 摘要:
//     协定失败时发生。
        public static event EventHandler<ContractFailedEventArgs> ContractFailed;

// 摘要:
//     检查条件；如果条件为 false，则遵循为分析器设置的升级策略。
//
// 参数:
//   condition:
//     要测试的条件表达式。
        [Conditional("DEBUG")]
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
        [Conditional("CONTRACTS_FULL")]
public static void Assert(bool condition);
//
// 摘要:
//     检查条件；如果条件为 false，则遵循由分析器设置的升级策略，并显示指定的消息。
//
// 参数:
//   condition:
//     要测试的条件表达式。
//
//   userMessage:
//     在不满足条件时要显示的消息。
        [Conditional("CONTRACTS_FULL")]
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
        [Conditional("DEBUG")]
public static void Assert(bool condition, string userMessage);
//
// 摘要:
//     指示代码分析工具假设指定的条件为 true（即使无法静态地证明该条件始终为 true）。
//
// 参数:
//   condition:
//     假设为 true 的条件表达式。
        [Conditional("CONTRACTS_FULL")]
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
        [Conditional("DEBUG")]
public static void Assume(bool condition);
//
// 摘要:
//     指示代码分析工具假设某个条件为 true（即使无法静态地证明该条件始终为 true），并在假设失败时显示一条消息。
//
// 参数:
//   condition:
//     假设为 true 的条件表达式。
//
//   userMessage:
//     假设失败时要发布的消息。
        [Conditional("CONTRACTS_FULL")]
        [Conditional("DEBUG")]
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
public static void Assume(bool condition, string userMessage);
//
// 摘要:
//     当方法的协定仅包含 if-then-throw 形式的前置条件时，标记协定部分的结尾。
        [Conditional("CONTRACTS_FULL")]
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.Success)]
public static void EndContractBlock();
//
// 摘要:
//     为封闭方法或属性指定一个后置条件协定。
//
// 参数:
//   condition:
//     要测试的条件表达式。该表达式可以包括 System.Diagnostics.Contracts.Contract.OldValue<T0>(T0)、System.Diagnostics.Contracts.Contract.ValueAtReturn<T0>(T0@)
//     和 System.Diagnostics.Contracts.Contract.Result<T0>() 值。
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
        [Conditional("CONTRACTS_FULL")]
public static void Ensures(bool condition);
//
// 摘要:
//     为提供的退出条件指定后置条件协定，并指定条件为 false 时要显示的消息。
//
// 参数:
//   condition:
//     要测试的条件表达式。该表达式可以包括 System.Diagnostics.Contracts.Contract.OldValue<T0>(T0)
//     和 System.Diagnostics.Contracts.Contract.Result<T0>() 值。
//
//   userMessage:
//     表达式不为 true 时要显示的消息。
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
        [Conditional("CONTRACTS_FULL")]
public static void Ensures(bool condition, string userMessage);
//
// 摘要:
//     基于提供的异常和条件为封闭方法或属性指定一个后置条件协定。
//
// 参数:
//   condition:
//     要测试的条件表达式。
//
// 类型参数:
//   TException:
//     引发后置条件检查的异常的类型。
        [Conditional("CONTRACTS_FULL")]
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
public static void EnsuresOnThrow<TException>(bool condition) where TException : Exception;
//
// 摘要:
//     基于提供的异常和条件为封闭方法或属性指定后置条件协定，并指定条件为 false 时要显示的消息。
//
// 参数:
//   condition:
//     要测试的条件表达式。
//
//   userMessage:
//     表达式为 false 时要显示的消息。
//
// 类型参数:
//   TException:
//     引发后置条件检查的异常的类型。
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
        [Conditional("CONTRACTS_FULL")]
public static void EnsuresOnThrow<TException>(bool condition, string userMessage) where TException : Exception;
//
// 摘要:
//     确定函数中是否存在某个元素集合中的元素。
//
// 参数:
//   collection:
//     将从中提取 T 类型的元素以将其传递给 predicate 的集合。
//
//   predicate:
//     用于计算 collection 中某个元素的函数。
//
// 类型参数:
//   T:
//     collection 中包含的类型。
//
// 返回结果:
//     当且仅当 predicate 对于 collection 中的 T 类型的任何元素都返回 true 时，才为 true。
//
// 异常:
//   System.ArgumentNullException:
//     collection 或 predicate 为 null。
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
public static bool Exists<T>(IEnumerable<T> collection, Predicate<T> predicate);
//
// 摘要:
//     确定指定的测试对某个整数范围中的任何整数是否为 true。
//
// 参数:
//   fromInclusive:
//     要传递给 predicate 的第一个整数。
//
//   toExclusive:
//     要传递给 predicate 的最后一个整数加一。
//
//   predicate:
//     用于计算指定范围内整数的任何值的函数。
//
// 返回结果:
//     如果 predicate 对于从 fromInclusive 开始到 toExclusive - 1 的范围内的任何整数都返回 true，则为 true。
//
// 异常:
//   System.ArgumentNullException:
//     predicate 为 null。
//
//   System.ArgumentException:
//     toExclusive  小于 fromInclusive。
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
public static bool Exists(int fromInclusive, int toExclusive, Predicate<int> predicate);
//
// 摘要:
//     确定函数中是否存在某个集合中的所有元素。
//
// 参数:
//   collection:
//     将从中提取 T 类型的元素以将其传递给 predicate 的集合。
//
//   predicate:
//     用于计算 collection 中所有元素是否存在的函数。
//
// 类型参数:
//   T:
//     collection 中包含的类型。
//
// 返回结果:
//     当且仅当 predicate 对于 collection 中的 T 类型的所有元素都返回 true 时，才为 true。
//
// 异常:
//   System.ArgumentNullException:
//     collection 或 predicate 为 null。
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
public static bool ForAll<T>(IEnumerable<T> collection, Predicate<T> predicate);
//
// 摘要:
//     确定某个特定条件是否对指定范围内的所有整数都有效。
//
// 参数:
//   fromInclusive:
//     要传递给 predicate 的第一个整数。
//
//   toExclusive:
//     要传递给 predicate 的最后一个整数加一。
//
//   predicate:
//     要计算其中是否存在指定范围内的整数的函数。
//
// 返回结果:
//     如果 predicate 对于从 fromInclusive 开始到 toExclusive - 1 的范围内的所有整数都返回 true，则为 true。
//
// 异常:
//   System.ArgumentNullException:
//     predicate 为 null。
//
//   System.ArgumentException:
//     toExclusive  小于 fromInclusive。
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
public static bool ForAll(int fromInclusive, int toExclusive, Predicate<int> predicate);
//
// 摘要:
//     为封闭类指定一个固定协定。
//
// 参数:
//   condition:
//     要测试的条件表达式。
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
        [Conditional("CONTRACTS_FULL")]
public static void Invariant(bool condition);
//
// 摘要:
//     为封闭类指定一个固定协定，并在该协定的条件失败时显示一条消息。
//
// 参数:
//   condition:
//     要测试的条件表达式。
//
//   userMessage:
//     条件为 false 时要显示的消息。
        [Conditional("CONTRACTS_FULL")]
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
public static void Invariant(bool condition, string userMessage);
//
// 摘要:
//     表示方法或属性开始时的值。
//
// 参数:
//   value:
//     要表示的值（字段或参数）。
//
// 类型参数:
//   T:
//     值的类型。
//
// 返回结果:
//     一个方法或属性开始处的参数或字段的值。
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.Success)]
public static T OldValue<T>(T value);
//
// 摘要:
//     为封闭方法或属性指定一个前置条件协定，并在该协定的条件失败时引发异常。
//
// 参数:
//   condition:
//     要测试的条件表达式。
//
// 类型参数:
//   TException:
//     条件为 false 时要引发的异常。
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
public static void Requires<TException>(bool condition) where TException : Exception;
//
// 摘要:
//     为封闭方法或属性指定一个前置条件协定。
//
// 参数:
//   condition:
//     要测试的条件表达式。
        [Conditional("CONTRACTS_FULL")]
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
public static void Requires(bool condition);
//
// 摘要:
//     为封闭方法或属性指定一个前置条件协定，并在该协定的条件失败时显示一条消息。
//
// 参数:
//   condition:
//     要测试的条件表达式。
//
//   userMessage:
//     条件为 false 时要显示的消息。
        [Conditional("CONTRACTS_FULL")]
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
public static void Requires(bool condition, string userMessage);
//
// 摘要:
//     为封闭方法或属性指定一个前置条件协定，并在该协定的条件失败时引发异常，其中包含提供的消息。
//
// 参数:
//   condition:
//     要测试的条件表达式。
//
//   userMessage:
//     条件为 false 时要显示的消息。
//
// 类型参数:
//   TException:
//     条件为 false 时要引发的异常。
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.MayFail)]
public static void Requires<TException>(bool condition, string userMessage) where TException : Exception;
//
// 摘要:
//     表示一个方法或属性的返回值。
//
// 类型参数:
//   T:
//     封闭方法或属性的返回值的类型。
//
// 返回结果:
//     封闭方法或属性的返回值。
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.Success)]
public static T Result<T>();
//
// 摘要:
//     表示从一个方法返回时 out 参数的最终（输出）值。
//
// 参数:
//   value:
//     out 参数。
//
// 类型参数:
//   T:
//     out 参数的类型。
//
// 返回结果:
//     out 参数的输出值。
        [ReliabilityContract(Consistency.WillNotCorruptState, Cer.Success)]
public static T ValueAtReturn<T>(out T value);
    }

如果要使用契约式编程，必须下载额外的工具和一个vs属性窗格。网址是：http://msdn.microsoft.com/en-us/devlabs/dd491992.aspx
因为Contract的有些方法使用了  ConditionalAttribute

上面的工作完成后，才能开始下面的学习！

你也可以在使用契约的代码文件中使用 #define 定义自己使用方法的契约，当然。这并不是好的做法，只是为了说明问题。

契约式编程不是一门崭新的编程方法论。C/C++ 时代早已有之。Microsoft 在 .NET 4.0 中正式引入契约式编程库。博主以为契约式编程是一种相当不错的编程思想，每一个开发人员都应该掌握。它不但可以使开发人员的思维更清晰，而且对于提高程序 性能很有帮助。值得一提的是，它对于并行程序设计也有莫大的益处。

我们先看一段很简单的，未使用契约式编程的代码示例。

// .NET 代码示例
public class RationalNumber
{
private int numberator;
private int denominator;

public RationalNumber(int numberator, int denominator)
    {
this.numberator = numberator;
this.denominator = denominator;
    }

public int Denominator
    {
get
{
return this.denominator;
        }
    }
}

上述代码表示一个在 32 位有符号整型范围内的有理数。数学上，有理数是一个整数 a 和一个非零整数 b 的比，通常写作 a/b，故又称作分数(题外话：有理数这个翻译真是够奇怪)。由此，我们知道，有理数的分母不能为 0 。所以，上述代码示例的构造函数还需要写些防御性代码。通常 .NET 开发人员会这样写：

// .NET 代码示例
public class RationalNumber
{
private int numberator;
private int denominator;

public RationalNumber(int numberator, int denominator)
    {
if (denominator == 0)
throw new ArgumentException("The second argument can not be zero.");
this.numberator = numberator;
this.denominator = denominator;
    }

public int Denominator
    {
get
{
return this.denominator;
        }
    }
}

下面我们来看一下使用契约式编程的 .NET 4.0 代码示例。为了更加方便的说明，博主在整个示例上都加了契约，但此示例并非一定都加这些契约。

// .NET 代码示例
public class RationalNumber
{
private int numberator;
private int denominator;

public RationalNumber(int numberator, int denominator)
    {
Contract.Requires(denominator != 0, "The second argument can not be zero.");
this.numberator = numberator;
this.denominator = denominator;
    }

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

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

详细的解释稍后再说。按理，既然契约式编程有那么多好处，那在 C/C++ 世界应该很流行才对。为什么很少看到关于契约式编程的讨论呢？看一下 C++ 的契约式编程示例就知道了。下面是 C++ 代码示例：

//typedef long int32_t;
#include <stdint.h>

template
inline void CheckInvariant(T& argument)
{
#ifdef CONTRACT_FULL
argument.Invariant();
#endif
}

public class RationalNumber
{
private:
    int32_t numberator;
    int32_t denominator;

public:
    RationalNumber(int32_t numberator, int32_t denominator)
    {
#ifdef CONTRACT_FULL
ASSERT(denominator != 0);
        CheckInvaraint(*this);
#endif
        this.numberator = numberator;
this.denominator = denominator;
#ifdef CONTRACT_FULL
CheckInvaraint(*this);
#endif
}

public:
    int32_t GetDenominator()
    {
#ifdef CONTRACT_FULL
// C++ Developers like to use struct type.
        class Contract
        {
            int32_t Result;
            Contract()
            {
            }
            ~Contract()
            {
            }
        }
#endif
#ifdef CONTRACT_FULL
Contract contract = new Contract();
        contract.Result = denominator;
        CheckInvairant(*this);
#endif
        return this.denominator;
#ifdef CONTRACT_FULL
CheckInvaraint(*this);
#endif
}

protected:
#ifdef CONTRACT_FULL
virtual void Invariant()
    {
        this.denominator != 0;
    }
#endif
}

Woo..., 上述代码充斥了大量的宏和条件编译。对于习惯了 C# 优雅语法的 .NET 开发人员来说，它们是如此丑陋。更重要的是，契约式编程在 C++ 世界并未被标准化，因此项目之间的定义和修改各不一样，给代码造成很大混乱。这正是很少在实际中看到契约式编程应用的原因。但是在 .NET 4.0 中，契约式编程变得简单优雅起来。.NET 4.0 提供了契约式编程库。实际上，.NET 4.0 仅仅是针对 C++ 宏和条件编译的再次抽象和封装。它完全基于 CONTRACTS_FULL， CONTRACTS_PRECONDITIONS Symbol 和 System.Diagnostics.Debug.Assert 方法、System.Environment.FastFail 方法的封装。

那么，何谓契约式编程？

何谓契约式编程

契约是减少大型项目成本的突破性技术。它一般由 Precondition(前置条件)， Postcondition(后置条件) 和 Invariant(不变量) 等概念组成。.NET 4.0 除上述概念之外，还增加了 Assert(断言)，Assume(假设) 概念。这可以由枚举 ContractFailureKind 类型一窥端倪。

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

正如前所述，.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() 方法的参数。

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 现