【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 注释

1 /*@2 3 @ public normal_behavior4 5 @ requires ! isEmpty();6 7 @*/8 9 Object pop()throwsNoSuchElementException;10

如前面所述，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() 的后置条件中所使用的模型字段

1 /*@2 3 @ public normal_behavior4 5 @ requires ! isEmpty();6 7 @ ensures8 9 @ elementsInQueue.equals(((JMLObjectBag)10 11 @ \old(elementsInQueue))12 13 @ .remove(\result)) &&14 15 @ \result.equals(\old(peek()));16 17 @*/18 19 Object pop()throwsNoSuchElementException;20 21

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

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

类级不变量

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