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

核心提示：来自:http://www-106.ibm.com/ 作者:Joe Verzulli 量词（Quantification）（译者注：这里量词的意思与逻辑学上的量词意思相近，而不是普通意义上理解的量词，JML起步－－使用JML 改进你的Java程序(2)，）在上面pop()方法的行为规范中，我们说它的返回值要等于pe

　　来自:http://www-106.ibm.com/ 作者:Joe Verzulli


量词（Quantification）（译者注：这里量词的意思与逻辑学上的量词意思相近，而不是普通意义上理解的量词。）


在上面pop()方法的行为规范中，我们说它的返回值要等于peek()方法的返回值，不过我们并没有看到关于peek()方法的规范。PRiorityQueue中peek()方法的行为规范请看下面的代码：



代码段3 PriorityQueue 中peek()方法的行为规范





/*@

@ public normal_behavior

@ requires ! isEmpty();

@ ensures elementsInQueue.has(esult);

@*/

/*@ 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(esult, obj)

@ <= 0)) &&

@ ((! isMinimumHeap) ==>

@ (forall Object obj;

@ elementsInQueue.has(obj);

@ compareObjects(esult, obj)

@ >= 0));

@*/

public Object peek() throws NoSuchElementException



使用量词


上面代码段4中的后置条件包含两个部分，分别用于大顶堆和小顶堆的情况。“==>”符号的意思是包含（译者注：这个包含与逻辑学中包含的意思一致）。x ==> y 当且仅当y为真或x为假时取真值。对于小顶堆排序来说，适用下面所列的代码：



(forall Object obj;

elementsInQueue.has(obj);

compareObjects(