JML起步--使用JML改進你的Java程序(4)

2019-11-18 13:17:47

字體：大中小

來源：轉載

供稿：網友

　　異常行為
　　前面給出的行為規范要求調用peek() 和 pop()方法時隊列不能為空，但其實當隊列空時是有可能會調用這兩個方法的。假如發生這種情況，這兩個方法就會拋出一個NoSUChElementException.異常。我們必須修正我們前面制定的行為規范，答應這種可能的發生。在這種情況下，我們要使用JML的exceptional_behavior語句。
　　
　　到目前，我們的行為規范還是以public normal_behavior打頭的。這里normal_behavior要害字表示這是一個正常行為，方法不會拋出任何異常。使用public exceptional_behavior標記可以用來描述拋出異常的行為。下面的代碼段顯示了類PRiorityQueue中peek()方法的行為規范中的異常部分：
　　
　　代碼段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;
　　
　　像我們前面看到的所有例子一樣，這個規范的第一部分也是以public normal_behavior開頭，表示正常行為；不同的是，這個規范還有第二部分，以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真。假如是，就執行既定規范；否則，拋出一個unchecked exception（譯者注：unchecked exception又叫做RuntimeException，關于這兩個概念，請參考java語言中關于異常的描述），用以表示我們的程序代碼違反了exceptional_behavior規范的要求。
　　
　　上面peek()方法中的signals語句的意思是假如隊列為空，就拋出一個NoSuchElementException異常。假如peek()方法在運行中拋出不是NoSuchElementException的其它異常的話，那么JML就會把這當成一個錯誤，因為e instanceof NoSuchElementException不是true。假如你既想處理NoSuchElementException異常又想處理其它運行期異常，我們可以修改上面的signals語句，改為signals (NoSuchElementException e) true; 。這個意思是說，假如peek()方法拋出一個NoSuchElementException異常的話，那條件true必須為真，而true是一個常量，總是可以滿足條件，所以對于NoSuchElementException異常的處理可以正常進行。不過我們這里并沒有提及關于其它異常的信息，而peek()方法可以拋出它的簽名（譯者注：方法的簽名是指，方法聲明的各個部分，具體來說，是方法名稱、參數類型、返回類型和拋出異常的總稱）答應的任何異常。它的簽名說它可以拋出NoSuchElementException異常，這就意味著它既可以拋出NoSuchElementException異常，又可以拋出RuntimeException。
　　
　　假如隊列中存在一些元素而且當我們調用peek()方法時還是拋出一個NoSuchElementException異常（或者其他異常），JML運行期斷言檢查就會拋出一個unchecked exception，這表示正常的后置條件失敗。
　　
　　結論
　　本文簡單介紹了JML的概念，說明了它對面向對象系統的分析和設計的貢獻，通過實例演示了如何在Java程序中使用JML標記。你可以從下面所列的資源中下載本文中所使用的完整的代碼，還可以從中找到更多的關于JML的信息。
　　
　　你可以使用開源的JML編譯器來編譯你含有JML標記的代碼，所生成的類文件會在運行時自動檢查JML規范。假如你的程序沒有實現規范中規定的事情，JML就會拋出一個unchecked exception 來說明你的程序違反了哪一條規范。這可以幫助我們捕捉程序中的bug，而且能保證我們的代碼與文檔（JML格式的文檔）高度一致。
　　
　　JML運行期斷言檢查編譯器是第一個JML工具，其他相關工具還有jmldoc和jmlunit等等。Jmldoc與javadoc工具相似，不同的是它在生成的Html格式文檔中包含JML規范；jmlunit可以成生一個Java類文件測試的框架，它可以讓你很方便地使用JUnit工具測試含有JML標記的Java代碼。你還可以從下面所列的資源中找到其他關于JML各個方面的相關內容。
　　
　　在此請答應我向 Gary Leavens 和 Yoonsik Cheon表示深深的謝意，是他們幫我解決了一部分關于JML的疑問并且審閱了你所看到的這篇文章。

上一篇：jive中的abstract Factory

下一篇：JML起步--使用JML改進你的Java程序(3)