使用JML改進Java程序之量詞的示例分析

小編給大家分享一下使用JML改進Java程序之量詞的示例分析，相信大部分人都還不怎么了解，因此分享這篇文章給大家參考一下，希望大家閱讀完這篇文章后大有收獲，下面讓我們一起去了解一下吧！

專注于為中小企業(yè)提供成都網(wǎng)站設(shè)計、成都網(wǎng)站制作服務(wù),電腦端+手機端+微信端的三站合一,更高效的管理,為中小企業(yè)古浪免費做網(wǎng)站提供優(yōu)質(zhì)的服務(wù)。我們立足成都，凝聚了一批互聯(lián)網(wǎng)行業(yè)人才，有力地推動了數(shù)千家企業(yè)的穩(wěn)健成長，幫助中小企業(yè)通過網(wǎng)站建設(shè)實現(xiàn)規(guī)模擴充和轉(zhuǎn)變。

量詞（Quantification）（譯者注：這里量詞的意思與邏輯學(xué)上的量詞意思相近，而不是普通意義上理解的量詞。）XML:namespace prefix = o ns = "urn:schemas-microsoft-com:Office:office" />

在上面pop()方法的行為規(guī)范中，我們說它的返回值要等于peek()方法的返回值，不過我們并沒有看到關(guān)于peek()方法的規(guī)范。PriorityQueue中peek()方法的行為規(guī)范請看下面的代碼：

代碼段3  PriorityQueue中peek()方法的行為規(guī)范

/*@

  @ public normal_behavior

  @  requires ! isEmpty();

  @  ensures elementsInQueue.has(esult);

  @*/

/*@ pure @*/ object peek() throws NoSuchElementException;

JML標記要求只有當(dāng)隊列中至少含有一個元素的時候，才能調(diào)用peek()方法，同時他還要求方法的返回值必須在elementsInQueue之內(nèi)，也就是說，這個返回值一定是這個隊列中的一個元素。

注釋/*@ pure @*/ 表明peek()方法是一個純方法（pure method），純方法是指沒有副作用的方法。JML中只允許使用純方法進行斷言確認，所以我們把peek()聲明為純方法，這樣我們就可以在pop()方法的后置條件中使用peek()方法。大家肯定想知道，為什么JML只允許使用純方法進行斷言確認？問題是這樣的，如果JML允許使用非純方法進行斷言確認的話，我們稍不注意就會寫出有副作用的行為規(guī)范。比如說可能會有這么一種情況，開啟了斷言確認以后，我們的代碼正確無誤，可是如果禁止了斷言確認后，我們的代碼卻不能運行了，或運行出錯了。這樣當(dāng)然不行！后面，我們還會進一步討論副作用的問題。

關(guān)于繼承

JML行為規(guī)范可以被子類（含子接口）或者是實現(xiàn)接口的類所繼承，這一點與j2se1.4中斷言有所不同。JML關(guān)鍵字 also表示當(dāng)前定義的行為規(guī)范與祖先類或被實現(xiàn)的接口中所定義的行為規(guī)范一起作用。因而，在 PriorityQueue接口定義的 peek()方法的行為規(guī)范同樣適用于 BinaryHeap類中的 peek()方法。這個就意味著，雖然在 BinaryHeap.peek()的行為規(guī)范中沒有明確定義， BinaryHeap.peek()的返回值也必須在 elementsInQueue當(dāng)中。

大頂堆和小頂堆（譯者注：大頂堆和小頂堆是數(shù)據(jù)結(jié)構(gòu)里面的概念，分別表示堆排序方法的不同實現(xiàn)方式。堆排序是一種通過調(diào)整二叉樹進行排序的方法。）

上面我們給peek()定義的行為規(guī)范明顯缺少了一塊，那就是我們根本沒有要求它返回的那個元素具有最大的優(yōu)先級。顯然，JCCC的PriorityQueue接口既可以用于大頂堆，也可以用于小頂堆。大頂堆和小頂堆的表現(xiàn)是有些差別的，在小頂堆中優(yōu)先級最高的元素值最小，而大頂堆中優(yōu)先級最高的元素值最大。因為PriorityQueue并不知道自己被用來進行大頂堆排序還是小頂堆排序，所以指定返回哪個元素的規(guī)范必須在實現(xiàn)PriorityQueue接口的類中進行定義。

在JCCC 中，類 BinaryHeap實現(xiàn)了PriorityQueue接口。BinaryHeap允許使用它的客戶代碼在構(gòu)造函數(shù)中通過一個參數(shù)來指定排序方案，也就是通過參數(shù)來指定是通過大頂堆方式排序還是通過小頂堆方式排序。我們使用一個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(esult, obj)

  @  <= 0)) &&

  @  ((! isMinimumHeap) ==>

  @  (forall Object obj;

  @  elementsInQueue.has(obj);

  @  compareObjects(esult, obj)

  @  >= 0));

  @*/

public Object peek() throws NoSuchElementException

使用量詞

上面代碼段4中的后置條件包含兩個部分，分別用于大頂堆和小頂堆的情況。“==>”符號的意思是包含（譯者注：這個包含與邏輯學(xué)中包含的意思一致）。x ==> y 當(dāng)且僅當(dāng)y為真或x為假時取真值。對于小頂堆排序來說，適用下面所列的代碼：

(forall Object obj;

  elementsInQueue.has(obj);

  compareObjects(esult, obj) <= 0)

上面的代碼中forall是一個JML量詞。上面forall表達式當(dāng)所有的對象obj滿足elementsInQueue.has(obj)為真且compareObjects(esult, obj)返回一個非正數(shù)兩個條件時才為真。換言之，當(dāng)使用compareObjects()進行比較時，peek()方法的返回值一定小于或等于elementsInQueue中每一個元素的值。其他的JML量詞還有exists、sum以及 min等等。

使用Comparator進行比較

BinaryHeap類允許以兩種方法比較元素的大小。一種方法是要進行比較的元素自己實現(xiàn)Comparable接口，比較過程使用元素中定義的方法進行。另外一種方法是客戶類在構(gòu)造BinaryHeap類的實例時向構(gòu)造函數(shù)傳入一個Comparator對象，使用該Comparator對象進行比較。無論使用哪一種比較方式，我們都使用模型域comparator來表示比較大小所用的Comparator對象。 在peek()方法的后置條件中，compareObjects()方法使用客戶端選擇的比較方式來進行元素的比較。compareObjects()方法定義如下：

代碼段5  compareObjects()方法

/*@

  @ public normal_behavior

  @  ensures

  @  (comparator == null) ==>

  @  (esult == ((Comparable) a).compareTo(b)) &&

  @  (comparator != null) ==>

  @  (esult == 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方法的定義中使用了另外一個關(guān)鍵字model，它的意思是compareObjects方法是一個模型方法。模型方法是只能用在行為規(guī)范中的JML方法。模型方法定義在Java的注釋中，所以常規(guī)的Java代碼不能使用。

如果BinaryHeap類的客戶代碼指定了一個特殊的Comparator用來進行比較的話，m_comparator就指向那個Comparator，否則m_comparator的值就是null。compareObjects()方法檢查m_comparator的值，然后采用適當(dāng)?shù)姆椒ㄟM行元素間的比較。

模型域如何取值

在代碼段4中我們討論了peek()方法的后置條件。這個條件保證peek()方法的返回值的優(yōu)先級大于或者等于模型域elementsInQueue中所有的元素的優(yōu)先級。那么有一個問題，像elementsInQueue這樣的模型域如何取值？前置條件、后置條件和不變量都是沒有副作用的，所以不能使用它們來設(shè)置模型域的值。

JML使用一個represents語句把模型域與具體的實現(xiàn)域關(guān)聯(lián)起來。比如下面的represents語句用來給模型域isMinimumHeap賦值：

//@ private represents isMinimumHeap <- m_isMinHeap;

這個語句的意思是模型域isMinimumHeap的值等于m_isMinHeap的值，其中，m_isMinHeap是BinaryHeap類中一個私有的布爾變量。 一旦需要用到isMinimumHeap的值，JML就會把m_isMinHeap的值賦給它。

represents語句并沒有限制<-右邊必須是成員變量。比如說，下面是elementsInQueue的represents語句：

代碼段6  elementsInQueue的represents語句

/*@ private represents elementsInQueue

  @  <- JMLObjectBag.convertFrom(

  @  Arrays.asList(m_elements)

  @  .subList(1, m_size + 1));

  @*/

從這里我們可以看出，elementsInQueue的元素就是數(shù)組m_elements[]從第一個元素到第m_size個元素共m_size個元素構(gòu)成的列表，其中數(shù)組m_elements[]是BinaryHeap的一個私有成員，用來存儲優(yōu)先級隊列中的元素，m_size是m_elements[]中正在使用的元素的個數(shù)。類BinaryHeap沒有使用m_elements[0]，這樣可以簡化對于索引的操作。JMLObjectBag.convertFrom()的作用是把一個List結(jié)構(gòu)轉(zhuǎn)化為一個elementsInQueue所需要的JMLObjectBag結(jié)構(gòu)。這樣一旦JML運行時進行斷言檢查的時候需要elementsInQueue的值，系統(tǒng)就會計算represents 語句<-符號右邊的代碼并進行求值。

以上是“使用JML改進Java程序之量詞的示例分析”這篇文章的所有內(nèi)容，感謝各位的閱讀！相信大家都有了一定的了解，希望分享的內(nèi)容對大家有所幫助，如果還想學(xué)習(xí)更多知識，歡迎關(guān)注創(chuàng)新互聯(lián)行業(yè)資訊頻道！

網(wǎng)頁題目：使用JML改進Java程序之量詞的示例分析
網(wǎng)站路徑：http://muchs.cn/article14/pgddge.html

成都網(wǎng)站建設(shè)公司_創(chuàng)新互聯(lián)，為您提供域名注冊、商城網(wǎng)站、網(wǎng)頁設(shè)計公司、網(wǎng)站收錄、網(wǎng)站改版、外貿(mào)建站

廣告

聲明：本網(wǎng)站發(fā)布的內(nèi)容（圖片、視頻和文字）以用戶投稿、用戶轉(zhuǎn)載內(nèi)容為主，如果涉及侵權(quán)請盡快告知，我們將會在第一時間刪除。文章觀點不代表本網(wǎng)站立場，如需處理請聯(lián)系客服。電話：028-86922220；郵箱：631063699@qq.com。內(nèi)容未經(jīng)允許不得轉(zhuǎn)載，或轉(zhuǎn)載時需注明來源： 創(chuàng)新互聯(lián)