文档介绍：应用建模语言JML改进Java程序
寿智振
Java建模语言(Java Modeling Language,JML)是一种进行详细设计的符号语言,它鼓励你用一种全新的方式来看待Java的类和方法。面向对象的分析和设计(OOAD)的一个重要原则就是过程性的思考应该尽可能地推迟,不过遵循这个原则的大多数人也不过是把这个原则适用到方法实现这个级别上。一旦设计好了类和接口,下面的事情自然就是实现其中定义的方法了。对呀,我们还能做什么呢?还有什么其它方法可以使用吗?毕竟,用Java进行程序设计和用其他语言进行程序设计一样,我们都要一步一步地实现每一个方法。 
标记本身只是表示如何做一个事情(how to do something),根本不管我们希望做什么。如果我们在做一个事情之前就能够知道我们能够达到什么样的结果是非常好的,不过Java语言并没有给我们提供一个可以显式地把这些信息插入到我们程序代码的方法。Java建模语言(Java Modeling Language,JML)在Java代码中增加了一些符号,这些符号用来标识一个方法是干什么的,却并不关心它的实现。如果使用JML的话,我们就能够描述一个方法的预期的功能而不管他如何实现。通过这种方式,JML把过程性的思考延迟到方法设计中,从而扩展了面向对象设计的这个原则。JML引入了大量用于描述行为的结构,比如有模型域、量词、断言可视范围、预处理、后处理、条件继承以及正常行为(与异常行为相对)规范等等。这些结构使得JML非常强大,不过你并不必要理解或者使用上面所述的所有方面,也不需要一次使用所有的这些方面。
这篇文章中采用循序渐进的方式来介绍JML。我们要先了解一下使用JML的各种好处,特别是对开发和编译过程的影响。然后,我们要讨论一下JML的一些结构,比如前置条件、后置条件、模型域、量词、副作用以及异常行为等等。同时,在讨论这些结构的同时,我们会给出一些例程来给你一个直观的感觉。这样经过本文你将可以对JML是如何工作的有一个概念性的理解,从而能够在你自己的项目中应用JML。 
一、Java建模语言JML对Jave程序代码的改进
使用JML来声明性地描述一个方法或类的预期行为可以显著提高整体的开发进程。把建模标记加入到你的Java程序代码中有以下好处:
能够更为精确地描述这些代码是做什么的
能够高效地发现和修正程序中的bug
可以在应用程序升级时降低引入bug的机会
可以提早发现客户代码对类的错误使用
可以提供与应用程序代码完全一致的JML格式的文档
JML标记总是在Java注释的内部,所以对正常编译的代码没有任何影响。如果你想比较一下普通的类和使用了JML的类有什么差别的话,你可以使用一个开源的JML编译器。用JML编译器编译的代码如果没有实现JML规范所要求的事项,运行时就会抛出一个JML异常。这个特性不仅可以帮助我们捕获代码中的bug,而且可以确保JML形式的文档可以与程序代码高度一致。mons ponent ()项目中的PriorityQueue接口和
BinaryHeap 类来演示JML的各种性质。在这里你可以找到使用了JML标记完整的这个两个文件。 
1、确定类实现的规范
中的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要求