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

　　量詞（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 語句<符號右邊的代碼並進行求值
From:http://tw.wingwit.com/Article/program/Java/Javascript/201311/25275.html