副作用

　　回忆一下清单 2 中 pop() 的后置条件：

　　这指出 pop() 具有从 elementsInQueue 除去元素的副作用。但是，它并未指出没有其它副作用。例如， pop() 的实现可以修改 m_isMinHeap ，以便将最小堆变成最大堆。只要这样的修改也返回正确值，那它就不会引起运行时断言失败，但是它会使整个 JML 规范变得脆弱。

　　我们可以加强后置条件，以禁止除了修改 elementsInQueue 之外的任何副作用存在，如清单 7 所示：

　　清单 7. 副作用的后置条件

　　通过添加 x == \old(x) 格式的后置条件堵住了漏洞。就其缺点而言，该方法最终会导致规范出现混乱，这是因为每个方法必须在后置条件中为不由该方法改变的每个字段添加子句。它还使维护变得更加困难，因为如果我们将新字段添加到类中，我们将不得不修改所有方法的后置条件，以便指出它们不会修改这一新字段。

　　JML 提供了一种更好的办法来指出方法的副作用：就是用 assignable 子句。

　　assignable 子句

　　assignable 子句允许我们编写如清单 8 所示的 pop() 规范：

　　清单 8. 用于方法规范的 assignable 子句

　　只有 assignable 子句中所列出的字段才能被方法修改(其它条件在下面有讨论)。 pop() 的 assignable 子句指出 pop() 可以修改 elementsInQueue ，但是它不能修改其它字段，比如 isMinimumHeap 或 comparator 。如果 pop() 的实现修改了 m_isMinHeap ，就会出错。(但是请注意，JML 编译器的当前版本不检查方法是否只修改了其 assignable 子句中的字段。)

　　修改位置

　　要说方法只可以修改 assignable 子句中所列出的字段，这显得简单了点。如果以下任一因素是 true，则实际规则允许方法修改一个位置( loc )：

　　assignable 子句中提到了 loc 。

　　assignable 子句中提到的位置依赖于 loc 。(例如，请考虑一下“ assignable isMinimumHeap; ”这种情况。模型字段 isMinimumHeap 依赖于具体字段 m_isMinHeap ，因此该 assignable 子句会允许方法修改 m_isMinHeap 以及 isMinimumHeap 。)

　　方法开始执行时没有分配 loc 。

　　loc 是方法的局部变量或者是方法的形式参数。

　　最后一种情况允许方法修改其参数，即使参数没有出现在 assignable 子句中。乍一看，这似乎是：如果变量作为参数传递给方法，则允许该方法修改其调用函数中的这一变量。例如，假设我们有个方法 foo(Bar obj) ，它包含语句 obj = anotherBar 。当该语句修改 obj 的值时，它并不影响 foo() 调用函数中的任何变量，这是因为 foo() 中 obj 与 foo() 调用函数中的变量截然不同，即使它们都引用同一 Bar 实例。

　　如果 foo(Bar obj) 包含了语句 obj.x = 17 ，则会如何?这会使变更对于调用函数是可见的。但是，其中有“陷阱”。 assignable 子句的规则允许方法为参数赋予一个新的值，而不必在 assignable 子句中提到该变量。但是这些规则不允许方法为参数的字段(比如 obj.x )赋予一个新的值。如果 foo() 需要修改 obj.x ，那么它必须具有 assignable obj.x; 形式的 assignable 子句。

　　有两个 JML 关键字可以和 assignable 子句一起使用： \nothing 和 \everything 。我们可以通过编写 assignable \nothing 表明方法不会有任何副作用。类似地，我们也可以通过编写 assignable \everything 表明允许方法修改任何内容。在前面的 peek() 方法上下文中所描述的 pure 关键字等同于 assignable \nothing; 。

　　异常行为

　　先前给出的 peek() 和 pop() 的规范要求在调用每个方法时队列非空。但是实际上可以在队列为空时调用 peek() 和 pop() 。在这种情况下，每种方法都会抛出 NoSuchElementException 。我们需要修改规范以允许这种可能性的存在，为此我们将使用 JML 的 exceptional_behavior 子句。

　　到目前为止我们的规范一直以 public normal_behavior 开始。 normal_behavior 关键字表明这些规范是针对方法不抛出任何异常时的情况。 public exceptional_behavior 注释可以用来描述抛出异常时的行为。清单 9 显示了用于 peek() 的 PriorityQueue 规范中的 exceptional_behavior ：

　　清单 9. exceptional_behavior 注释

　　和我们到目前所见到的其它每个示例一样，该规范的第一部分是以 public normal_behavior 开头的。以 public exceptional_behavior 开头的第二部分描述了异常行为。就如同 normal_behavior 子句一样， exceptional_behavior 子句也有 requires 子句。 requires 子句表明要抛出 signals 子句中所列的异常而必须为 true 的条件。在上面这个示例中，如果 isEmpty() 为 true，那么 peek() 将抛出 NoSuchElementException 。

　　signals 子句

　　signals 子句的通用格式为 signals(E e) R; ，其中 E 为 Exception 或者是从 Exception 派生来的类， R 是表达式。JML 如下解释 signals 子句：如果抛出 E 类型的异常，则 JML 检查 R 是否为 true。如果为 true，那么该方法满足其规范。如果 R 为 false，则 JML 抛出一个未经检查的异常(unchecked exception)，表明违反了 exceptional_behavior 规范。

　　上面的 peek() 声明中的 signals 子句要求队列为空时抛出 NoSuchElementException 。如果 peek() 抛出任何其它异常(例如，属于未经检查的异常的 IllegalStateException )，则 JML 会把它作为错误来捕获，因为 e instanceof NoSuchElementException 将为 false。如果我们希望允许 peek() 返回 NoSuchElementException 或一个未经检查的异常，就要将 signals 子句修改成 signals (NoSuchElementException e) true; 。这意味着如果 peek() 抛出 NoSuchElementException ，那么 true 必须为 true，这始终成立。因为我们还没有说明有关其它异常的任何内容，因此 peek() 可能会抛出其说明所允许的任何异常。该说明指定 throws NoSuchElementException ，这意味着可以抛出 NoSuchElementException 或是未经检查的异常。

　　如果队列非空时调用 peek() 并且它抛出 NoSuchElementException (或任何其它异常)，则 JML 运行时断言检查器会产生一个未经检查的异常，表明正常行为后置条件没有得到满足。

　　结束语

　　在本文中我介绍了 JML，说明了它对面向对象分析和设计过程的帮助，并为您举例说明了如何在 Java 程序中使用 JML 注释。您可以从下载本文所使用的完整源代码，还可以在那里找到有助您进一步学习 JML 的参考资料。

　　您可以使用开放源码 JML 编译器来生成类文件，这些文件可以在运行时自动检查 JML 规范。如果程序没有完成其 JML 注释中规定要做的事，则 JML 会抛出一个未经检查的异常，指出违反了哪部分规范。这在捕获错误或帮助使文档(JML 注释格式)与代码保持同步方面都非常有用。

　　JML 运行时断言检查编译器是数目不断增多的使用 JML 的工具中的第一个。其它工具包括 jmldoc 和 jmlunit 。 jmldoc 类似于 javadoc ，不过它还在生成的 HTML 文档中包含了 JML 规范。 jmlunit 生成测试案例类的框架，它使 JML 能方便地与 JUnit 结合使用。

        代码下载