0 导论
【1】
软件工程意味着构建正确且可维护的软件。对软件正确性的验证技术在60年代末已有深厚的基础（以
Floyd [25] 与 Hoare [33] 最为显著）。接下来的十多年内，各种以自动化辅助验证程序正确性的系统已得以开发（例如[37, 27, 51]）。想要改进软件工程师的生产过程，最重要的即是改良软件工程师的首要思维与劳动工具：编程语言。当然，大量的编程语言的设计都格外的考虑了正确性，通过约束和检验得以保证，像早期的语言 Gypsy [1] 和 Euclid [38]。另一些语言，将嵌入的约束转换为运行时的检验，从而在每次程序运行时动态的检验其正确性。此类最著名的为 Eiffel [54]。
尽管有了理想化的基础，也有过技术竞争中的无数胜例，但目前的软件开发实践仍然成本高昂且易于出错。语言规范的最普遍形式仍是非正式的自然语言式文档与标准化库的接口描述（与本文相关的实例，即.NET Framework，参见例[61]）。
然而，大量程序员自定的前提并未被详细说明，为程序的维护带来了不便，因为这些隐含的前提很容易破坏。此外，通常并不存在一种切实的方法来证实程序确实在
程序员设想的前提下运行、且没有被程序员意外忽视的前提。我们认为，如果更多的此类前提能够得到记录和强制化，程序开发就能得以进步。实际上，在编写此类
规范变得容易，并且产生短期就能感受到的效益之前，此种改变仍是不切实际的。
Spec＃编程体系是以一种更高效的方式开发与维护高质量软件的新尝试。一种编程体系要得以广泛的应用，必须能提供完善的基础结构，包括基础库、工具、设计支持、完整的编辑能力，还有最重要的一点，即面向大多数程序员的易用性。因此，我们的途径是将其整合进.NET Framework这个现成的业界基础平台中。Spec＃编程体系基于Spec＃编程语言，它是现有的面向对象.NET编程语言C＃的扩展。它对C＃的扩展包括预处理与后处理之类约束的理念、不可空类型、更高程度数据抽象的易用性等。此外，每次对C＃编程理念的强化事实上都在证实着Spec＃编程的方法论。与现有.NET代码和库的互操作能力将得以支持，但仅当源代码来自于Spec＃时，代码的可靠性才能得到保证。同时，这种约束也将成为可执行程序的一部分，并在运行中被动态的检查。Spec＃编程体系不仅仅包括语言和编译器，还包括名为Boogie的自动程序检验器，用作静态的约束检查。Spec＃体系将完全集成到微软Visual
Studio环境中。
Spec＃编程体系主要的影响在于：
－仅是对一种目前流行的语言的小规模扩展；
－是一种可靠性编程的方法论，提供了约束，提供了包括甚至涉及到回调时仍然有效的对象恒量验证；
－提供实现其方法论的工具，包括从易于使用的动态检查，到高可靠性的自动化静态验证；
－实现平稳的学习曲线，凭此程序员可以渐进的着手利用约束的优点。
本文是对Spec＃编程体系、该体系的设计以及其设计的理论基础的概论。该系统目前正在开发之中。
1、语言
Spec＃语言是C＃语言的超集，是面向.NET平台的面向对象语言。C＃与本文相关的特性包括类的单一继承与多重接口实现、对象引用、动态调用的方法以及异常处理。Spec＃对C＃的扩展包括对区分不可空对象引用与可空对象引用的类型支持、预处理与后处理等方法约束、异常处理的规范、以及对对象数据字段约束的支持。本节将说明这些特性并解释其设计。
1.0、不可空类型
目前程序中的许多错误被证明是空引用错误，这表明，我们急需一种编程语言具有能够辨别表达式是否可能得出空值的能力（实验证明见例[24,22]）。事实上，我们很希望根除这种空引用错误。
我们决定把可空性辨别的类型支持加入到Spec＃，因为我们认为，对于程序员来说，类型能提供最方便的途径来利用可空性辨别。为保证对C＃的向后兼容性，C＃引用对象T在Spec＃中用于表示可空类型，而相应的不可空类型则需引入新的符号，在Spec＃中选择了T!符号。
不可空类型系统主要的困难在于在未完成构造的对象中访问不可空变量。如下例所示：
class Student : Person { Transcript! t ;
public Student (string name,
EnrollmentInfo! ei)
: base(name) { t = new Transcript(ei);
}
由于成员变量t被声明为不可空类型，故构造函数必须赋予t一个非空的值。然而，在此例中需要注意，对t的赋值发生在调用基类的构造函数之后（在C＃中这是必然的）。在该调用期内，t的值仍为null。然而该成员变量已经可访问（例如基类的构造函数中的动态方法调用）。这违背了不可空类型系统的类型安全保证。
在Spec＃中，该问题通过语法得以解决，即允许构造函数在被构造的对象可访问之前初始化成员变量。上面的例子可更正为：
class Student : Person { Transcript! t ;
public Student (string name,
EnrollmentInfo! ei)
: t (new Transcript(ei)),
base(name) {
}
Spec＃借用了C＋＋的成员变量初始化语法。但Spec＃有别于C＋＋的重要的一点是，成员变量初始值将在基类构造函数被调用前取得。注意，这样的初始化表达式可以利用构造函数的参数，对于任何不可空类型的设计来说，这都被认为是重要且实用的特性。Spec＃要求初始化所有的不可空成员变量。
Spec＃中的不可空类型仅用于约束成员变量、本地变量、形式参数和返回值不为空值。数组元素类型规定不能为不可空类型，以避免数组元素初始化的问题和C＃的共变数组的问题。
为了让不可空类型的使用更符合C＃程序员的胃口，Spec＃规定了对本地变量的不可空性的表示符。Spec＃编译器以数据流分析的方式来执行其推导。
决定使用此简单不可空类型系统的原因有三。
第一，空引用的问题是面向对象编程中共有的，提供该问题的解决方案应该对大多数程序员都有相当的吸引力；第二，此简单解决方案适用于多数有用的不可空引用
编程模式；第三，对于超出了不可空类型系统可表述的情形，程序员可用如下所述的方法与类约定。
1.1、方法约定
所有的方法（包含C＃
中的构造函数、属性与索引器）都可以通过约束来描述其用途，即描述其调用者与其实现之间的约定。作为该约束的一部分，预处理约束描述的是方法能被调用的条
件，为调用者的责任。后处理约束描述的是方法返回的条件。“抛出集”和与其相关的“异常后处理”限制了方法可能抛出哪些异常，及描述了其中每个异常的产生
条件。最后，“框架条件”限制了方法中允许更改的哪些部分的程序状态。后处理约束、抛出集、以及框架条件则是方法实现的责任。方法约定确定了一种责任，即
在违背约定的错误发生时能够对过失进行界定的责任。
在现代编程语言中，统一错误处理一般由异常机制提供。由于在C＃和.NET框架中的异常机制缺乏确切的限制，Spec＃对在更多的规则下使用异常提供了支持，使程序更易懂、更容易维护。在阐释方法约定之前，我们先从Spec＃的角度来说明异常。
异常
Spec＃根据异常发出的条件来区分异常。【Goodenough[28]】
将异常看成特定方法的附属物，并将异常划分为两种错误，被称为调用者错误与供应者错误。调用者错误发生在某个方法在非法条件下被调用时，即该方法的预处理
约束未被满足。我们进一步将供应者错误表述为可容性错误或观测性程序错误。可容性错误发生在方法未能完成其预期的操作时，可能是操作完全未进行（如收到的
网络数据包的奇偶校检错误），也可能是做出了一定的努力之后（如等待网络套接字的输入经过了很长的时间）。可容性错误之集是调用者与实现之间的约束的一部
分。观测性程序错误或者是程序固有的错误（如数组越界错误），或者是和特定的方法无关的错误（如内存溢出错误）。
在这些种类的异常之中，必须重点的考虑是否
需要程序去捕获异常。可容性错误是程序预期行为的组成部分，所以需要让程序来捕获并处理可容性错误。相反，程序难以对调用者错误或观测性错误进行表示，甚
至程序不可能确定如何来应对此类错误。如果要程序来处理此种错误，则只能在应用程序或线程的最外层进行处理。
由于有这样的考虑，Spec＃借鉴了Java[29]，让程序员以“checked”与“unchecked”来声明异常类。可容性错误声明为“checked”的异常，而调用者错误与观测性程序错误声明为“unchecked”的异常。
【Fig.0】
ArrayList.Insert 方法
将元素插入
ArrayList 的指定索引处。
public virtual void Insert(
int index,
object value
);
参数
index
从零开始的索引，应在该位置插入 value。
value
要插入的 Object。该值可以为空引用
异常
异常类型 条件
ArgumentOutOfRangeException index 小于零。
- 或 -
index 大于 Count。
NotSupportedException ArrayList 为只读。
- 或 -
ArrayList 具有固定大小。
【Fig.0】
在Spec＃中，实现了ICheckedException接口的异常类都被看着是checked的异常。关于Spec＃中异常设计更多的信息请参考有关异常安全[48]的其它文件。
预处理条件
程序员的假定前提中最重要的可能就是预处理条件。下面是包含预处理条件的方法的一个简单的例子：
class ArrayList {
public virtual void Insert(int index ,
object value)
requires 0 <= index && index
<= Count;
requires !IsReadOnly &&
!IsFixedSize;
{ . . . }
预处理条件限定了在数组中，对象将要插入的索引号必须在数组边界之内，且数组允许增长。为遵守预处理条件，Spec＃编译器执行运行时检查。如果预处理条件不被满足，则抛出RequiresViolationException表示调用者错误。如果用户在调用现场使用Boogie，则Boogie会尝试静态验证预处理条件是否能在调用现场得以保持，如不能则给出错误报告。
有关此方法的.NET框架文档参见图0。在Insert的.NET文档与对Insert的约束之间有一点细微的差别。两种规范都指明了对调用者的预期，而其差别在于对预处理条件的违反引发的行为。为支持.NET框架规范的这种典型的健壮编程风格，Spec＃的预处理条件引入了“otherwise”子句。otherwise子句可用于指定编译器在运行时检测到对预处理条件的违背时，使用特定的异常代替缺省的RequiresViolationException异常。
class ArrayList { void Insert(int index ,
object value)
requires 0 <= index && index
<= Count
otherwise ArgumentOutOfRangeException;
requires !IsReadOnly &&
!IsFixedSize
otherwise NotSupportedException;
{ . . . }
由于otherwise子句中使用的异常表示的是调用者错误，故必须为unchecked异常。
后处理条件
方法约束也可包含后处理条件。例如，Insert的后处理条件可以如下规定：
ensures Count == old(Count) + 1;
ensures value == this[index ];
ensures Forall{int i in 0 : index ;
old(this[i]) == this[i]};
ensures Forall{int i in index : old(Count);
old(this[i]) == this[i + 1]};
以上的后处理条件描述了Insert的作用：使Count增加1，传入的value被插入到指定的索引位置，且保持其他的元素的相对位置。本例还显示出Spec＃约束的另一些特征：第一行中的old(Count)表示方法执行前Count的值；第三行的Forall函数作用于包含布尔表达式old(this[i]) == this[i]的大括号，其中i的取值为从0到index的半开空间内的整数值。大括号和量词作为语法上的限制，保证编译器能够生成可运算代码。
Boogie尝试验证Insert的每个实现是否满足后处理条件。若验证成功，则无需进行运行时检验了（该检验抛出EnsuresViolationException），因为运行时检验不会失败。
在运行时检验中，我们引入了Eiffel机制来计算old(E)。当方法被调用前，执行出现在后处理条件的所有old(E)中的表达式E的计算，并保存其结果。然后，当且仅当old(E)的值被计算后处理条件所需时，使用该保存的E的值。注意，当后处理条件的计算中出现短路布尔表达式或者方法运行未正常结束时，old(E)的值实际上有可能不需要用到。
以上的实例还阐明了关于动态和静态检验约定之间区别的一个更一般性的观点。Boogie需要知晓程序和其内在的数据结构，并且有对量词的支持，以便静态的检查Insert的后处理条件。然而，使用了过程化抽象的约定对于静态模块化检验可能会产生问题，因为此类检验只可访问程序中有限的部分。同样的，使用了更高层数据结构的约束对于静态检验也可能会产生问题，因为……
下接第7页