微软发布了 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)中被指定。
评论