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