JML起步---使用JML 改进你的Java程序(2)

内容: 来自:http://www-106.ibm.com/ 作者:Joe Verzulli 量词（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) @ @ (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) @ (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