【IT168 技术文章】面向对象分析和设计的原则之一就是应当尽可能地把过程设想往后推。我们大多数人只在实现方法之前遵守这一规则。一旦确定了类及其接口并该开始实现方法时，我们就转向了过程设想。那么到底有没有别的选择?和大多数语言一样，编写 Java 代码时，我们需要为计算每个方法的结果一步一步地提供过程。

　　就其本身而言，过程化表示法只是说 如何做某事，却不曾说过我们正在设法做 什么。在动手之前了解我们想要取得的结果，这可能会有用，但是 Java 语言没有提供显式地将这种信息合并到代码中的方法。

　　Java 建模语言(JML)将注释添加到 Java 代码中，这样我们就可以确定方法所执行的内容，而不必说明它们如何做到这一点。有了 JML，我们就可以描述方法预期的功能，无需考虑实现。通过这种方法，JML 将延迟过程设想的面向对象原则扩展到了方法设计阶段。

　　JML 为说明性的描述行为引入了许多构造。这些构造包括模型字段、量词、断言的可见度范围、前提条件、后置条件、不变量、合同继承以及正常行为与异常行为的规范。这些构造使得 JML 的功能变得非常强大，但是没必要理解或使用所有这些构造，也没必要马上使用所有的构造。您可以从简单的起点开始逐步学习和使用 JML。

　　在本文中，我们将采取循序渐进的方法来学习 JML。我们将从概述使用 JML 的好处入手，重点讲述它对开发和编译过程的影响。接下来，我们将讨论用于前提条件、后置条件、模型字段、量化、副作用和异常行为的 JML 构造。在这个过程中，示例会显示每种 JML 构造的动机。在本文结尾处，您将对 JML 的工作原理有个概念性的理解，并能将它应用到您自己的程序中。

　　JML 概述

　　使用 JML 来说明性地描述所希望的类和方法的行为，可以显著地改善整个开发过程。将建模表示法添加到 Java 代码中，其好处包括以下几点：

　　能更加精确地描述代码所完成的任务

　　能有效地发现和纠正错误

　　能减少随着应用程序的进展而引入错误的机会

　　能较早地发现客户没有正确使用类

　　能产生始终与应用程序代码保持同步的精确文档

　　JML 注释始终位于 Java 注解(comment)内部，因此它们不会对进行正常编译的代码产生影响。当我们想将类的实际行为与其 JML 规范进行比较时，可以使用开放源码 JML 编译器。用 JML 编译器编译过的代码如果没有做到规范中规定它应该做的事，那么该代码在运行时会抛出 JML 异常。这不仅能捕获代码中的错误，还能确保文档(JML 注释格式)与代码保持同步。

　　在以下几节中,我将使用开放源码 Jakarta 公共集合组件(Jakarta Commons Collection Component，JCCC)的 PriorityQueue 接口和 BinaryHeap 类来说明 JML 的特性。

　　需求和职责

　　本文的源代码包括了 JCCC 的 PriorityQueue 接口。 PriorityQueue 接口包含了方法特征符，这些特征符指定了参数和返回值的数据类型，但是没有说明任何有关方法行为的内容。我们希望能指定 PriorityQueue 的语义，这样的话实现它的所有类就能以预期的方式运作(在没有行为规范的情况下，我们最终会得到一个实现了 PriorityQueue 接口的堆栈类，或者其它某种非常规的情况)。

　　请研究 PriorityQueue 中 pop() 方法。优先级队列对 pop() 有什么需求呢?有三个基本需求。首先，除非队列中至少有一个元素，否则不应该调用 pop() 。其次，它应当返回队列中优先级最高的元素。最后，它应当除去从队列中返回的元素。

　　清单 1 演示了表示第一个需求的 JML 注释：

　　清单 1. pop() 方法需求的 JML 注释

　　如前面所述，JML 注释是写在 Java 注解内部的。包含 JML 的多行注解是以字符 /*@ 开头的。JML 忽略行中所有作为第一个非空格字符的 @ 符号。JML 还可以写在以 //@ 开头的单行注解内部。

　　这里 JML 中 public 关键字的意义和在 Java 语言中的意义是一样的。 public 表示该 JML 规范对于应用程序中的其它所有类都是可见的。公共规范只能涉及公共方法和成员变量。JML 还允许规范拥有 private 、 protected 或 package 级别的作用域。JML 的作用域规则与 Java 语言中的相应规则类似。

　　normal_behavior 关键字表示该规范描述了 pop() 正常返回而没有抛出异常的情况。随后我们将讨论如何确定异常行为。

　　前提条件和后置条件

　　JML 关键字 requires 用于前提条件。 前提条件(precondition)指的是在调用方法之前必须要满足的条件。清单 1 指出 pop() 的前提条件是 isEmpty() 返回 false ;也就是说，队列中至少要包含一项。

　　方法的 后置条件(postcondition)指定该方法的职责;也就是说，当方法返回时，后置条件应当是 true。在我们的示例中， pop() 应当返回队列中拥有最高优先级的元素。我们希望指定该后置条件，这样 JML 就可以在运行时检查它。要做到这一点，我们需要清楚已经添加到优先级队列中的所有值，以便确定 pop() 应当返回哪一个值。我们可以考虑将一个成员变量添加到 PriorityQueue 以便在队列中存储这些值，但是这里有两个问题：

　　PriorityQueue 是一个接口，因此它应当与不同的实现(比如二进制堆、Fibonacci 堆或日历队列)兼容。 PriorityQueue 的 JML 注释不应当描述任何有关实现的内容。

　　作为接口， PriorityQueue 只能包含静态成员变量。

　　JML 用 模型字段的概念解决了这一两难局面。

　　模型字段

　　模型字段类似于只能在行为规范中使用的成员变量。下面有一个在 PriorityQueue 中使用的模型字段声明示例：

　　//@ public model instance JMLObjectBag elementsInQueue;

　　该声明指出有一个模型字段 elementsInQueue ，其数据类型为 JMLObjectBag (属于 JML 的 bag 数据类型)。 instance 关键字表示：即使该字段是在接口中进行声明的，也要在实现 PriorityQueue 的类的每个实例中分别放置该字段的非静态副本。和所有 JML 注释一样， elementsInQueue 的声明出现在 Java 注解中，因此 elementsInQueue 不能用于正规的 Java 代码中。没有哪个对象会在运行时包含 elementsInQueue 字段。

　　elementsInQueue 包含了添加到优先级队列的值。清单 2 显示了 pop() 的规范是如何利用 elementsInQueue 的：

　　清单 2. pop() 的后置条件中所使用的模型字段

　　ensures 关键字指出其后跟的是 pop() 返回时必须满足的后置条件。 \result 是 JML 关键字，它等于 pop() 所返回的值。 \old() 是 JML 函数，在调用 pop() 之前它返回其参数所具有的值。

　　ensures 子句包含两个后置条件。第一个指出将 pop() 所返回的值从 elementsInQueue 中除去。第二个指出返回值和 peek() 返回的值一样。

　　类级不变量

　　我们已经看到 JML 允许我们指定方法的前提条件和后置条件。它还允许我们指定类级不变量。类级不变量是这样的条件：即在类中每个方法的入口和出口处这些条件都必须为 true。例如， //@ public instance invariant elementsInQueue != null; 是 PriorityQueue 的不变量，这就是说，在实现 PriorityQueue 的类的构造函数返回之后， elementsInQueue 无论何时都不能是 null。

　　在 pop() 先前的规范中，我们说它的返回值等于 peek() 的返回值，但是我们不曾研究 peek() 的规范。 PriorityQueue 中 peek() 的规范如清单 3 所示：

　　清单 3. PriorityQueue 中 peek() 的规范

　　该 JML 注释指出应当在队列中至少有一个元素时才调用 peek() 。它还指出 peek() 返回的值必须位于 elementsInQueue 中;也就是说，这个值必须是先前插入到队列中的值。

　　/*@ pure @*/ 注解指出 peek() 是一个纯方法。 纯方法(pure method)就是没有副作用的方法。JML 只允许断言使用纯方法。我们将 peek() 声明为纯方法，这样就可以在 pop() 的后置条件中使用它。如果 JML 允许在断言中使用非纯方法，那么我们可能就会在无意之中编写出具有副作用的规范。这可能会导致代码在启用断言检查进行编译时可以正常运行，而在禁用断言检查时则无法运行。我们待会将进一步讨论副作用。

　　关于继承

　　JML 规范是由实现接口的子类和类继承的(不同于 J2SE 1.4 中的断言语句)。JML 关键字 also 指出规范是与从祖先类继承的规范和从实现的接口继承的规范合并在一起的。因此， PriorityQueue 接口中的 peek() 的规范也适用于 BinaryHeap 中的 peek() 。这意味着 BinaryHeap.peek() 返回的值必须位于 elementsInQueue 中，即使这没有在 BinaryHeap.peek() 规范中显式说明。

　　最小堆和最大堆

　　peek() 规范中显然遗漏了一件事。它从未指出返回值就是具有最高优先级的那个值。结果是 JCCC 中 PriorityQueue 接口既可以用于最小堆也可以用于最大堆。对于最小堆，具有最高优先级的元素是最小的元素，而对于最大堆，具有最高优先级的元素是最大的元素。这是因为 PriorityQueue 不知道它正在与最小堆还是最大堆一起使用，所以指出返回哪个元素的那部分规范必须放入实现 PriorityQueue 的类中。

　　在 JCCC 中， BinaryHeap 类实现 PriorityQueue 。 BinaryHeap 允许客户机通过构造函数中的一个参数来指定它应当用作最小堆还是最大堆。我们使用布尔模型变量 isMinimumHeap 来指出 BinaryHeap 是用作最小堆还是最大堆。 BinaryHeap 中 peek() 的规范使用了 isMinimumHeap ，如清单 4 所示：

　　清单 4. BinaryHeap 类中 peek() 的规范

　　添加量词

　　清单 4 中的后置条件包括了两个部分，一部分是最小堆的后置条件，另一部分是最大堆的后置条件。 ==> 符号表示“暗示”。 x ==> y 当(且仅当)y 为 true 或 x 为 false 时才为 true。对于最小堆，下列条件适用：

　　\forall 是 JML 量词。如果对于所有 Objects obj ， elementsInQueue.has(obj) 为 true 并且 compareObjects(\result, obj) 返回一个小于等于零的值，那么上面的 \forall 表达式为 true。换句话说，当 compareObjects() 用于比较值的大小时， peek() 返回的值小于等于 elementsInQueue 中的任何元素。其它的 JML 量词包括 \exists 、 \sum 和 \min 。

　　添加比较器

　　BinaryHeap 类允许用两种不同的方法对元素进行比较。一种方法是使用 Comparable 接口依靠元素的自然排序来进行。另一种方法是让客户机将 Comparator 对象传递给 BinaryHeap 构造函数。然后将使用 Comparator 来进行排序。我们使用模型字段 comparator 来表示 Comparator 对象(如果有的话)。 peek() 后置条件中的 compareObjects() 方法使用客户机所选中的任一比较方法。 compareObjects() 的定义如清单 5 所示：

　　清单 5. compareObjects() 方法

　　compareObjects 声明中的关键字 model 表明这是一个模型方法。 模型方法是只能在规范中使用的 JML 方法。它们是在 Java 注解中声明的，不能用在正规的 Java 实现代码中。

　　如果 BinaryHeap 的客户机要求使用特定的 Comparator ，那么 m_comparator 将引用该 Comparator ;否则它就为 null。 compareObjects() 检查 m_comparator 的值并使用适当的比较操作。

　　模型字段如何获取值

　　我们在清单 4 中显示了 peek() 的后置条件。后置条件验证返回值的优先级是否大于等于模型字段 elementsInQueue 中所有元素的优先级。这产生了一个问题：诸如 elementsInQueue 这样的模型字段如何获取它们的值?前提条件、后置条件和不变量都必须没有副作用，因此它们不能设置模型字段的值。

　　JML 使用 represents 子句来将模型字段和具体实现字段相关联。例如，下面的 represents 子句被用于模型字段 isMinimumHeap ：

　　该子句指出模型字段 isMinimumHeap 的值等于 m_isMinHeap 的值。 m_isMinHeap 是 BinaryHeap 类中的私有布尔成员字段。无论何时需要 isMinimumHeap 的值，JML 都将用 m_isMinHeap 的值来替换。

　　represents 子句在 <- 右边并不只限于成员字段。请研究下面这个 elementsInQueue 的 represents 子句：

　　清单 6. elementsInQueue 的 represents 子句

　　该子句指出 elementsInQueue 等于 m_elements[] 中从下标 1 到 m_size 的值(包含 1 和 m_size)。 m_elements[] 是 BinaryHeap 中的私有成员变量，用于将元素存储在优先级队列中。 m_size 是 m_elements[] 中当前所使用元素的数目。 BinaryHeap 不使用 m_elements[0] ;这简化了二进制堆的下标计算。 JMLObjectBag.convertFrom() 将 List 转换成 JMLObjectBag ，这是 elementsInQueue 所需的数据类型。

　　无论 JML 运行时断言检查器何时需要 elementsInQueue 的值，它都会查看 represents 子句中 <- 右边的代码段。

　　副作用

　　回忆一下清单 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 结合使用。

        代码下载