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