代码契约（Code Contract）：它并不是语言本身的新功能，而是一些额外的工具，帮助人们控制代码边界。
代码契约之于C#，就相当于诗词歌赋之于语言。 --- C# in Depth
一，概述
1.1 未引入“代码契约（特指MS代码契约）”之前的状态---“契约”
• 契约：20世纪80年代，Bertand Meyer在设计Eiffel语言时就将其作为重要的部分。已有大量的计算机科学研究开始探究正式的规范说明和验证，它允许在编译时检查程序的正确性，不过契约的作用还不止于此。
• 契约编程的核心理念是将API的需求和承诺与实现相分离。
• 契约约定比文档约定方式更“同步”一些。
• 或使用Debug.Assert方式，但其不能在Release构建时不会捕获非法参数。
/************************使用代码契约方式之前*****************************/
/// <summary> /// Counts the number of whitespace characters in <paramref name="text"/> /// </summary> /// <param name="text">String to examine. Must not be null.</param> /// <example cref="ArgumentNullException"><paramref name="text"/> is null.</example> /// <returns>The number of whitespace characters</returns> public static int CountWhiteSpace(string text) { if (string.IsNullOrEmpty(text)) throw new ArgumentNullException("text"); return text.Count(char.IsWhiteSpace); }
/************************使用代码契约方式之前*****************************/ /// <summary> /// 说明:只能在Debug模式下规范”契约“。 /// </summary> /// <param name="text"></param> /// <returns></returns> public static int CountStringLength(string text) { // 命名空间：using System.Diagnostics; Debug.Assert(text != null); return text.Length; }
1.2 代码契约
• C#代码契约起源于微软开发的一门研究语言Spec#（参见http://mng.bz/4147）。
• 契约工具：包括：ccrewrite（二进制重写器，基于项目的设置确保契约得以贯彻执行）、ccrefgen（它生成契约引用集，为客户端提供契约信息）、cccheck（静态检查器，确保代码能在编译时满足要求，而不是仅仅
检查在执行时实际会发生什么）、ccdocgen（它可以为代码中指定的契约生成xml文档）。
• 契约种类：前置条件、后置条件、固定条件、断言和假设、旧式契约。
• 代码契约工具下载及安装：下载地址Http://mng.bz/cn2k。（代码契约工具并不包含在Visual Studio 2010中，但是其核心类型位于mscorlib内。）
• 命名空间：System.Diagnostics.Contracts.Contract
• 代码契约优势：编译前执行检查（如若设置异常类型使用EnsuresOnThrow<Exception>则会在编译时抛出异常），这样比较编译后检查有明显的优势。
1.3 契约种类介绍
• 前置条件（precondition）：是对方法调用者提出的要求，而不是表示普通条件下方法本身的行为。Contract.Requires<T>();
1 /// <summary> 2 /// 实现“前置条件”的代码契约 3 /// </summary> 4 /// <param name="text">Input</param> 5 /// <returns>Output</returns> 6 public static int CountWhiteSpace(string text) 7 { 8 // 命名空间：using System.Diagnostics.Contracts; 9 Contract.Requires<ArgumentNullException>(text != null, "Paramter:text");// 使用了泛型形式的Requires 10 return text.Count(char.IsWhiteSpace); 11 }
• 后置条件(postcondition)：表示对方法输出的约束：返回值、out或ref参数的值，以及任何被改变的状态。Ensures();
/// <summary> /// 实现“前置条件”的代码契约 /// </summary> /// <param name="text">Input</param> /// <returns>Output</returns> public static int CountWhiteSpace(string text) { // 命名空间：using System.Diagnostics.Contracts; Contract.Requires<ArgumentNullException>(!string.IsNullOrEmpty(text), "text"); // 使用了泛型形式的Requires Contract.Ensures(Contract.Result<int>() > 0); // 1.方法在return之前，所有的契约都要在真正执行方法之前（Assert和Assume除外，下面会介绍）。 // 2.实际上Result<int>()仅仅是编译器知道的”占位符“：在使用的时候工具知道它代表了”我们将得到那个返回值“。 return text.Count(char.IsWhiteSpace); } public static bool TryParsePreserveValue(string text, ref int value) { Contract.Ensures(Contract.Result<bool>() || Contract.OldValue(value) == Contract.ValueAtReturn(out value)); // 此结果表达式是无法证明真伪的。 return int.TryParse(text, out value); // 所以此处在编译前就会提示错误信息：Code Contract：ensures unproven: XXXXX }
• 固定条件（invariant）：它们是只要对象的状态可见，就必须自始至终遵循的契约。换句话说，在类的公共方法运行时，固定条件可以改变，但在方法的最后，它们仍要满足契约。
1 public sealed class CardGame 2 { 3 readonly Stack<Card> deck = new Stack<Card>(Card.CreateFullDeck()); 4 readonly Stack<Card> discardPile = new Stack<Card>(); 5 readonly List<Player> players = new List<Player>(); 6 7 public void DealCard(Player p) 8 { 9 players.Add(p); 10 } 11 12 [ContractInvariantMethod] 13 private void ObjectInvarint() 14 { 15 Contract.Invariant((deck.Count + discardPile.Count + players.Sum(p => p.CardCount)) == Card.FullDeckSize); // 校验总和是否一致。 16 } 17 }
特性：1. 固定条件方法是无参数、无返回值、私有的。
2. 用[ContractInvariantMethod]标签修饰。
3. 执行起来代价低廉，不必担心性能损失。
4. 如果检查集合内容还可用Contract.ForAll or Contarct.Exists.
[ContractInvariantMethod] private void InvarintCollection() { Contract.Invariant(Contract.ForAll(players, item => item.Name != "Stephen")); // 校验集合。 Contract.Invariant(!Contract.Exists(players, item => item.Name != "Stephen")); // 与上句作用相同。 }
• 断言和假设 ：可检测在代码进行到“一半”时发生的事情。
断言Assert：静态检查器会检测Assert是否正确，而Assume不会。大多数情况下使用。
假设Assume：正因为静态检查器不会检查，所以某些情况下需要过滤掉静态检查器无法检验的东西。
public static int RollDic(Random rng) { Contract.Ensures(Contract.Result<int>() >= 2); if (rng == null) rng = new Random(); Contract.Assert(rng != null); int firstRoll = rng.Next(1, 7); Contract.Assume(firstRoll >= 1); Contract.Assume(firstRoll <= 6); return firstRoll; }
• 旧式契约：本质上是另一种形式的前置条件。DoNet2.0支持。
public static int CountSpace(string text) { if (text == null) throw new ArgumentNullException("text"); Contract.EndContractBlock(); // 此方法不做任何事情，只是让二进制编译器知道，此句以上的部分是契约。 return text.Count(char.IsWhiteSpace); }
二， 使用ccrewrite和ccrefge重写二进制
2.1 契约重写：重写刚刚获取的程序集的某些部分，以替换原始的程序集。
替换的事件序列：
• 检查前置条件。
• 为OldValue方法调用获取初始的状态。
• 执行代码的功能部分，如Assert
• 检查后置条件
• 检查固定条件
2.2 契约继承（重要）
• 特性：1. 覆盖某方法（或实现某个接口方法，规范契约）会继承该方法中的契约。
2. 不能再继承的方法中添加额外的前置条件，但却可以添加固定条件和后置条件。必须符合Liskov替换原则（里氏代换原则http://zh.wikipedia.org/wiki/Liskov%E4%BB%A3%E6%8F%9B%E5%8E%9F%E5%89%87）。
• 继承：使其子类也有父类中的前置条件、后置条件等，作为一种条件约束，但也有其限制，而且继承很容易被滥用，不如实现接口方式稳妥。
[Pure] public static bool Report(string text) { Console.WriteLine(text); return true; } public class ContractBase { public virtual void VirtualMethod(string text) { Contract.Requires(Report("Base precondition")); Contract.Ensures(Report("Base postcondition")); } } public class Derived : ContractBase { public override void VirtualMethod(string text) { Contract.Ensures(Report("Dervied postcondition")); } } /* ******************************************************* * 结果： * Base precondition * Dervied postcondition * Base postconditon * * 注：尽管Dervied中覆写的方法没有调用base.VirtualMethod(), * 契约仍然被执行。 * *******************************************************/
• 为接口指定契约：
1 /************************************************************* 2 * 说明： 3 * 1. ICaseConverter与ICaseConverterContracts互为实现（相互反向 4 * 引用）。 5 * 2. ICaseConverter只定义接口方法。 6 * 3. ICaseConverterContracts抽象类中实现接口的约束，内部要定义成 7 * 私有。 8 * 4. CurrentCultrueUpperCaseFormatter实现接口ICaseConverter，而 9 * 与抽象类隔离。 10 * ***********************************************************/ 11 /// <summary> 12 /// 接口类 13 /// </summary> 14 [ContractClass(typeof(ICaseConverterContracts))] // 指定契约类 15 public interface ICaseConverter 16 { 17 string Convert(string text); 18 } 19 20 /// <summary> 21 /// 契约类 22 /// </summary> 23 [ContractClassFor(typeof(ICaseConverter))] // 声明契约所服务的类型 24 internal abstract class ICaseConverterContracts : ICaseConverter 25 { 26 public string Convert(string text) 27 { 28 Contract.Requires(!string.IsNullOrEmpty(text)); // 前置条件 29 Contract.Ensures(Contract.Result<string>() != null); // 后置条件 30 return default(string);// 如果没有实现此类，则返回默认值。 31 } 32 33 private ICaseConverterContracts() { } // 禁止实例化该类 34 } 35 36 /// <summary> 37 /// 实现类 38 /// </summary> 39 public class CurrentCultrueUpperCaseFormatter : ICaseConverter // 继承接口中的契约 40 { 41 public string Convert(string text) 42 { 43 return text.ToUpper(CultureInfo.CurrentCulture); // 实现接口方法。（由二进制重写器执行检查） 44 } 45 }
• 失败行为
Contract全局失败事件：Contract.ContractFailed ，可注册并捕获所有Contract失败事件
Contract.ContractFailed += new EventHandler<ContractFailedEventArgs>(Contract_ContractFailed); ... static void Contract_ContractFailed(object sender, ContractFailedEventArgs e) { Console.WriteLine("{0}:{1},{2}", e.FailureKind, e.Condition, e.Message); e.SetHandled(); }
三， 静态检查
• 意义：在编译时执行检查，任何错误将在Error List中显示警告信息和错误信息。
static string DontPassMeNull(string input) { Contract.Requires(input != null); Contract.Ensures(Contract.Result<string>() != null); return input; } static string MightReturnNull() { return "Not null really"; } /// <summary> /// Error list中显示警告信息 /// </summary> public static void DoTest() { DontPassMeNull("definitely okay"); // 总能通过 DontPassMeNull(MightReturnNull()); // CodeContracts:requires unproven:input != null 无法证明 DontPassMeNull(null); // 提示错误信息 }
• 静态检查选项：在属性页中选择Implicit Non-null Obligations选项可执行前置空引用的检查，Implicit Array Bounds Obligations选项可检查数组是否越界。
• 有选择性的执行检查
1. BaseLine（基线）方法：
在属性页中，选中：
则，在程序跟目录会生成baseline.xml文件，包含所有警告信息。
将错误导出到文件中有利于分析错误。
2. 特性控制检查：
[assembly: ContractVerification(false)]
[ContractVerification(false)]
四，后记（契约实战）
4.1 契约是一种稳固的保障：它不仅意味着在满足前置条件时，代码将以特定的方式运行，还意味着在不满足的时候，就不会继续执行。
4.2 不要考虑为不易变类型设置固定条件。如果某些情况不会改变类型的状态，那它也肯定不会破坏固定条件。相反，如果在构造时有必须遵循的规则，那么也应该是前置条件。
更多关于“代码契约”内容请阅读《C# in Depth》