JML起步--使用JML改進(jìn)你的Java程序(1)

2019-11-18 13:17:43

字體：大中小

供稿：網(wǎng)友

　　java建模語(yǔ)言（Java Modeling Language，JML）是一種進(jìn)行具體設(shè)計(jì)的符號(hào)語(yǔ)言，他鼓勵(lì)你用一種全新的方式來(lái)看待Java的類(lèi)和方法。本教程中，Java程序設(shè)計(jì)資深顧問(wèn)Joe Verzulli 將會(huì)給大家介紹這一新的工具以及如何使用這個(gè)工具。
　　
　　面向?qū)ο蟮姆治龊驮O(shè)計(jì)（OOAD）的一個(gè)重要原則就是過(guò)程性的思考應(yīng)該盡可能地推遲，不過(guò)遵循這個(gè)原則的大多數(shù)人也不過(guò)是把這個(gè)原則適用到方法實(shí)現(xiàn)這個(gè)級(jí)別上。一旦設(shè)計(jì)好了類(lèi)和接口，下面的事情自然就是實(shí)現(xiàn)其中定義的方法了。對(duì)呀，我們還能做什么呢？還有什么其它方法可以使用嗎？究竟，用Java進(jìn)行程序設(shè)計(jì)和用其他語(yǔ)言進(jìn)行程序設(shè)計(jì)一樣，我們都要一步一步地實(shí)現(xiàn)每一個(gè)方法。
　　
　　標(biāo)記本身只是表示如何做一個(gè)事情（how to do something），根本不管我們希望做什么。假如我們?cè)谧鲆粋€(gè)事情之前就能夠知道我們能夠達(dá)到什么樣的結(jié)果是非常好的，不過(guò)Java語(yǔ)言并沒(méi)有給我們提供一個(gè)可以顯示地把這些信息插入到我們程序代碼的方法。
　　
　　Java建模語(yǔ)言（Java Modeling Language，JML）在Java代碼中增加了一些符號(hào)，這些符號(hào)用來(lái)標(biāo)識(shí)一個(gè)方法是干什么的，卻并不關(guān)心它的實(shí)現(xiàn)。假如使用JML的話(huà)，我們就能夠描述一個(gè)方法的預(yù)期的功能而不管他如何實(shí)現(xiàn)。通過(guò)這種方式，JML把過(guò)程性的思考延遲到方法設(shè)計(jì)中，從而擴(kuò)展了面向?qū)ο笤O(shè)計(jì)的這個(gè)原則。
　　
　　JML引入了大量用于描述行為的結(jié)構(gòu)，比如有模型域、量詞、斷言可視范圍、預(yù)處理、后處理、條件繼續(xù)以及正常行為（與異常行為相對(duì)）規(guī)范等等。這些結(jié)構(gòu)使得JML非常強(qiáng)大，不過(guò)你并不必要理解或者使用上面所述的所有方面，也不需要一次使用所有的這些方面。你可以一點(diǎn)一點(diǎn)的學(xué)習(xí)，從非常簡(jiǎn)單的開(kāi)始。
　　
　　這篇文章中采用循序漸進(jìn)的方式來(lái)介紹JML。我們要先了解一下使用JML的各種好處，非凡是對(duì)開(kāi)發(fā)和編譯過(guò)程的影響。然后，我們要討論一下JML的一些結(jié)構(gòu)，比如前置條件、后置條件、模型域、量詞、副作用以及異常行為等等。同時(shí)，在討論這些結(jié)構(gòu)的同時(shí)，我們會(huì)給出一些例程來(lái)給你一個(gè)直觀的感覺(jué)。這樣經(jīng)過(guò)本文的學(xué)習(xí)，你將可以對(duì)JML是如何工作的有一個(gè)概念性的理解，從而能夠在你自己的項(xiàng)目中應(yīng)用JML。
　　
　　JML概覽
　　使用JML來(lái)聲明性地描述一個(gè)方法或類(lèi)的預(yù)期行為可以顯著提高整體的開(kāi)發(fā)進(jìn)程。把建模標(biāo)記加入到你的Java程序代碼中有以下好處：
　　
　　能夠更為精確地描述這些代碼是做什么的
　　能夠高效地發(fā)現(xiàn)和修正程序中的bug
　　可以在應(yīng)用程序升級(jí)時(shí)降低引入bug的機(jī)會(huì)
　　可以提早發(fā)現(xiàn)客戶(hù)代碼對(duì)類(lèi)的錯(cuò)誤使用
　　可以提供與應(yīng)用程序代碼完全一致的JML格式的文檔
　　JML標(biāo)記總是在Java注釋的內(nèi)部，所以對(duì)正常編譯的代碼沒(méi)有任何影響。假如你想比較一下普通的類(lèi)和使用了JML的類(lèi)有什么差別的話(huà)，你可以使用一個(gè)開(kāi)源的JML編譯器（請(qǐng)參考如下地址）。用JML編譯器編譯的代碼假如沒(méi)有實(shí)現(xiàn)JML規(guī)范所要求的事項(xiàng)，運(yùn)行時(shí)就會(huì)拋出一個(gè)JML異常。這個(gè)特性不僅可以幫助我們捕捉代碼中的bug，而且可以確保JML形式的文檔可以與程序代碼高度一致。
　　
　　文章下面的部分，我將使用開(kāi)放源代碼的Jakarta Commons Collection Component （JCCC）項(xiàng)目中的PRiorityQueue接口和BinaryHeap 類(lèi)來(lái)演示JML的各種性質(zhì)。在這里你可以找到使用了JML標(biāo)記完整的這個(gè)兩個(gè)文件。
　　
　　要求和責(zé)任
　　本文中使用的代碼（請(qǐng)參考如下地址）包括開(kāi)源項(xiàng)目JCCC中的PriorityQueue 接口。接口嘛，自然是聲明了一些方法的簽名，包括方法的參數(shù)類(lèi)型、返回值的類(lèi)型，并不涉及方法的實(shí)現(xiàn)。一般情況下或者只是按照J(rèn)ava語(yǔ)法要求的話(huà)，實(shí)現(xiàn)接口的類(lèi)只要實(shí)現(xiàn)了接口中定義的各個(gè)方法即可，不論實(shí)現(xiàn)的方式是多么地離奇古怪。我們并不想這樣，我們希望能夠確定一個(gè)行為規(guī)范，所有實(shí)現(xiàn)這個(gè)接口的類(lèi)都用我們指定的方式來(lái)實(shí)現(xiàn)這個(gè)接口中定義的方法。通過(guò)使用JML我們可以做到這一點(diǎn)。
　　
　　考慮一下PriorityQueue接口的pop()方法，對(duì)于優(yōu)先級(jí)隊(duì)列來(lái)說(shuō)，pop()方法應(yīng)該有什么樣的功能要求？最起碼應(yīng)該有三個(gè)：第一，假如要調(diào)用pop()方法，隊(duì)列中至少要有一個(gè)元素；第二，該方法應(yīng)該返回隊(duì)列中優(yōu)先級(jí)最高的那個(gè)元素；第三，該方法應(yīng)該從隊(duì)列中刪除返回的那個(gè)元素。
　　
　　下面代碼段顯示了表示滿(mǎn)足第一個(gè)要求的JML標(biāo)記：
　　
　　代碼段1　pop()方法功能規(guī)范的JML標(biāo)記
　　
　　/*@
　　
　　　 @　 public normal_behavior
　　
　　　 @　　 requires ! isEmpty();
　　
　　　 @*/
　　
　　Object pop() throws NoSUChElementException;
　　
　　前面已經(jīng)提到，JML標(biāo)記是寫(xiě)在Java代碼的注釋中的。包含JML標(biāo)記的多行注釋以/*@ 開(kāi)頭，JML忽略任何以@開(kāi)頭的空行。假如是單行的話(huà)，你也可以使用//@這種標(biāo)記。
　　
　　這里JML注釋中public要害字與Java中的public意思是一樣的，它表示程序中其他所有的類(lèi)都要遵循這個(gè)JML要求。Public要求只能應(yīng)用在public方法和public成員變量上。JML同樣有private-、 protected-、以及 package-級(jí)別的作用域。同樣，這些作用域的規(guī)則與Java語(yǔ)言中作用域的規(guī)則非常相似。
　　
　　這里normal_behavior要害字的意思是，這個(gè)JML要求表示這是一種正常情況，運(yùn)行時(shí)不會(huì)拋出異常。后面，我們會(huì)描述異常行為是怎么被界定的。
　　
　　前置條件和后置條件
　　JML要害字requires用來(lái)表示前置條件，前置條件表示調(diào)用一個(gè)方法前必須滿(mǎn)足的一些要求。上面代碼段中包含一個(gè)前置條件，它要求調(diào)用pop()方法的前提就是isEmpty()方法返回false，也就是說(shuō)要求這個(gè)隊(duì)列至少含有一個(gè)元素。
　　
　　一個(gè)方法的后置條件規(guī)范表示一個(gè)方法的責(zé)任，也就是說(shuō)當(dāng)這個(gè)方法返回時(shí)，它必須滿(mǎn)足這個(gè)后置條件的要求。在我們上面的例子中，pop()方法應(yīng)該返回隊(duì)列中優(yōu)先級(jí)最高的元素。我們希望指定一個(gè)后置條件要求JML在運(yùn)行時(shí)檢查是否滿(mǎn)足這個(gè)事實(shí)。要做到這一點(diǎn)，我們必須跟蹤所有添加到這個(gè)優(yōu)先級(jí)隊(duì)列中的元素，這樣我們就可以判定pop()方法應(yīng)該返回哪一個(gè)元素。怎么做呢？你可能會(huì)考慮在PriorityQueue接口中加入一個(gè)成員變量來(lái)存儲(chǔ)隊(duì)列中元素的值，不過(guò)這樣做有兩個(gè)問(wèn)題：
　　
　　PriorityQueue是一個(gè)接口，它可能有各種不同具體的實(shí)現(xiàn)方式，比如說(shuō)binary heap、Fibonacci heap或者calendar queue等等，它要與它的各種實(shí)現(xiàn)一致，況且JML標(biāo)記不應(yīng)該涉及到任何具體的實(shí)現(xiàn)細(xì)節(jié)。
　　作為一個(gè)接口，PriorityQueue只能擁有靜態(tài)成員變量。
　　為了處理這種情況，JML引入了一個(gè)叫做模型域（model fields）的概念。
　　
　　模型域
　　模型域類(lèi)似于成員變量，它只能被應(yīng)用到行為規(guī)范中。這是一個(gè)PriorityQueue中聲明模型域的例子：
　　
　　//@ public model instance JMLObjectBag elementsInQueue;
　　
　　這個(gè)聲明的意思是說(shuō)這里有一個(gè)叫做elementsInQueue的模型域，它的類(lèi)型是JMLObjectBag （這個(gè)數(shù)據(jù)類(lèi)型是在JML中定義的）。instance要害字表示雖然這個(gè)域是定義在接口中，可是任何實(shí)現(xiàn)這個(gè)接口的類(lèi)都擁有一個(gè)單獨(dú)的、非靜態(tài)的elementsInQueue域。與其他JML標(biāo)記一樣，這個(gè)聲明也是出現(xiàn)在注釋中的，所以常規(guī)的Java代碼是不能使用這個(gè)elementsInQueue變量的。在程序運(yùn)行的時(shí)候，是沒(méi)有任何對(duì)象擁有一個(gè)叫做elementsInQueue的成員變量的。
　　
　　行為規(guī)范與實(shí)現(xiàn)
　　使用一個(gè)包來(lái)存儲(chǔ)隊(duì)列中的元素，然后檢查每一個(gè)元素找出優(yōu)先級(jí)最高的那一個(gè)會(huì)讓人覺(jué)得效率不高。不過(guò)這只是行為規(guī)范的一部分，而不會(huì)涉及到實(shí)現(xiàn)。行為規(guī)范的作用在于描述 PriorityQueue的行為接口，也就是說(shuō)規(guī)定了使用 PriorityQueue的客戶(hù)代碼所能依靠的外部行為。
　　
　　PriorityQueue接口的各個(gè)具體實(shí)現(xiàn)只要可以滿(mǎn)足這個(gè)行為規(guī)范的要求，就可以使用任何更為高效的方法。比如說(shuō)，JCCC有一個(gè)實(shí)現(xiàn)這個(gè)接口的 BinaryHeap類(lèi)，它的實(shí)現(xiàn)方式就是使用一個(gè)存儲(chǔ)在數(shù)組中的 binary heap 。
　　
　　不過(guò)雖然用JML定義行為規(guī)范的時(shí)候不需要考慮執(zhí)行效率，程序運(yùn)行時(shí)JML斷言檢查卻是很重要的。所以開(kāi)啟斷言檢查時(shí)程序的運(yùn)行可能會(huì)有性能的壓力。
　　
　　elementsInQueue 存儲(chǔ)添加到優(yōu)先級(jí)隊(duì)列的元素的值，下面的代碼段顯示pop()方法如何使用elementsInQueue：
　　
　　代碼段2　在pop()的后置條件中使用模型域
　　
　　/*@
　　
　　　 @ public normal_behavior
　　
　　　 @　 requires ! isEmpty();
　　
　　　 @　 ensures
　　
　　　 @　　 elementsInQueue.equals(((JMLObjectBag)
　　
　　　 @　　　　　/old(elementsInQueue))
　　
　　　 @　　　　　　　　　　　　.remove(/result)) &&
　　
　　　 @　　 /result.equals(/old(peek()));
　　
　　　 @*/
　　
　　Object pop() throws NoSuchElementException;
　　
　　ensures要害字表示后面跟著的是pop()方法返回時(shí)必須滿(mǎn)足的后置條件。/result是一個(gè)JML要害字，它等于pop()方法的返回值。/old()是一個(gè)JML函數(shù)，它返回pop()方法調(diào)用之前參數(shù)的值。
　　
　　這個(gè)ensures語(yǔ)句包含了兩個(gè)后置條件。第一，pop()方法返回的那個(gè)元素必須要從elementsInQueue刪除。第二，這個(gè)返回值要與peek()方法返回的值一致。
　　
　　類(lèi)級(jí)別的不變量
　　我們現(xiàn)在已經(jīng)看到JML能夠讓我們規(guī)定方法的前置條件和后置條件，它同樣也答應(yīng)我們指定類(lèi)級(jí)別的不變量。類(lèi)級(jí)別的不變量指的是進(jìn)入和退出一個(gè)類(lèi)中每個(gè)方法都必須滿(mǎn)足的條件。比方說(shuō)吧，//@ public instance invariant elementsInQueue != null; 就是PriorityQueue的一個(gè)不變量，它的意思是任何實(shí)現(xiàn)PriorityQueue的類(lèi)一旦被實(shí)例化，elementsInQueue的值就不能是null。

上一篇：JML起步--使用JML改進(jìn)你的Java程序(2)

下一篇：jive中的abstract Factory