熱點推薦:
您现在的位置: 電腦知識網 >> 編程 >> Java編程 >> JSP教程 >> 正文

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

2013-11-15 11:35:34  來源: JSP教程 

  異常行為
  前面給出的行為規范要求調用peek() 和 pop()方法時隊列不能為空但其實當隊列空時是有可能會調用這兩個方法的如果發生這種情況這兩個方法就會拋出一個NoSuchElementException異常我們必須修正我們前面制定的行為規范允許這種可能的發生在這種情況下我們要使用JML的exceptional_behavior語句
  
  到目前我們的行為規范還是以public normal_behavior打頭的這裡normal_behavior關鍵字表示這是一個正常行為方法不會拋出任何異常使用public exceptional_behavior標記可以用來描述拋出異常的行為下面的代碼段顯示了類PriorityQueue中peek()方法的行為規范中的異常部分
  
  代碼段  exceptional_behavior標記
  
  /*@
  
    @ public normal_behavior
  
    @  requires ! isEmpty();
  
    @  ensures elementsInQueuehas(\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
    推薦文章
    Copyright © 2005-2013 電腦知識網 Computer Knowledge   All rights reserved.