Java建模语言（Java Modeling Language，JML）是一种进行详细设计的符号语言，他鼓励你用一种全新的方式来看待Java的类和方法。本教程中，Java程序设计资深顾问Joe Verzulli 将会给大家介绍这一新的工具以及如何使用这个工具。
　　
　　面向对象的分析和设计（OOAD）的一个重要原则就是过程性的思考应该尽可能地推迟，不过遵循这个原则的大多数人也不过是把这个原则适用到方法实现这个级别上。一旦设计好了类和接口，下面的事情自然就是实现其中定义的方法了。对呀，我们还能做什么呢？还有什么其它方法可以使用吗？毕竟，用Java进行程序设计和用其他语言进行程序设计一样，我们都要一步一步地实现每一个方法。
　　
　　标记本身只是表示如何做一个事情（how to do something），根本不管我们希望做什么。如果我们在做一个事情之前就能够知道我们能够达到什么样的结果是非常好的，不过Java语言并没有给我们提供一个可以显示地把这些信息插入到我们程序代码的方法。
　　
　　Java建模语言（Java Modeling Language，JML）在Java代码中增加了一些符号，这些符号用来标识一个方法是干什么的，却并不关心它的实现。如果使用JML的话，我们就能够描述一个方法的预期的功能而不管他如何实现。通过这种方式，JML把过程性的思考延迟到方法设计中，从而扩展了面向对象设计的这个原则。
　　
　　JML引入了大量用于描述行为的结构，比如有模型域、量词、断言可视范围、预处理、后处理、条件继承以及正常行为（与异常行为相对）规范等等。这些结构使得JML非常强大，不过你并不必要理解或者使用上面所述的所有方面，也不需要一次使用所有的这些方面。你可以一点一点的学习，从非常简单的开始。
　　
　　这篇文章中采用循序渐进的方式来介绍JML。我们要先了解一下使用JML的各种好处，特别是对开发和编译过程的影响。然后，我们要讨论一下JML的一些结构，比如前置条件、后置条件、模型域、量词、副作用以及异常行为等等。同时，在讨论这些结构的同时，我们会给出一些例程来给你一个直观的感觉。这样经过本文的学习，你将可以对JML是如何工作的有一个概念性的理解，从而能够在你自己的项目中应用JML。
　　
　　JML概览
　　使用JML来声明性地描述一个方法或类的预期行为可以显著提高整体的开发进程。把建模标记加入到你的Java程序代码中有以下好处：
　　
　　能够更为精确地描述这些代码是做什么的
　　能够高效地发现和修正程序中的bug
　　可以在应用程序升级时降低引入bug的机会
　　可以提早发现客户代码对类的错误使用
　　可以提供与应用程序代码完全一致的JML格式的文档
　　JML标记总是在Java注释的内部，所以对正常编译的代码没有任何影响。如果你想比较一下普通的类和使用了JML的类有什么差别的话，你可以使用一个开源的JML编译器（请参考 如下地址）。用JML编译器编译的代码如果没有实现JML规范所要求的事项，运行时就会抛出一个JML异常。这个特性不仅可以帮助我们捕获代码中的bug，而且可以确保JML形式的文档可以与程序代码高度一致。
　　
　　文章下面的部分，我将使用开放源代码的Jakarta Commons Collection Component （JCCC）项目中的PriorityQueue接口和BinaryHeap 类来演示JML的各种性质。在这里你可以找到使用了JML标记完整的这个两个文件。
　　
　　要求和责任
　　本文中使用的代码（请参考 如下地址）包括开源项目JCCC中的PriorityQueue 接口。接口嘛，自然是声明了一些方法的签名，包括方法的参数类型、返回值的类型，并不涉及方法的实现。一般情况下或者只是按照Java语法要求的话，实现接口的类只要实现了接口中定义的各个方法即可，不论实现的方式是多么地离奇古怪。我们并不想这样，我们希望能够确定一个行为规范，所有实现这个接口的类都用我们指定的方式来实现这个接口中定义的方法。通过使用JML我们可以做到这一点。
　　
　　考虑一下PriorityQueue接口的pop()方法，对于优先级队列来说，pop()方法应该有什么样的功能要求？最起码应该有三个：第一，如果要调用pop()方法，队列中至少要有一个元素；第二，该方法应该返回队列中优先级最高的那个元素；第三，该方法应该从队列中删除返回的那个元素。
　　
　　下面代码段显示了表示满足第一个要求的JML标记：
　　
　　代码段1　pop()方法功能规范的JML标记
　　
　　/*@
　　
　　　 @　 public normal_behavior
　　
　　　 @　　 requires ! isEmpty();
　　
　　　 @*/
　　
　　Object pop() throws NoSuchElementException;
　　
　　前面已经提到，JML标记是写在Java代码的注释中的。包含JML标记的多行注释以/*@ 开头，JML忽略任何以@开头的空行。如果是单行的话，你也可以使用//@这种标记。
　　
　　这里JML注释中public关键字与Java中的public意思是一样的，它表示程序中其他所有的类都要遵循这个JML要求。Public要求只能应用在public方法和public成员变量上。JML同样有private-、 protected-、 以及 package-级别的作用域。同样，这些作用域的规则与Java语言中作用域的规则非常相似。
　　
　　这里normal_behavior关键字的意思是，这个JML要求表示这是一种正常情况，运行时不会抛出异常。后面，我们会描述异常行为是怎么被界定的。
　　
　　前置条件和后置条件
　　JML关键字requires用来表示前置条件，前置条件表示调用一个方法前必须满足的一些要求。上面代码段中包含一个前置条件，它要求调用pop()方法的前提就是isEmpty()方法返回false，也就是说要求这个队列至少含有一个元素。
　　
　　一个方法的后置条件规范表示一个方法的责任，也就是说当这个方法返回时，它必须满足这个后置条件的要求。在我们上面的例子中，pop()方法应该返回队列中优先级最高的元素。我们希望指定一个后置条件要求JML在运行时检查是否满足这个事实。要做到这一点，我们必须跟踪所有添加到这个优先级队列中的元素，这样我们就可以判断pop()方法应该返回哪一个元素。怎么做呢？你可能会考虑在PriorityQueue接口中加入一个成员变量来存储队列中元素的值，不过这样做有两个问题：
　　
　　PriorityQueue是一个接口，它可能有各种不同具体的实现方式，比如说binary heap、Fibonacci heap或者calendar queue等等，它要与它的各种实现一致，况且JML标记不应该涉及到任何具体的实现细节。
　　作为一个接口，PriorityQueue只能拥有静态成员变量。
　　为了处理这种情况，JML引入了一个叫做模型域（model fields）的概念。
　　
　　模型域
　　模型域类似于成员变量，它只能被应用到行为规范中。这是一个PriorityQueue中声明模型域的例子：
　　
　　//@ public model instance JMLObjectBag elementsInQueue;
　　
　　这个声明的意思是说这里有一个叫做elementsInQueue的模型域，它的类型是JMLObjectBag （这个数据类型是在JML中定义的）。instance关键字表示虽然这个域是定义在接口中，可是任何实现这个接口的类都拥有一个单独的、非静态的elementsInQueue域。与其他JML标记一样，这个声明也是出现在注释中的，所以常规的Java代码是不能使用这个elementsInQueue变量的。在程序运行的时候，是没有任何对象拥有一个叫做elementsInQueue的成员变量的。
　　
　　行为规范与实现
　　使用一个包来存储队列中的元素，然后检查每一个元素找出优先级最高的那一个会让人觉得效率不高。不过这只是行为规范的一部分，而不会涉及到实现。行为规范的作用在于描述 PriorityQueue的行为接口，也就是说规定了使用 PriorityQueue的客户代码所能依赖的外部行为。
　　
　　PriorityQueue接口的各个具体实现只要可以满足这个行为规范的要求，就可以使用任何更为高效的方法。比如说，JCCC有一个实现这个接口的 BinaryHeap类，它的实现方式就是使用一个存储在数组中的 binary heap 。
　　
　　不过虽然用JML定义行为规范的时候不需要考虑执行效率，程序运行时JML断言检查却是很重要的。所以开启断言检查时程序的运行可能会有性能的压力。
　　
　　elementsInQueue 存储添加到优先级队列的元素的值，下面的代码段显示pop()方法如何使用elementsInQueue：
　　
　　代码段2　在pop()的后置条件中使用模型域
　　
　　/*@
　　
　　　 @ public normal_behavior
　　
　　　 @　 requires ! isEmpty();
　　
　　　 @　 ensures
　　
　　　 @　　 elementsInQueue.equals(((JMLObjectBag)
　　
　　　 @　　　　　\old(elementsInQueue))
　　
　　　 @　　　　　　　　　　　　.remove(\result)) &&
　　
　　　 @　　 \result.equals(\old(peek()));
　　
　　　 @*/
　　
　　Object pop() throws NoSuchElementException;
　　
　　ensures关键字表示后面跟着的是pop()方法返回时必须满足的后置条件。\result是一个JML关键字，它等于pop()方法的返回值。\old()是一个JML函数，它返回pop()方法调用之前参数的值。
　　
　　这个ensures语句包含了两个后置条件。第一，pop()方法返回的那个元素必须要从elementsInQueue删除。第二，这个返回值要与peek()方法返回的值一致。
　　
　　类级别的不变量
　　我们现在已经看到JML能够让我们规定方法的前置条件和后置条件，它同样也允许我们指定类级别的不变量。类级别的不变量指的是进入和退出一个类中每个方法都必须满足的条件。比方说吧，//@ public instance invariant elementsInQueue != null; 就是PriorityQueue的一个不变量，它的意思是任何实现PriorityQueue的类一旦被实例化，elementsInQueue的值就不能是null。

查看本文来源

　　量词（Quantification）（译者注：这里量词的意思与逻辑学上的量词意思相近，而不是普通意义上理解的量词。）
　　
　　在上面pop()方法的行为规范中，我们说它的返回值要等于peek()方法的返回值，不过我们并没有看到关于peek()方法的规范。PriorityQueue中peek()方法的行为规范请看下面的代码：
　　
　　代码段3　PriorityQueue 中peek()方法的行为规范
　　
　　/*@
　　
　　　 @ public normal_behavior
　　
　　　 @　 requires ! isEmpty();
　　
　　　 @　 ensures elementsInQueue.has(\result);
　　
　　　 @*/
　　
　　/*@ pure @*/ Object peek() throws NoSuchElementException;
　　
　　JML标记要求只有当队列中至少含有一个元素的时候，才能调用peek()方法，同时他还要求方法的返回值必须在elementsInQueue之内，也就是说，这个返回值一定是这个队列中的一个元素。
　　
　　注释/*@ pure @*/ 表明peek()方法是一个纯方法（pure method），纯方法是指没有副作用的方法。JML中只允许使用纯方法进行断言确认，所以我们把peek()声明为纯方法，这样我们就可以在pop()方法的后置条件中使用peek()方法。大家肯定想知道，为什么JML只允许使用纯方法进行断言确认？问题是这样的，如果JML允许使用非纯方法进行断言确认的话，我们稍不注意就会写出有副作用的行为规范。比如说可能会有这么一种情况，开启了断言确认以后，我们的代码正确无误，可是如果禁止了断言确认后，我们的代码却不能运行了，或运行出错了。这样当然不行！后面，我们还会进一步讨论副作用的问题。
　　
　　关于继承
　　JML行为规范可以被子类（含子接口）或者是实现接口的类所继承，这一点与J2SE1.4中断言有所不同。JML关键字 also表示当前定义的行为规范与祖先类或被实现的接口中所定义的行为规范一起作用。因而，在 PriorityQueue接口定义的 peek()方法的行为规范同样适用于 BinaryHeap类中的 peek()方法。这个就意味着，虽然在 BinaryHeap.peek()的行为规范中没有明确定义， BinaryHeap.peek()的返回值也必须在 elementsInQueue当中。
　　
　　大顶堆和小顶堆（译者注：大顶堆和小顶堆是数据结构里面的概念，分别表示堆排序方法的不同实现方式。堆排序是一种通过调整二叉树进行排序的方法。）
　　
　　上面我们给peek()定义的行为规范明显缺少了一块，那就是我们根本没有要求它返回的那个元素具有最大的优先级。显然，JCCC的PriorityQueue接口既可以用于大顶堆，也可以用于小顶堆。大顶堆和小顶堆的表现是有些差别的，在小顶堆中优先级最高的元素值最小，而大顶堆中优先级最高的元素值最大。因为PriorityQueue并不知道自己被用来进行大顶堆排序还是小顶堆排序，所以指定返回哪个元素的规范必须在实现PriorityQueue接口的类中进行定义。
　　
　　在JCCC 中，类 BinaryHeap实现了PriorityQueue接口。BinaryHeap允许使用它的客户代码在构造函数中通过一个参数来指定排序方案，也就是通过参数来指定是通过大顶堆方式排序还是通过小顶堆方式排序。我们使用一个boolean模型变量isMinimumHeap来判断BinaryHeap的排序方式是大顶堆还是小顶堆。下面的例子是BinaryHeap使用isMinimumHeap给peek()方法定义的行为规范：
　　
　　代码段4　 BinaryHeap 类中peek()方法的行为规范
　　
　　/*@
　　
　　　 @ also
　　
　　　 @　 public normal_behavior
　　
　　　 @　　 requires ! isEmpty();
　　
　　　 @　　 ensures
　　
　　　 @　　　 (isMinimumHeap ==>
　　
　　　 @　　　　　 (\forall Object obj;
　　
　　　 @　　　　　　　　　elementsInQueue.has(obj);
　　
　　　 @　　　　　　　　　compareObjects(\result, obj)
　　
　　　 @　　　　　　　　　　　　　　 <= 0)) &&
　　
　　　 @　　　 ((! isMinimumHeap) ==>
　　
　　　 @　　　　　 (\forall Object obj;
　　
　　　 @　　　　　　　　　elementsInQueue.has(obj);
　　
　　　 @　　　　　　　　　compareObjects(\result, obj)
　　
　　　 @　　　　　　　　　　　　　　 >= 0));
　　
　　　 @*/
　　
　　public Object peek() throws NoSuchElementException
　　
　　使用量词
　　上面代码段4中的后置条件包含两个部分，分别用于大顶堆和小顶堆的情况。“==>”符号的意思是包含（译者注：这个包含与逻辑学中包含的意思一致）。x ==> y 当且仅当y为真或x为假时取真值。对于小顶堆排序来说，适用下面所列的代码：
　　
　　(\forall Object obj;
　　
　　　　　　　elementsInQueue.has(obj);
　　
　　　　　　　compareObjects(\result, obj) <= 0)
　　
　　上面的代码中\forall是一个JML量词。上面\forall表达式当所有的对象obj满足elementsInQueue.has(obj)为真且compareObjects(\result, obj)返回一个非正数两个条件时才为真。换言之，当使用compareObjects()进行比较时，peek()方法的返回值一定小于或等于elementsInQueue中每一个元素的值。其他的JML量词还有\exists、\sum以及 \min等等。
　　
　　使用Comparator进行比较
　　BinaryHeap类允许以两种方法比较元素的大小。一种方法是要进行比较的元素自己实现Comparable接口，比较过程使用元素中定义的方法进行。另外一种方法是客户类在构造BinaryHeap类的实例时向构造函数传入一个Comparator对象，使用该Comparator对象进行比较。无论使用哪一种比较方式，我们都使用模型域comparator来表示比较大小所用的Comparator对象。 在peek()方法的后置条件中，compareObjects()方法使用客户端选择的比较方式来进行元素的比较。compareObjects()方法定义如下：
　　
　　代码段5　　compareObjects() 方法
　　
　　/*@
　　
　　　 @ public normal_behavior
　　
　　　 @　 ensures
　　
　　　 @　　 (comparator == null) ==>
　　
　　　 @　　　　 (\result == ((Comparable) a).compareTo(b)) &&
　　
　　　 @　　 (comparator != null) ==>
　　
　　　 @　　　　 (\result == comparator.compare(a, b));
　　
　　　 @
　　
　　　 @ public pure model int compareObjects(Object a, Object b)
　　
　　　 @ {
　　
　　　 @ if (m_comparator == null)
　　
　　　 @　　 return ((Comparable) a).compareTo(b);
　　
　　　 @ else
　　
　　　 @　　 return m_comparator.compare(a, b);
　　
　　　 @ }
　　
　　　 @*/
　　
　　compareObjects方法的定义中使用了另外一个关键字model，它的意思是compareObjects方法是一个模型方法。模型方法是只能用在行为规范中的JML方法。模型方法定义在Java的注释中，所以常规的Java代码不能使用。
　　
　　如果BinaryHeap类的客户代码指定了一个特殊的Comparator用来进行比较的话，m_comparator就指向那个Comparator，否则m_comparator的值就是null。compareObjects()方法检查m_comparator的值，然后采用适当的方法进行元素间的比较。
　　
　　模型域如何取值
　　在代码段4中我们讨论了peek()方法的后置条件。这个条件保证peek()方法的返回值的优先级大于或者等于模型域elementsInQueue中所有的元素的优先级。那么有一个问题，像elementsInQueue这样的模型域如何取值？前置条件、后置条件和不变量都是没有副作用的，所以不能使用它们来设置模型域的值。
　　
　　JML使用一个represents语句把模型域与具体的实现域关联起来。比如下面的represents语句用来给模型域isMinimumHeap赋值：
　　
　　//@ private represents isMinimumHeap <- m_isMinHeap;
　　
　　这个语句的意思是模型域isMinimumHeap的值等于m_isMinHeap的值，其中，m_isMinHeap是BinaryHeap类中一个私有的布尔变量。 一旦需要用到isMinimumHeap的值，JML就会把m_isMinHeap的值赋给它。
　　
　　represents语句并没有限制<-右边必须是成员变量。比如说，下面是elementsInQueue的represents语句：
　　
　　代码段6　 elementsInQueue 的represents语句
　　
　　/*@ private represents elementsInQueue
　　
　　　 @　　　　 <- JMLObjectBag.convertFrom(
　　
　　　 @　　　　　　　　　 Arrays.asList(m_elements)
　　
　　　 @　　　　　　　　　　 .subList(1, m_size + 1));
　　
　　　 @*/
　　
　　从这里我们可以看出，elementsInQueue的元素就是数组m_elements[]从第一个元素到第m_size个元素共m_size个元素构成的列表，其中数组m_elements[]是BinaryHeap的一个私有成员，用来存储优先级队列中的元素，m_size是m_elements[]中正在使用的元素的个数。类BinaryHeap没有使用m_elements[0]，这样可以简化对于索引的操作。JMLObjectBag.convertFrom()的作用是把一个List结构转化为一个elementsInQueue所需要的JMLObjectBag结构。这样一旦JML运行时进行断言检查的时候需要elementsInQueue的值，系统就会计算represents 语句<-符号右边的代码并进行求值。

查看本文来源

　　请大家回忆一下代码段2中pop()方法的后处理代码：
　　
　　ensures
　　
　　elementsInQueue.equals(((JMLObjectBag)
　　
　　　　　　　　 \old(elementsInQueue))
　　
　　　　　　　　　　　　　　　 .remove(\result)) &&
　　
　　\result.equals(\old(peek()));
　　
　　这里我们说有一个副作用，那就是在从elementsInQueue删除一个元素的时候会有副作用。事实上，这里还可能有其他的副作用。比方说，一个pop()方法的具体实现中如果修改了m_isMinHeap的值，那么就把排序方法从一个小顶堆变成了大顶堆。只要这种修改能够返回正确结果，就不会引起运行期间的断言检查异常，可是这个却事实上削弱了JML行为规范的作用。我们可以加强后置条件，不允许除了修改elementsInQueue以外的任何改变，请看下面的代码：
　　
　　代码断7　　加强的后置条件
　　
　　ensures
　　
　　elementsInQueue.equals(((JMLObjectBag)
　　
　　　　　　　　\old(elementsInQueue))
　　
　　　　　　　　　　　　　　　 .remove(\result)) &&
　　
　　\result.equals(\old(peek())) &&
　　
　　isMinimumHeap == \old(isMinimumHeap) &&
　　
　　comparator == \old(comparator);
　　
　　从中我们可以看出，通过加入形如x == \old(x)的语句，我们可以消除变量x发生改变的副作用。可是有一个问题，如果用这种办法，每一个方法在它的后置条件都要为每一个变量加上这么一句，这样就会导致行为规范的混乱。而且如果我们给一个类增加一个成员的变量的话，那么我们就得在这个类的所有方法的后处理规范中增加一句，这将让维护变得异常困难。 JML通过引入assignable语句提供了一种更好地解决方案。
　　
　　assignable 语句
　　使用assignable语句，我们可以这样完成pop()方法的后置条件：
　　
　　代码段8　　在方法的行为规范中使用assignable语句
　　
　　/*@
　　
　　　 @ public normal_behavior
　　
　　　 @　 requires ! isEmpty();
　　
　　　 @　 assignable elementsInQueue;
　　
　　　 @　 ensures
　　
　　　 @　　 elementsInQueue.equals(((JMLObjectBag)
　　
　　　 @　　　　　\old(elementsInQueue))
　　
　　　 @　　　　　　　　　　　　.remove(\result)) &&
　　
　　　 @　　 \result.equals(\old(peek()));
　　
　　　 @*/
　　
　　Object pop() throws NoSuchElementException;
　　
　　只有在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语句意味着方法不仅可以修改显式声明的isMinimumHeap，而且还能修改m_isMinHeap。）
　　方法开始执行时loc尚没有分配。
　　loc 是方法的局部变量或者是方法的形式参数。
　　最后一种情况允许一个方法修改它的参数，即使这个参数没有显式地出现在assignable语句中。粗略一看，这个好像允许一个方法通过参数传递允许它的调用者修改变量的值。比方说，有一个方法foo(Bar obj)，它里面有一个语句obj = anotherBar。不过虽然这个语句修改了obj的值，却不会影响到foo()的调用者，因为虽然这两个obj都是指向一个Bar对象，而且具有一样的名字，foo()方法中的此obj实际上与foo()的调用者中的彼obj是不同的（译者注：关于这一点，请参考Java中索引与对象的概念）。
　　
　　现在我们考虑如果方法foo(Bar obj)里面有一个语句obj.x = 17会怎么样？这个将显式地改变调用者中的变量。这是有问题的。assignable 语句的规则允许一个方法不需要在assignable 语句中声明就可以修改传入参数的值，不过它并不允许修改参数的成员变量，具体在这里来说，就是不允许修改obj.x的值。如果你希望在foo()方法中修改obj.x的值，你就必须在assignable 语句中声明，你可以写assignable obj.x; 。
　　
　　assignable 语句中可以使用两个JML关键字，\nothing和\everything。 我们可以通过assignable \nothing 语句来表明一个方法没有任何副作用；同样，我们可以通过assignable \everything语句来表明我们的方法可以修改一切变量的值。早先我们使用了一个JML关键字pure，它就等同于使用assignable \nothing; 。

查看本文来源

　　异常行为
　　前面给出的行为规范要求调用peek() 和 pop()方法时队列不能为空，但其实当队列空时是有可能会调用这两个方法的。如果发生这种情况，这两个方法就会抛出一个NoSuchElementException.异常。我们必须修正我们前面制定的行为规范，允许这种可能的发生。在这种情况下，我们要使用JML的exceptional_behavior语句。
　　
　　到目前，我们的行为规范还是以public normal_behavior打头的。这里normal_behavior关键字表示这是一个正常行为，方法不会抛出任何异常。使用public exceptional_behavior标记可以用来描述抛出异常的行为。下面的代码段显示了类PriorityQueue中peek()方法的行为规范中的异常部分：
　　
　　代码段9　　exceptional_behavior标记
　　
　　/*@
　　
　　　 @ public normal_behavior
　　
　　　 @　 requires ! isEmpty();
　　
　　　 @　 ensures elementsInQueue.has(\result);
　　
　　　 @ also
　　
　　　 @ public exceptional_behavior
　　
　　　 @　 requires isEmpty();
　　
　　　 @　 signals (Exception e) e instanceof NoSuchElementException;
　　
　　　 @*/
　　
　　/*@ pure @*/ Object peek() throws NoSuchElementException;
　　
　　像我们前面看到的所有例子一样，这个规范的第一部分也是以public normal_behavior开头，表示正常行为；不同的是，这个规范还有第二部分，以public exceptional_behavior开头，描述了异常行为。与normal_behavior 语句一样， exceptional_behavior 语句也有一个 requires 语句。这个requires 语句表示当抛出signals 语句中所列的异常时必须满足的条件。在上面的例子中，如果isEmpty()方法返回真的话，peek()就会抛出一个NoSuchElementException异常。
　　
　　signals 语句
　　signals 语句是形如signals(E e) R的语句，其中E是Exception类本身或其一个子类，R是一个表达式。JML 用如下方式解释一个signal 语句：如果有一个类型为E的异常抛出的话，就检查是否为R真。如果是，就执行既定规范；否则，抛出一个unchecked exception（译者注：unchecked exception又叫做RuntimeException，关于这两个概念，请参考Java语言中关于异常的描述），用以表示我们的程序代码违背了exceptional_behavior规范的要求。
　　
　　上面peek()方法中的signals语句的意思是如果队列为空，就抛出一个NoSuchElementException异常。如果peek()方法在运行中抛出不是NoSuchElementException的其它异常的话，那么JML就会把这当成一个错误，因为e instanceof NoSuchElementException不是true。如果你既想处理NoSuchElementException异常又想处理其它运行期异常，我们可以修改上面的signals语句，改为signals (NoSuchElementException e) true; 。这个意思是说，如果peek()方法抛出一个NoSuchElementException异常的话，那条件true必须为真，而true是一个常量，总是可以满足条件，所以对于NoSuchElementException异常的处理可以正常进行。不过我们这里并没有提及关于其它异常的信息，而peek()方法可以抛出它的签名（译者注：方法的签名是指，方法声明的各个部分，具体来说，是方法名称、参数类型、返回类型和抛出异常的总称）允许的任何异常。它的签名说它可以抛出NoSuchElementException异常，这就意味着它既可以抛出NoSuchElementException异常，又可以抛出RuntimeException。
　　
　　如果队列中存在一些元素而且当我们调用peek()方法时还是抛出一个NoSuchElementException异常（或者其他异常），JML运行期断言检查就会抛出一个unchecked exception，这表示正常的后置条件失败。
　　
　　结论
　　本文简单介绍了JML的概念，说明了它对面向对象系统的分析和设计的贡献，通过实例演示了如何在Java程序中使用JML标记。你可以从下面所列的资源中下载本文中所使用的完整的代码，还可以从中找到更多的关于JML的信息。
　　
　　你可以使用开源的JML编译器来编译你含有JML标记的代码，所生成的类文件会在运行时自动检查JML规范。如果你的程序没有实现规范中规定的事情，JML就会抛出一个unchecked exception 来说明你的程序违背了哪一条规范。这可以帮助我们捕获程序中的bug，而且能保证我们的代码与文档（JML格式的文档）高度一致。
　　
　　JML运行期断言检查编译器是第一个JML工具，其他相关工具还有jmldoc和jmlunit等等。Jmldoc与javadoc工具相似，不同的是它在生成的HTML格式文档中包含JML规范；jmlunit可以成生一个Java类文件测试的框架，它可以让你很方便地使用JUnit工具测试含有JML标记的Java代码。你还可以从下面所列的资源中找到其他关于JML各个方面的相关内容。
　　
　　在此请允许我向 Gary Leavens 和 Yoonsik Cheon表示深深的谢意，是他们帮我解决了一部分关于JML的疑问并且审阅了你所看到的这篇文章。

查看本文来源