異常行為 前面給出的行為規范要求調用peek() 和 pop()方法時隊列不能為空
但其實當隊列空時是有可能會調用這兩個方法的
如果發生這種情況
這兩個方法就會拋出一個NoSuchElementException
異常
我們必須修正我們前面制定的行為規范
允許這種可能的發生
在這種情況下
我們要使用JML的exceptional_behavior語句
到目前
我們的行為規范還是以public normal_behavior打頭的
這裡normal_behavior關鍵字表示這是一個正常行為
方法不會拋出任何異常
使用public exceptional_behavior標記可以用來描述拋出異常的行為
下面的代碼段顯示了類PriorityQueue中peek()方法的行為規范中的異常部分
代碼段
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的疑問並且審閱了你所看到的這篇文章
From:http://tw.wingwit.com/Article/program/Java/JSP/201311/19260.html
