在已经介绍过，代码协定的基本内容包括三大契约：前置条件、后置条件，以及类不变项。本文就简单的介绍一下这三大契约的使用方法。
前置条件（precondiction）：
前置条件主要用来标记执行该函数之前满足的条件。前置条件必须由调用方来满足的，如果前置条件不满足是，函数不予执行，以便于我们提前感知错误。一种非常常见的前置条件就是参数的有效性检查。例如，对如如下代码：
int GetValue(int index) { if ((index <0) || (index >= array.Length)) throw new IndexOutOfRangeException("索引超出范围"); return array[index]; }
改函数的第一句的入参检查就是一个前置条件判断。
在Code Contract框架中，我们可以使用Contract.Eqquires来验证前置条件，上述代码则可以 改写如下：
int GetValue(int index) { Contract.Requires((index > 0) && (index < array.Length)); return array[index]; }
与前面的if-else形式的判断相比，判断条件稍微有所不同：if-else是判断参数的无效条件，而Contract.Equires则是判断参数的有效条件。不过实现的功能都是在参数无效的时候，抛异常阻止函数的进一步运行。
当Contract.Equires验证失败时，则会抛出一个ContractException，错误信息为：前置条件失败: (index > 0) && (index < array.Length)。本身这个异常对于程序员来说是非常不错的，但是有的时候我们需要把它转换为用户可以理解的更加友好点的提示信息，此时则可以使用如下重载形式：
Contract.Requires<TException>(bool condition) Contract.Requires(bool condition, string userMessage) Contract.Requires<TException>(bool condition, string userMessage)
基本上看着参数就知道怎么用了，就不多介绍了。
使用限制：由于前置条件是在执行函数前检查的，因此Contract.Eqquires要求在函数体开始的位置，否则编译的时候会报错。
后置条件（postcondion）：
和前置条件相对的，后置条件则是在函数执行完后应该满足的条件。前置条件必须由函数体方来满足的，如果后置条件不满足是，函数执行出错，以便于我们快速感知错误。后置条件比较常见的任务是函数返回值的判断，例如，对于如下代码：
object GetValue(int index) { object output = array[index]; if (output == null) throw new InvalidOperationException(); return output; }
其中高亮部分就是一个后置条件的判断。在Code Contract中我们则可以用Contract.Ensures来实现后置条件：
object GetValue(int index) { Contract.Ensures(Contract.Result<object>() != null); return array[index]; }
从上面的代码中可以看到，使用Code Contract来实现后置条件是比在代码中按照常规的方式编码要简介不少的，主要体现在如下几个方面：
- 无需用临时变量来保存返回值
- 写在函数的开头，只需实现一次。而常规编码的方式则需要在每一个返回的分支都判断一次。
Contract.Ensures的这两个特性可以看作是Code Contract的语法糖，它之所以能实现这样的功能，并非编译器级别的支持，而是通过在程序集中注入了相应的功能的，类似一个隐式的代码生成器。另外，还可以通过编译开关随时关闭Contract.Ensures的代码，Release版本中关掉检查可以提高运行效率。
Contract.Ensures也有好几个重载版本：
Contract.Ensures(bool condition, string userMessage) Contract.Ensures(bool condition, string userMessage); Contract.EnsuresOnThrow<TException>(bool condition) Contract.EnsuresOnThrow<TException>(bool condition, string userMessage)
另外，Contract.Ensures经常和几个语法糖函数一起使用的，如前面介绍过的Contract.Result<T>()，Contract.OldValue<T>(T value)和Contract.ValueAtReturn<T>(out T value)也是非常常用的。
类不变项（class invariant）
类不变项也是提供了一个约定条件，函数体需要保证在函数执行前后，该约定为真。使用类不变项的方式如下：
public int CurrentIndex { get; set; } [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(CurrentIndex >= 0); }
类不变项契约条件是作为一个单独的函数声明的，要在函数前加上ContractInvariantMethodAttribute标记，函数体中使用Contract.Invariant函数声明条件。
当函数执行的条件不满足该条件时，即抛出异常。如：
public void Foo() { CurrentIndex = -5; }
这个功能也是类似一种语法糖，实际上Code Contract框架应该是将检查函数嵌入到每个成员函数的首尾中了的。