JML起步--使用JML 改進你的Java程序(2)

2019-11-18 14:02:49

字體：大中小

來源：轉載

供稿：網友

　　來自: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(

上一篇：Jive中的設計模式

下一篇：Jini能給您帶來什么