在 pop() 先前的规范中，我们说它的返回值等于 peek() 的返回值，但是我们不曾研究 peek() 的规范。 PriorityQueue 中 peek() 的规范如清单 3 所示：
清单 3. PriorityQueue 中 peek() 的规范
2 @ public normal_behavior
3 @ requires ! isEmpty();
4 @ ensures elementsInQueue.has(\result);
5 @*/
6 /*@ pure @*/ Object peek() throws NoSuchElementException;
7
该 JML 注释指出应当在队列中至少有一个元素时才调用 peek() 。它还指出 peek() 返回的值必须位于 elementsInQueue 中;也就是说，这个值必须是先前插入到队列中的值。
/*@ pure @*/ 注解指出 peek() 是一个纯方法。 纯方法(pure method)就是没有副作用的方法。JML 只允许断言使用纯方法。我们将 peek() 声明为纯方法，这样就可以在 pop() 的后置条件中使用它。如果 JML 允许在断言中使用非纯方法，那么我们可能就会在无意之中编写出具有副作用的规范。这可能会导致代码在启用断言检查进行编译时可以正常运行，而在禁用断言检查时则无法运行。我们待会将进一步讨论副作用。
关于继承
JML 规范是由实现接口的子类和类继承的(不同于 J2SE 1.4 中的断言语句)。JML 关键字 also 指出规范是与从祖先类继承的规范和从实现的接口继承的规范合并在一起的。因此， PriorityQueue 接口中的 peek() 的规范也适用于 BinaryHeap 中的 peek() 。这意味着 BinaryHeap.peek() 返回的值必须位于 elementsInQueue 中，即使这没有在 BinaryHeap.peek() 规范中显式说明。
最小堆和最大堆
peek() 规范中显然遗漏了一件事。它从未指出返回值就是具有最高优先级的那个值。结果是 JCCC 中 PriorityQueue 接口既可以用于最小堆也可以用于最大堆。对于最小堆，具有最高优先级的元素是最小的元素，而对于最大堆，具有最高优先级的元素是最大的元素。这是因为 PriorityQueue 不知道它正在与最小堆还是最大堆一起使用，所以指出返回哪个元素的那部分规范必须放入实现 PriorityQueue 的类中。
在 JCCC 中， BinaryHeap 类实现 PriorityQueue 。 BinaryHeap 允许客户机通过构造函数中的一个参数来指定它应当用作最小堆还是最大堆。我们使用布尔模型变量 isMinimumHeap 来指出 BinaryHeap 是用作最小堆还是最大堆。 BinaryHeap 中 peek() 的规范使用了 isMinimumHeap ，如清单 4 所示：
清单 4. BinaryHeap 类中 peek() 的规范
2
3 @ also
4
5 @ public normal_behavior
6
7 @ requires ! isEmpty();
8
9 @ ensures
10
11 @ (isMinimumHeap ==>
12
13 @ (\forall Object obj;
14
15 @ elementsInQueue.has(obj);
16
17 @ compareObjects(\result, obj)
18
19 @ <= 0)) &&
20
21 @ ((! isMinimumHeap) ==>
22
23 @ (\forall Object obj;
24
25 @ elementsInQueue.has(obj);
26
27 @ compareObjects(\result, obj)
28
29 @ >= 0));
30
31 @*/
32
33 public Object peek() throws NoSuchElementException
34
35
添加量词
清单 4 中的后置条件包括了两个部分，一部分是最小堆的后置条件，另一部分是最大堆的后置条件。 ==> 符号表示“暗示”。 x ==> y 当(且仅当)y 为 true 或 x 为 false 时才为 true。对于最小堆，下列条件适用：
2 elementsInQueue.has(obj);
3 compareObjects(\result, obj) <= 0)
4
\forall 是 JML 量词。如果对于所有 Objects obj ， elementsInQueue.has(obj) 为 true 并且 compareObjects(\result, obj) 返回一个小于等于零的值，那么上面的 \forall 表达式为 true。换句话说，当 compareObjects() 用于比较值的大小时， peek() 返回的值小于等于 elementsInQueue 中的任何元素。其它的 JML 量词包括 \exists 、 \sum 和 \min 。
添加比较器
BinaryHeap 类允许用两种不同的方法对元素进行比较。一种方法是使用 Comparable 接口依靠元素的自然排序来进行。另一种方法是让客户机将 Comparator 对象传递给 BinaryHeap 构造函数。然后将使用 Comparator 来进行排序。我们使用模型字段 comparator 来表示 Comparator 对象(如果有的话)。 peek() 后置条件中的 compareObjects() 方法使用客户机所选中的任一比较方法。 compareObjects() 的定义如清单 5 所示：
清单 5. compareObjects() 方法
2 @ public normal_behavior
3 @ ensures
4 @ (comparator == null) ==>
5 @ (\result == ((Comparable) a).compareTo(b)) &&
6 @ (comparator != null) ==>
7 @ (\result == comparator.compare(a, b));
8 @
9 @ public pure model int compareObjects(Object a, Object b)
10 @ {
11 @ if (m_comparator == null)
12 @ return ((Comparable) a).compareTo(b);
13 @ else
14 @ return m_comparator.compare(a, b);
15 @ }
16 @*/
17
compareObjects 声明中的关键字 model 表明这是一个模型方法。 模型方法是只能在规范中使用的 JML 方法。它们是在 Java 注解中声明的，不能用在正规的 Java 实现代码中。
如果 BinaryHeap 的客户机要求使用特定的 Comparator ，那么 m_comparator 将引用该 Comparator ;否则它就为 null。 compareObjects() 检查 m_comparator 的值并使用适当的比较操作。
模型字段如何获取值
我们在清单 4 中显示了 peek() 的后置条件。后置条件验证返回值的优先级是否大于等于模型字段 elementsInQueue 中所有元素的优先级。这产生了一个问题：诸如 elementsInQueue 这样的模型字段如何获取它们的值?前提条件、后置条件和不变量都必须没有副作用，因此它们不能设置模型字段的值。
JML 使用 represents 子句来将模型字段和具体实现字段相关联。例如，下面的 represents 子句被用于模型字段 isMinimumHeap ：
2
该子句指出模型字段 isMinimumHeap 的值等于 m_isMinHeap 的值。 m_isMinHeap 是 BinaryHeap 类中的私有布尔成员字段。无论何时需要 isMinimumHeap 的值，JML 都将用 m_isMinHeap 的值来替换。
represents 子句在 <- 右边并不只限于成员字段。请研究下面这个 elementsInQueue 的 represents 子句：
清单 6. elementsInQueue 的 represents 子句
2
3 @ <- JMLObjectBag.convertFrom(
4
5 @ Arrays.asList(m_elements)
6
7 @ .subList(1, m_size + 1));
8
9 @*/
10
11
该子句指出 elementsInQueue 等于 m_elements[] 中从下标 1 到 m_size 的值(包含 1 和 m_size)。 m_elements[] 是 BinaryHeap 中的私有成员变量，用于将元素存储在优先级队列中。 m_size 是 m_elements[] 中当前所使用元素的数目。 BinaryHeap 不使用 m_elements[0] ;这简化了二进制堆的下标计算。 JMLObjectBag.convertFrom() 将 List 转换成 JMLObjectBag ，这是 elementsInQueue 所需的数据类型。
无论 JML 运行时断言检查器何时需要 elementsInQueue 的值，它都会查看 represents 子句中 <- 右边的代码段。
