如何使用JML改進(jìn)你的Java程序

小編給大家分享一下如何使用JML改進(jìn)你的Java程序，相信大部分人都還不怎么了解，因此分享這篇文章給大家參考一下，希望大家閱讀完這篇文章后大有收獲，下面讓我們一起去了解一下吧！

JML起步

XML:namespace prefix = o ns = "urn:schemas-microsoft-com:Office:office" /> 

使用JML 改進(jìn)你的Java程序

by Joe Verzulli (Mailto:joe55055@yahoo.com">joe55055@yahoo.com)

http://www-106.ibm.com/developerworks/java/library/j-jml.html

Java建模語言（Java Modeling Language，JML）是一種進(jìn)行詳細(xì)設(shè)計的符號語言，他鼓勵你用一種全新的方式來看待Java的類和方法。本教程中，Java程序設(shè)計資深顧問Joe Verzulli 將會給大家介紹這一新的工具以及如何使用這個工具。

面向?qū)ο蟮姆治龊驮O(shè)計（ooaD）的一個重要原則就是過程性的思考應(yīng)該盡可能地推遲，不過遵循這個原則的大多數(shù)人也不過是把這個原則適用到方法實現(xiàn)這個級別上。一旦設(shè)計好了類和接口，下面的事情自然就是實現(xiàn)其中定義的方法了。對呀，我們還能做什么呢？還有什么其它方法可以使用嗎？畢竟，用Java進(jìn)行程序設(shè)計和用其他語言進(jìn)行程序設(shè)計一樣，我們都要一步一步地實現(xiàn)每一個方法。

標(biāo)記本身只是表示如何做一個事情（how to do something），根本不管我們希望做什么。如果我們在做一個事情之前就能夠知道我們能夠達(dá)到什么樣的結(jié)果是非常好的，不過Java語言并沒有給我們提供一個可以顯示地把這些信息插入到我們程序代碼的方法。

Java建模語言（Java Modeling Language，JML）在Java代碼中增加了一些符號，這些符號用來標(biāo)識一個方法是干什么的，卻并不關(guān)心它的實現(xiàn)。如果使用JML的話，我們就能夠描述一個方法的預(yù)期的功能而不管他如何實現(xiàn)。通過這種方式，JML把過程性的思考延遲到方法設(shè)計中，從而擴(kuò)展了面向?qū)ο笤O(shè)計的這個原則。

JML引入了大量用于描述行為的結(jié)構(gòu)，比如有模型域、量詞、斷言可視范圍、預(yù)處理、后處理、條件繼承以及正常行為（與異常行為相對）規(guī)范等等。這些結(jié)構(gòu)使得JML非常強(qiáng)大，不過你并不必要理解或者使用上面所述的所有方面，也不需要一次使用所有的這些方面。你可以一點(diǎn)一點(diǎn)的學(xué)習(xí)，從非常簡單的開始。

這篇文章中采用循序漸進(jìn)的方式來介紹JML。我們要先了解一下使用JML的各種好處，特別是對開發(fā)和編譯過程的影響。然后，我們要討論一下JML的一些結(jié)構(gòu)，比如前置條件、后置條件、模型域、量詞、副作用以及異常行為等等。同時，在討論這些結(jié)構(gòu)的同時，我們會給出一些例程來給你一個直觀的感覺。這樣經(jīng)過本文的學(xué)習(xí)，你將可以對JML是如何工作的有一個概念性的理解，從而能夠在你自己的項目中應(yīng)用JML。

JML概覽

使用JML來聲明性地描述一個方法或類的預(yù)期行為可以顯著提高整體的開發(fā)進(jìn)程。把建模標(biāo)記加入到你的Java程序代碼中有以下好處：

• 能夠更為精確地描述這些代碼是做什么的

• 能夠高效地發(fā)現(xiàn)和修正程序中的bug

• 可以在應(yīng)用程序升級時降低引入bug的機(jī)會

• 可以提早發(fā)現(xiàn)客戶代碼對類的錯誤使用

• 可以提供與應(yīng)用程序代碼完全一致的JML格式的文檔

JML標(biāo)記總是在Java注釋的內(nèi)部，所以對正常編譯的代碼沒有任何影響。如果你想比較一下普通的類和使用了JML的類有什么差別的話，你可以使用一個開源的JML編譯器（請參考 sources">如下地址）。用JML編譯器編譯的代碼如果沒有實現(xiàn)JML規(guī)范所要求的事項，運(yùn)行時就會拋出一個JML異常。這個特性不僅可以幫助我們捕獲代碼中的bug，而且可以確保JML形式的文檔可以與程序代碼高度一致。

文章下面的部分，我將使用開放源代碼的Jakarta Commons Collection Component （JCCC）項目中的PriorityQueue接口和BinaryHeap 類來演示JML的各種性質(zhì)。在這里你可以找到使用了JML標(biāo)記完整的這個兩個文件。

要求和責(zé)任

本文中使用的代碼（請參考 如下地址）包括開源項目JCCC中的PriorityQueue 接口。接口嘛，自然是聲明了一些方法的簽名，包括方法的參數(shù)類型、返回值的類型，并不涉及方法的實現(xiàn)。一般情況下或者只是按照J(rèn)ava語法要求的話，實現(xiàn)接口的類只要實現(xiàn)了接口中定義的各個方法即可，不論實現(xiàn)的方式是多么地離奇古怪。我們并不想這樣，我們希望能夠確定一個行為規(guī)范，所有實現(xiàn)這個接口的類都用我們指定的方式來實現(xiàn)這個接口中定義的方法。通過使用JML我們可以做到這一點(diǎn)。

考慮一下PriorityQueue接口的pop()方法，對于優(yōu)先級隊列來說，pop()方法應(yīng)該有什么樣的功能要求？最起碼應(yīng)該有三個：第一，如果要調(diào)用pop()方法，隊列中至少要有一個元素；第二，該方法應(yīng)該返回隊列中優(yōu)先級最高的那個元素；第三，該方法應(yīng)該從隊列中刪除返回的那個元素。

下面代碼段顯示了表示滿足第一個要求的JML標(biāo)記：

代碼段1  pop()方法功能規(guī)范的JML標(biāo)記

/*@

  @  public normal_behavior

  @  requires ! isEmpty();

  @*/

object pop() throws NoSuchElementException;

前面已經(jīng)提到，JML標(biāo)記是寫在Java代碼的注釋中的。包含JML標(biāo)記的多行注釋以/*@ 開頭，JML忽略任何以@開頭的空行。如果是單行的話，你也可以使用//@這種標(biāo)記。

這里JML注釋中public關(guān)鍵字與Java中的public意思是一樣的，它表示程序中其他所有的類都要遵循這個JML要求。Public要求只能應(yīng)用在public方法和public成員變量上。JML同樣有private-、 protected-、 以及 package-級別的作用域。同樣，這些作用域的規(guī)則與Java語言中作用域的規(guī)則非常相似。

這里normal_behavior關(guān)鍵字的意思是，這個JML要求表示這是一種正常情況，運(yùn)行時不會拋出異常。后面，我們會描述異常行為是怎么被界定的。

前置條件和后置條件

JML關(guān)鍵字requires用來表示前置條件，前置條件表示調(diào)用一個方法前必須滿足的一些要求。上面代碼段中包含一個前置條件，它要求調(diào)用pop()方法的前提就是isEmpty()方法返回false，也就是說要求這個隊列至少含有一個元素。

一個方法的后置條件規(guī)范表示一個方法的責(zé)任，也就是說當(dāng)這個方法返回時，它必須滿足這個后置條件的要求。在我們上面的例子中，pop()方法應(yīng)該返回隊列中優(yōu)先級最高的元素。我們希望指定一個后置條件要求JML在運(yùn)行時檢查是否滿足這個事實。要做到這一點(diǎn)，我們必須跟蹤所有添加到這個優(yōu)先級隊列中的元素，這樣我們就可以判斷pop()方法應(yīng)該返回哪一個元素。怎么做呢？你可能會考慮在PriorityQueue接口中加入一個成員變量來存儲隊列中元素的值，不過這樣做有兩個問題：

• PriorityQueue是一個接口，它可能有各種不同具體的實現(xiàn)方式，比如說binary heap、Fibonacci heap或者calendar queue等等，它要與它的各種實現(xiàn)一致，況且JML標(biāo)記不應(yīng)該涉及到任何具體的實現(xiàn)細(xì)節(jié)。

• 作為一個接口，PriorityQueue只能擁有靜態(tài)成員變量。

為了處理這種情況，JML引入了一個叫做模型域（model fields）的概念。

模型域

模型域類似于成員變量，它只能被應(yīng)用到行為規(guī)范中。這是一個PriorityQueue中聲明模型域的例子：

//@ public model instance JMLObjectBag elementsInQueue;

這個聲明的意思是說這里有一個叫做elementsInQueue的模型域，它的類型是JMLObjectBag （這個數(shù)據(jù)類型是在JML中定義的）。instance關(guān)鍵字表示雖然這個域是定義在接口中，可是任何實現(xiàn)這個接口的類都擁有一個單獨(dú)的、非靜態(tài)的elementsInQueue域。與其他JML標(biāo)記一樣，這個聲明也是出現(xiàn)在注釋中的，所以常規(guī)的Java代碼是不能使用這個elementsInQueue變量的。在程序運(yùn)行的時候，是沒有任何對象擁有一個叫做elementsInQueue的成員變量的。

行為規(guī)范與實現(xiàn)

使用一個包來存儲隊列中的元素，然后檢查每一個元素找出優(yōu)先級最高的那一個會讓人覺得效率不高。不過這只是行為規(guī)范的一部分，而不會涉及到實現(xiàn)。行為規(guī)范的作用在于描述 PriorityQueue的行為接口，也就是說規(guī)定了使用 PriorityQueue的客戶代碼所能依賴的外部行為。

PriorityQueue接口的各個具體實現(xiàn)只要可以滿足這個行為規(guī)范的要求，就可以使用任何更為高效的方法。比如說，JCCC有一個實現(xiàn)這個接口的 BinaryHeap類，它的實現(xiàn)方式就是使用一個存儲在數(shù)組中的 binary heap 。

不過雖然用JML定義行為規(guī)范的時候不需要考慮執(zhí)行效率，程序運(yùn)行時JML斷言檢查卻是很重要的。所以開啟斷言檢查時程序的運(yùn)行可能會有性能的壓力。

elementsInQueue 存儲添加到優(yōu)先級隊列的元素的值，下面的代碼段顯示pop()方法如何使用elementsInQueue：

代碼段2  在pop()的后置條件中使用模型域

/*@

  @ public normal_behavior

  @  requires ! isEmpty();

  @  ensures

  @  elementsInQueue.equals(((JMLObjectBag)

  @  old(elementsInQueue))

  @  .remove(esult)) &&

  @  esult.equals(old(peek()));

  @*/

Object pop() throws NoSuchElementException;

ensures關(guān)鍵字表示后面跟著的是pop()方法返回時必須滿足的后置條件。esult是一個JML關(guān)鍵字，它等于pop()方法的返回值。old()是一個JML函數(shù)，它返回pop()方法調(diào)用之前參數(shù)的值。

這個ensures語句包含了兩個后置條件。第一，pop()方法返回的那個元素必須要從elementsInQueue刪除。第二，這個返回值要與peek()方法返回的值一致。

類級別的不變量

我們現(xiàn)在已經(jīng)看到JML能夠讓我們規(guī)定方法的前置條件和后置條件，它同樣也允許我們指定類級別的不變量。類級別的不變量指的是進(jìn)入和退出一個類中每個方法都必須滿足的條件。比方說吧，//@ public instance invariant elementsInQueue != null; 就是PriorityQueue的一個不變量，它的意思是任何實現(xiàn)PriorityQueue的類一旦被實例化，elementsInQueue的值就不能是null。

以上是“如何使用JML改進(jìn)你的Java程序”這篇文章的所有內(nèi)容，感謝各位的閱讀！相信大家都有了一定的了解，希望分享的內(nèi)容對大家有所幫助，如果還想學(xué)習(xí)更多知識，歡迎關(guān)注億速云行業(yè)資訊頻道！