內(nèi)容: 來(lái)自:http://www-106.ibm.com/ 作者:Joe Verzulli 異常行為前面給出的行為規(guī)范要求調(diào)用peek() 和 pop()方法時(shí)隊(duì)列不能為空，但其實(shí)當(dāng)隊(duì)列空時(shí)是有可能會(huì)調(diào)用這兩個(gè)方法的。如果發(fā)生這種情況，這兩個(gè)方法就會(huì)拋出一個(gè)NoSuchElementException.異常。我們必須修正我們前面制定的行為規(guī)范，允許這種可能的發(fā)生。在這種情況下，我們要使用JML的exceptional_behavior語(yǔ)句。 到目前，我們的行為規(guī)范還是以public normal_behavior打頭的。這里normal_behavior關(guān)鍵字表示這是一個(gè)正常行為，方法不會(huì)拋出任何異常。使用public exceptional_behavior標(biāo)記可以用來(lái)描述拋出異常的行為。下面的代碼段顯示了類PriorityQueue中peek()方法的行為規(guī)范中的異常部分： 代碼段9 exceptional_behavior標(biāo)記 /*@ @ public normal_behavior @ requires ! isEmpty(); @ ensures elementsInQueue.has(result); @ also @ public exceptional_behavior @ requires isEmpty(); @ signals (Exception e) e instanceof NoSuchElementException; @*//*@ pure @*/ Object peek() throws NoSuchElementException; 像我們前面看到的所有例子一樣，這個(gè)規(guī)范的第一部分也是以public normal_behavior開(kāi)頭，表示正常行為；不同的是，這個(gè)規(guī)范還有第二部分，以public exceptional_behavior開(kāi)頭，描述了異常行為。與normal_behavior 語(yǔ)句一樣， exceptional_behavior 語(yǔ)句也有一個(gè) requires 語(yǔ)句。這個(gè)requires 語(yǔ)句表示當(dāng)拋出signals 語(yǔ)句中所列的異常時(shí)必須滿足的條件。在上面的例子中，如果isEmpty()方法返回真的話，peek()就會(huì)拋出一個(gè)NoSuchElementException異常。 signals 語(yǔ)句signals 語(yǔ)句是形如signals(E e) R的語(yǔ)句，其中E是Exception類本身或其一個(gè)子類，R是一個(gè)表達(dá)式。JML 用如下方式解釋一個(gè)signal 語(yǔ)句：如果有一個(gè)類型為E的異常拋出的話，就檢查是否為R真。如果是，就執(zhí)行既定規(guī)范；否則，拋出一個(gè)unchecked exception（譯者注：unchecked exception又叫做RuntimeException，關(guān)于這兩個(gè)概念，請(qǐng)參考Java語(yǔ)言中關(guān)于異常的描述），用以表示我們的程序代碼違背了exceptional_behavior規(guī)范的要求。 上面peek()方法中的signals語(yǔ)句的意思是如果隊(duì)列為空，就拋出一個(gè)NoSuchElementException異常。如果peek()方法在運(yùn)行中拋出不是NoSuchElementException的其它異常的話，那么JML就會(huì)把這當(dāng)成一個(gè)錯(cuò)誤，因?yàn)閑 instanceof NoSuchElementException不是true。如果你既想處理NoSuchElementException異常又想處理其它運(yùn)行期異常，我們可以修改上面的signals語(yǔ)句，改為signals (NoSuchElementException e) true; 。這個(gè)意思是說(shuō)，如果peek()方法拋出一個(gè)NoSuchElementException異常的話，那條件true必須為真，而true是一個(gè)常量，總是可以滿足條件，所以對(duì)于NoSuchElementException異常的處理可以正常進(jìn)行。不過(guò)我們這里并沒(méi)有提及關(guān)于其它異常的信息，而peek()方法可以拋出它的簽名（譯者注：方法的簽名是指，方法聲明的各個(gè)部分，具體來(lái)說(shuō)，是方法名稱、參數(shù)類型、返回類型和拋出異常的總稱）允許的任何異常。它的簽名說(shuō)它可以拋出NoSuchElementException異常，這就意味著它既可以拋出NoSuchElementException異常，又可以拋出RuntimeException。 如果隊(duì)列中存在一些元素而且當(dāng)我們調(diào)用peek()方法時(shí)還是拋出一個(gè)NoSuchElementException異常（或者其他異常），JML運(yùn)行期斷言檢查就會(huì)拋出一個(gè)unchecked exception，這表示正常的后置條件失敗。 結(jié)論本文簡(jiǎn)單介紹了JML的概念，說(shuō)明了它對(duì)面向?qū)ο笙到y(tǒng)的分析和設(shè)計(jì)的貢獻(xiàn)，通過(guò)實(shí)例演示了如何在Java程序中使用JML標(biāo)記。你可以從下面所列的資源中下載本文中所使用的完整的代碼，還可以從中找到更多的關(guān)于JML的信息。 你可以使用開(kāi)源的JML編譯器來(lái)編譯你含有JML標(biāo)記的代碼，所生成的類文件會(huì)在運(yùn)行時(shí)自動(dòng)檢查JML規(guī)范。如果你的程序沒(méi)有實(shí)現(xiàn)規(guī)范中規(guī)定的事情，JML就會(huì)拋出一個(gè)unchecked exception 來(lái)說(shuō)明你的程序違背了哪一條規(guī)范。這可以幫助我們捕獲程序中的bug，而且能保證我們的代碼與文檔（JML格式的文檔）高度一致。 JML運(yùn)行期斷言檢查編譯器是第一個(gè)JML工具，其他相關(guān)工具還有jmldoc和jmlunit等等。Jmldoc與javadoc工具相似，不同的是它在生成的HTML格式文檔中包含JML規(guī)范；jmlunit可以成生一個(gè)Java類文件測(cè)試的框架，它可以讓你很方便地使用JUnit工具測(cè)試含有JML標(biāo)記的Java代碼。你還可以從下面所列的資源中找到其他關(guān)于JML各個(gè)方面的相關(guān)內(nèi)容。 在此請(qǐng)?jiān)试S我向 Gary Leavens 和 Yoonsik Cheon表示深深的謝意，是他們幫我解決了一部分關(guān)于JML的疑問(wèn)并且審閱了你所看到的這篇文章。 資源 下載本文中所用的源代碼 。 Sourceforge是JML規(guī)范、開(kāi)源JML工具如JML編譯器、jmldoc、jmlunit以及相關(guān)信息的主頁(yè)。 PriorityQueue 接口和 BinaryHeap 類是開(kāi)源項(xiàng)目 雅加達(dá)通用集合組件（JCCC）的一部分。 Gary T. Leavens、Albert L. Baker和Clyde Ruby的 'JML設(shè)計(jì)起步' (愛(ài)荷華州立大學(xué)計(jì)算機(jī)科學(xué)系，2003年1月) 是對(duì)JML的更為詳細(xì)地介紹。 Bertrand Meyer在面向?qū)ο筌浖?gòu)造，第二版一書(shū)中關(guān)于通過(guò)契約（JML最基本的概念）進(jìn)行設(shè)計(jì)的討論(Prentice Hall, 1997)。 Granville Miller在介紹面向?qū)ο笙到y(tǒng)建模中關(guān)于 Java建模 部分（developerWorks, 2002）。 Eric Allen在'Diagnosing Java code: Assertions and temporal logic in Java programming' (developerWorks, July 2002)一書(shū)中討論了一些斷言檢查限制的問(wèn)題。 Kyle Brown在'A stepped approach to J2EE testing with SDAO' (developerWorks, March 2003)一文中討論了如何把模擬數(shù)據(jù)對(duì)象與分層測(cè)試聯(lián)合起來(lái)。 Java程序設(shè)計(jì)的各個(gè)方面的信息請(qǐng)參考IBM developerWorks Java專區(qū)。 Java, java, J2SE, j2se, J2EE, j2ee, J2ME, j2me, ejb, ejb3, JBOSS, jboss, spring, hibernate, jdo, struts, webwork, ajax, AJAX, mysql, MySQL, Oracle, Weblogic, Websphere, scjp, scjd