量词（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)
@
@
((! isMinimumHeap) ==
@
(\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)
上面的代码中\forall是一个JML量词。上面\forall表达式当所有的对象obj满足elementsInQueue.has(obj)为真且compareObjects(\result, obj)返回一个非正数两个条件时才为真。换言之，当使用compareObjects()进行比较时，peek()方法的返回值一定小于或等于elementsInQueue中每一个元素的值。其他的JML量词还有\exists、\sum以及 \min等等。
使用Comparator进行比较
BinaryHeap类允许以两种方法比较元素的大小。一种方法是要进行比较的元素自己实现Comparable接口，比较过程使用元素中定义的方法进行。另外一种方法是客户类在构造BinaryHeap类的实例时向构造函数传入一个Comparator对象，使用该Comparator对象进行比较。无论使用哪一种比较方式，我们都使用模型域comparator来表示比较大小所用的Comparator对象。 在peek()方法的后置条件中，compareObjects()方法使用客户端选择的比较方式来进行元素的比较。compareObjects()方法定义如下：
代码段5
compareObjects() 方法
/*@
@ public normal_behavior
@
ensures
@
(comparator == null) ==
@
(\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
这个语句的意思是模型域isMinimumHeap的值等于m_isMinHeap的值，其中，m_isMinHeap是BinaryHeap类中一个私有的布尔变量。 一旦需要用到isMinimumHeap的值，JML就会把m_isMinHeap的值赋给它。
represents语句并没有限制
代码段6
elementsInQueue 的represents语句
/*@ private represents elementsInQueue
@
@
Arrays.asList(m_elements)
@
.subList(1, m_size + 1));
@*/
从这里我们可以看出，elementsInQueue的元素就是数组m_elements[]从第一个元素到第m_size个元素共m_size个元素构成的列表，其中数组m_elements[]是BinaryHeap的一个私有成员，用来存储优先级队列中的元素，m_size是m_elements[]中正在使用的元素的个数。类BinaryHeap没有使用m_elements[0]，这样可以简化对于索引的操作。JMLObjectBag.convertFrom()的作用是把一个List结构转化为一个elementsInQueue所需要的JMLObjectBag结构。这样一旦JML运行时进行断言检查的时候需要elementsInQueue的值，系统就会计算represents 语句
