內(nèi)容: 來自:http://www-106.ibm.com/ 作者:Joe Verzulli 量詞（Quantification）（譯者注：這里量詞的意思與邏輯學(xué)上的量詞意思相近，而不是普通意義上理解的量詞。）在上面pop()方法的行為規(guī)范中，我們說它的返回值要等于peek()方法的返回值，不過我們并沒有看到關(guān)于peek()方法的規(guī)范。PriorityQueue中peek()方法的行為規(guī)范請(qǐng)看下面的代碼： 代碼段3 PriorityQueue 中peek()方法的行為規(guī)范 /*@ @ public normal_behavior @ requires ! isEmpty(); @ ensures elementsInQueue.has(result); @*//*@ pure @*/ Object peek() throws NoSuchElementException; JML標(biāo)記要求只有當(dāng)隊(duì)列中至少含有一個(gè)元素的時(shí)候，才能調(diào)用peek()方法，同時(shí)他還要求方法的返回值必須在elementsInQueue之內(nèi)，也就是說，這個(gè)返回值一定是這個(gè)隊(duì)列中的一個(gè)元素。 注釋/*@ pure @*/ 表明peek()方法是一個(gè)純方法（pure method），純方法是指沒有副作用的方法。JML中只允許使用純方法進(jìn)行斷言確認(rèn)，所以我們把peek()聲明為純方法，這樣我們就可以在pop()方法的后置條件中使用peek()方法。大家肯定想知道，為什么JML只允許使用純方法進(jìn)行斷言確認(rèn)？問題是這樣的，如果JML允許使用非純方法進(jìn)行斷言確認(rèn)的話，我們稍不注意就會(huì)寫出有副作用的行為規(guī)范。比如說可能會(huì)有這么一種情況，開啟了斷言確認(rèn)以后，我們的代碼正確無誤，可是如果禁止了斷言確認(rèn)后，我們的代碼卻不能運(yùn)行了，或運(yùn)行出錯(cuò)了。這樣當(dāng)然不行！后面，我們還會(huì)進(jìn)一步討論副作用的問題。關(guān)于繼承 JML行為規(guī)范可以被子類（含子接口）或者是實(shí)現(xiàn)接口的類所繼承，這一點(diǎn)與J2SE1.4中斷言有所不同。JML關(guān)鍵字 also表示當(dāng)前定義的行為規(guī)范與祖先類或被實(shí)現(xiàn)的接口中所定義的行為規(guī)范一起作用。因而，在 PriorityQueue接口定義的 peek()方法的行為規(guī)范同樣適用于 BinaryHeap類中的 peek()方法。這個(gè)就意味著，雖然在 BinaryHeap.peek()的行為規(guī)范中沒有明確定義， BinaryHeap.peek()的返回值也必須在 elementsInQueue當(dāng)中。 大頂堆和小頂堆（譯者注：大頂堆和小頂堆是數(shù)據(jù)結(jié)構(gòu)里面的概念，分別表示堆排序方法的不同實(shí)現(xiàn)方式。堆排序是一種通過調(diào)整二叉樹進(jìn)行排序的方法。）上面我們給peek()定義的行為規(guī)范明顯缺少了一塊，那就是我們根本沒有要求它返回的那個(gè)元素具有最大的優(yōu)先級(jí)。顯然，JCCC的PriorityQueue接口既可以用于大頂堆，也可以用于小頂堆。大頂堆和小頂堆的表現(xiàn)是有些差別的，在小頂堆中優(yōu)先級(jí)最高的元素值最小，而大頂堆中優(yōu)先級(jí)最高的元素值最大。因?yàn)镻riorityQueue并不知道自己被用來進(jìn)行大頂堆排序還是小頂堆排序，所以指定返回哪個(gè)元素的規(guī)范必須在實(shí)現(xiàn)PriorityQueue接口的類中進(jìn)行定義。 在JCCC 中，類 BinaryHeap實(shí)現(xiàn)了PriorityQueue接口。BinaryHeap允許使用它的客戶代碼在構(gòu)造函數(shù)中通過一個(gè)參數(shù)來指定排序方案，也就是通過參數(shù)來指定是通過大頂堆方式排序還是通過小頂堆方式排序。我們使用一個(gè)boolean模型變量isMinimumHeap來判斷BinaryHeap的排序方式是大頂堆還是小頂堆。下面的例子是BinaryHeap使用isMinimumHeap給peek()方法定義的行為規(guī)范： 代碼段4 BinaryHeap 類中peek()方法的行為規(guī)范 /*@ @ 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中的后置條件包含兩個(gè)部分，分別用于大頂堆和小頂堆的情況。“==>符號(hào)的意思是包含（譯者注：這個(gè)包含與邏輯學(xué)中包含的意思一致）。x ==> y 當(dāng)且僅當(dāng)y為真或x為假時(shí)取真值。對(duì)于小頂堆排序來說，適用下面所列的代碼： (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方法的定義中使用了另外一個(gè)關(guān)鍵字model，它的意思是compareObjects方法是一個(gè)模型方法。模型方法是只能用在行為規(guī)范中的JML方法。模型方法定義在Java的注釋中，所以常規(guī)的Java代碼不能使用。 如果BinaryHeap類的客戶代碼指定了一個(gè)特殊的Comparator用來進(jìn)行比較的話，m_comparator就指向那個(gè)Comparator，否則m_comparator的值就是null。compareObjects()方法檢查m_comparator的值，然后采用適當(dāng)?shù)姆椒ㄟM(jìn)行元素間的比較。 模型域如何取值在代碼段4中我們討論了peek()方法的后置條件。這個(gè)條件保證peek()方法的返回值的優(yōu)先級(jí)大于或者等于模型域elementsInQueue中所有的元素的優(yōu)先級(jí)。那么有一個(gè)問題，像elementsInQueue這樣的模型域如何取值？前置條件、后置條件和不變量都是沒有副作用的，所以不能使用它們來設(shè)置模型域的值。 JML使用一個(gè)represents語句把模型域與具體的實(shí)現(xiàn)域關(guān)聯(lián)起來。比如下面的represents語句用來給模型域isMinimumHeap賦值： //@ private represents isMinimumHeap