微软新语言 Spec#终结 Null 引用异常

微软发布了 Spec# 1.0 版本。Spec#是 C#的一个扩展，支持许多契约（contract）属性，如非 Null 类型系统，前置和后置条件，循环常量（loop invariant）和对象常量等。

Null 引用异常（reference exceptions）也许是 C#、Java 和 VB 程序中最普通不过的异常了。为了消除这种错误，Spec#支持一个非 Null 类型系统。在这个系统里，编译器确保用“!”符号标记的变量永不为 Null，比如“Customer! _customer ”。为了便于使用，它允许成员变量在基类构造器（constructors）前就可以被初始化。

非 Null 类型系统还可以扩展到参数、本地变量和返回值。一个例外是数组中的值，因为可能会因数组初始化和 C#的协变数组（covariant array）而导致错误。

前置条件指定对象或者在方法调用前被传递的参数等所需要的状态。比如，开发人员可以通过“requires”语句要求某个集合（collection）为不是只读的，或者要求在 Insert 方法调用前要用到的索引是有效的。不像现在在 C#里面被用到的运行时异常（runtime exception），Spec#希望在编译时就能够设置这些条件。“otherwise”语句可以被用来表示哪些异常会被抛出，如果前置条件不能被静态检查和事后违背的话。

指定了 ensures clause 的后置条件会确保类的常量不被中断，返回的值也在一个可接受的范围。它会先于被调用的方法前存取对象值，所以开发人员也能确保类似数值变量可以一直以 1 为单位增长这样的事情。而且，还被编译器静态地保证。

类似于 Java，Spec#也使用了可检查异常。主要的区别是，在一个发生异常的事件中也许仍可以设置后置条件。这种情况下，开发人员会将 ensures clause 置于 throws clause 之上，以确保所做的修改已经正确回滚。

其中没有提到的地方是 Spec#是如何通过可检查异常（checked exception）处理版本标定（versioning）和继承（inheritance）。在 Java 中，如果说可能会跳出一个基类中没有定义的异常，那么一般很难去通过增加功能性或者子类来扩展类。

那些常量很像后置条件（post-condition），但是它们应用到类中所有的方法上。指定了“常量”声明，它们就可以保证在每个方法调用的最后，对象处在一个稳定的条件下。

Spec#严重依赖上面提到的契约类型。但是因为它们不是基础类库（Base Class Library）的一部分，所以 Spec#允许预编译库的契约在一个编译时引用到的分离仓库（repository）中被指定。

查阅英文原文： Spec# Puts an End to Null Reference Exceptions

编辑注：感谢孟岩、岳立东对本文部分专业术语的审校。