规范合同和规范#之间的差异

这来自Microsoft Research的代码合同常见问题解答：

代码合约与规范#有任何关系吗

代码合约是Spec#项目的衍生产品。Spec#的研究重点是在存在的情况下理解对象不变量的含义继承、回调、别名和多线程。规范#是C#v2.0的超集，并使用源代码级重写器来编织合同纳入代码。它使用验证条件生成和Spec#代码静态验证的定理证明器。但是妥善处理维护对象的所有复杂问题不变量是有代价的：验证变得不平凡。这就是为什么Spec#还需要一个所有权规则来了解哪些对象可能别名或不能互相别名。

代码契约是从Spec#学习什么是有效的和什么没有。与Spec#不同，代码契约是语言无关的，并且因此可以跨所有.NET语言工作，从VB到C#再到F#。重写器工作在MSIL上，因此不依赖于特定的编译器。它的静态分析引擎使用抽象解释比核查更快、更可预测；进一步抽象解释推断循环不变量和方法契约有助于代码合同的采用和易用性。

因此，代码契约似乎将是未来更受"支持"的工具。