应用建模语言JML改进Java程序

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