去年我们已经开始在讨论Spec#这是一个基于C#的支持通过契约来进行设计的语言以契约来设计是构建于诸如静态类型化这样的概念之上的特定的动作只有在编译时被验证之后才能执行契约通常使用前置和后置条件的形式来表示比如一个参数或返回值永远不能为空或者只能包含某个特定范围的值
为了不让开发人员学习整个诸如Spec#这样的新语言微软正在构建一个独立于语言的函数库可以被任何NET语言所利用在某些方面契约 看上去类似断言不过它们本质上存在非常大的区别契约通过静态代码分析的组合来实现它能被用于编译器内部和外部以及测试框架之中它们也能被执行 这意味着它们在运行调试版本的时候和断言很类似让我们来看第一个例子
string GetDescription(int x){
ContractRequires(x>);
ContractEnsures(ContractResult() != null);
如果只看签名开发人员只能获得静态类型的信息GetDescription要求输入一个整数并返回一个字符串而通过附加契约开发人员和工具都可以知道GetDescription要求输入一个正整数并返回一个不能为空的字符串
除了显式的契约之外契约检查器也支持隐式的契约一个例子就是被零除这样的情况如果一个类包含一个整数除法其中的除数是一个变量那么所 有的代码路径都必须保证这个变量不会为零或者会引发一个警告如果在这种情况中的变量是一个开放类的属性那么它也会要求检查每个子类对于非关联化空值 和数组索引也存在一些隐式契约
为了让契约设计更容易还存在一个ObjectInvariant方法的概念这个特别的方法只包含契约可以被注入到每个方法调用的末尾以保证对象的状态保持一致要着重注意的是这个东西要应用到所有方法之中包括那些来自于其他程序集的子类
