5. Object Invariants
对象不变量表示无论对象是否对客户程序可见，类的每一个实例都应该保持的契约。它表示对象处于一个“良好”状态。
在 .NET 4.0 中，对象的所有不变量都应当放入一个受保护的返回 void 的实例方法中。同时用[ContractInvariantMethod]特性标记该方法。此外，该方法体内在调用一系列 Contract.Invariant() 方法后不能再有其他代码。通常我们会把该方法命名为 ObjectInvariant 。
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 的契约示例：
{
Contract.Requires(Contract.ForAll(array, (T x) => x != null));
}
B. Exists
它和 ForAll 方法差不多。
7. 接口契约
因为 C#/VB 编译器不允许接口内的方法带有实现代码，所以我们如果想在接口中实现契约，需要创建一个帮助类。接口和契约帮助类通过一对特性来链接。如下所示：
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> 。
