由于 .NET 要求显式实现接口方法，所以在契约内引用相同接口的其他方法就显得很笨拙。由此，.NET 允许在契约方法之前，使用一个局部变量引用接口类型。如下所示：
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 类型参数的重载版本。如下所示：
这样当契约被违反时，.NET 可以在运行时提供一个信息提示。目前，该字符串只能是编译时常量。但是，将来 .NET 可能会改变，字符串可以运行时被计算。但是，如果是字符串常量，静态诊断工具可以选择显示它。
10. 契约特性
A. ContractClass 和 ContractClassFor
这两个特性，我们已经在接口契约和抽象方法契约里看到了。ContractClass 特性用于添加到接口或抽象类型上，但是指向的却是实现该类型的帮助类。ContractClassFor 特性用来添加到帮助类上，指向我们需要契约验证的接口或抽象类型。
B. ContractInvariantMethod
这个特性用来标记表示对象不变量的方法。
C. Pure
Pure 特性只声明在那些没有副作用的方法调用者上。.NET 现存的一些委托可以被认为如此，比如 System.Predicate<T> 和 System.Comparison<T>。
D. RuntimeContracts
这是个程序集级别的特性(具体如何，俺也不太清楚)。
E. ContractPublicPropertyName
这个特性用在字段上。它被用在方法契约中，且该方法相对于字段来说，更具可见性。比如私有字段和公共方法。如下所示：
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 契约。
