如同一个类的实现列举了该类的实际（具体）属性一样，一个类的规格说明列举了它的“规格说明属性”。（规格说明属性通常称为“抽象属性”，但是在Java中抽象还有其它的意思，因此我们将尽量避免使用这个术语。）规格说明通常只引用规格说明属性，而从不引用具体属性。具体属性依赖于各个特殊的实现，因此我们不想将它引入到一个能够以多种方法实现的规格说明中去。

按照习惯，在规格说明属性中，如“sequence”这样的小写类型指向一个精确的实体。象“float”这种简单的Java类型也以小写形式给出。大写类型通常指向Java中的类。

一个规格说明属性的存在对于一个类的接口或实现并不意味着什么。接口可能并不提供查询规格说明域的方法，因此该类的客户端可能并不访问存储在规格说明属性中的信息。同样的，这个类的实现中可能不会包含一个规格说明属性类型所对于的具体属性，而那个信息可能由多个具体属性共同运算得到，或者它根本就不可用。而问题的关键是规格说明属性的使用对于规格说明是有益的。

方法的规格说明

方法的规格说明根据方法的前置条件和后置条件描述一个过程的行为。注意方法的规格说明也只能引用规格说明属性、方法的参数以及全局变量，而不能引用方法实现的具体属性。

前置条件

前置条件是在方法调用时必须为真的一组属性。方法的调用者应该负责对前置条件的检查。如果不对该条件进行检查，方法就可能会表现出任何行为，包括导致程序崩溃、返回错误的结果、将问题告诉用户或者从问题中恢复。调用者应该总是假设要调用的方法并没有进行前置条件检查。但是使用一个方法检查它的前置条件（如果检查能够有效的执行），并在不满足条件的时候抛出一个错误将是一个很好的练习。（在6.170课程中，你对不满足前置条件情况的处理并不会影响你的得分。）

一个方法的规格说明中的“需求”条款指出了它应该满足怎样的前置条件。如果规格说明中遗漏了“需求”条款，那么将假设这个方法没有任何前置条件。

后置条件

后置条件是由方法退出时负责检查的，必须为真的一组属性。如果在方法调用的时候没有进行前置条件检查，那么这个方法将可能表现出任何行为。特别的，如果在方法进入时没有进行前置条件检查，那么在方法退出时就一定要进行后置条件检查。

一个后置条件可以使用一个单独的逻辑表达式来描述，但是我们建议将它们分解为逻辑上相互区别的多个部分。Liskov的文章使用“效果”和“改变”，而6.170课程使用“返回”、“效果”、“抛出”和“改变”。（下面的描述中，“缺省”指假设方法规格说明中遗漏了后置条件项的情况。）

返回（缺省：对返回值没有限制）

方法的返回值，如果有的话。

效果（缺省：真，表明“可以产生任何效果”）

方法执行所产生的副作用，比如对于当前对象或者作为参数传递的对象的状态的改变。

抛出（缺省：无，说明并不抛出任何异常）

可能会抛出的异常，以及异常抛出的条件。

改变（缺省：无，说明方法的执行没有副作用）

程序执行中可能改变的值。除非在效果项中指出，它们并不一定会被修改。例如，假设一个规格说明属性被列在改变项中而没有被列在效果项中，那么它就可以接受任何为该类抽象不变式所允许的对象值。

如果x对象有f、g和h三个规格说明属性，那么“改变x”意味着x.f、x.g、x.h的任意组合都可能被修改，而“改变 x.g, x.h”则是更严格的限制。

通常，程序员对于没有列在改变项中的数值更感兴趣，因为它们的值是不能被方法改变的。

按照惯例，方法规格说明的Javadoc标记按照以下顺序出现：需求、改变、抛出、效果、返回。

返回顶部