OO第三次博客做業

OO第三單元總結

1、JML語言基礎

  JML(Java Modeling Language)是用於對Java程序進行規格化設計的一種表示語言。JML是一種行爲接口規格語言（Behavior Interface Specification Language，BISL），基於Larch方法構建。BISL提供了對方法和類型的規格定義手段。所謂接口即一個方法或類型外部可見的內容。近年來，JML持續受到關注，爲嚴格的程序設計提供了一套行之有效的方法。經過JML及其支持工具，不只能夠基於規格自動構造測試用例，並整合了SMT Solver等工具以靜態方式來檢查代碼實現對規格的知足狀況。

通常而言JML有2種主要用法：

（1）開展規格化設計。這樣交給代碼實現人員的將不是可能帶有內在模糊性的天然語言描述，而是邏輯嚴格的規格。

（2）針對已有的代碼實現，書寫其對應的規格，從而提升代碼的可維護性。這在遺留代碼的維護方面具備特別重要的意義。

一、JML表達式

1）原子表達式

\result表達式：表示一個非void 類型的方法執行所得到的結果，即方法執行後的返回值。

\old( expr )表達式：用來表示一個表達式expr 在相應方法執行前的取值。

\not_assigned(x,y,...)表達式：用來表示括號中的變量是否在方法執行過程當中被賦值。

\not_modified(x,y,...)表達式：與上面的\not_assigned表達式相似，該表達式限制括號中的變量在方法執行期間的取值未發生變化。

\type(type)表達式：返回類型type對應的類型(Class)，如type( boolean )爲Boolean.TYPE。

\typeof(expr)表達式：該表達式返回expr對應的準確類型。

2）量化表達式

\forall表達式：全稱量詞修飾的表達式，表示對於給定範圍內的元素，每一個元素都知足相應的約束。

\exists表達式：存在量詞修飾的表達式，表示對於給定範圍內的元素，存在某個元素知足相應的約束。

\sum表達式：返回給定範圍內的表達式的和。

\product表達式：返回給定範圍內的表達式的連乘結果。

\max表達式：返回給定範圍內的表達式的最大值。

\min表達式：返回給定範圍內的表達式的最小值。

\num_of表達式：返回指定變量中知足相應條件的取值個數。

3）集合表達式

集合構造表達式：能夠在JML規格中構造一個局部的集合（容器），明確集合中能夠包含的元素。例子：new JMLObjectSet {Integer i | s.contains(i) && 0 < i.intValue() } 表示構造一個JMLObjectSet對象，其中包含的元素類型爲Integer，該集合中的全部元素都在容器集合s中出現。

4）操做符

(1) 子類型關係操做符： E1<:E2 ，若是類型E1是類型E2的子類型(sub type)，則該表達式的結果爲真，不然爲假。

(2) 等價關係操做符： b_expr1<==>b_expr2 或者b_expr1<=!=>b_expr2 ，其中b_expr1和b_expr2都是布爾表達式，這兩個表達式的意思是b_expr1==b_expr2 或者b_expr1!=b_expr2 。

(3) 推理操做符： b_expr1==>b_expr2 或者b_expr2<==b_expr1 。

(4) 變量引用操做符：除了能夠直接引用Java代碼或者JML規格中定義的變量外，JML還提供了幾個歸納性的關鍵詞來引用相關的變量。

二、JML方法規格

前置條件(pre-condition): 前置條件經過requires子句來表示： requires P; 。其中requires是JML關鍵詞，表達的意思是「要求調用者確保P爲真」.

後置條件(post-condition): 後置條件經過ensures子句來表示： ensures P; 。其中ensures是JML關鍵詞，表達的意思是「方法實現者確保方法執行返回結果必定知足謂詞P的要求，即確保P爲真」.

反作用範圍限定(side-effects): 反作用指方法在執行過程當中會修改對象的屬性數據或者類的靜態成員數據，從而給後續方法的執行帶來影響。從方法規格的角度，必需要明確給出反作用範圍。JML提供了反作用約束子句，使用關鍵詞assignable 或者modifiable 。

signals子句: signals子句的結構爲signals (***Exception e) b_expr ，意思是當b_expr 爲true 時，方法會拋出括號中給出的相應異常e。

三、類型規格

不變式invariant: 不變式（invariant）是要求在全部可見狀態下都必須知足的特性，語法上定義invariant P ，其中invariant 爲關鍵詞， P 爲謂詞。

狀態變化約束constraint: 對象的狀態在變化時每每也許知足一些約束，這種約束本質上也是一種不變式。JML爲了簡化使用規則，規定invariant只針對可見狀態(即當下可見狀態)的取值進行約束，而是用constraint來對前序可見狀態和當前可見狀態的關係進行約束。

2、JML工具鏈

jml-launcher（圖形用戶界面工具的啓動器）。
jml和jml-gui（檢查器）。
jmlc和jmlc-gui（編譯用於運行時斷言檢查）。
jmldoc和jmldoc-gui（包含JML規範信息的javadoc版本）。
jmle（編譯用於執行或原型規範）。
jmlrac（java的一個版本，VM，包含CLASSPATH中的bin / jmlruntime.jar文件，用於運行使用jmlc編譯的文件）。
jmlre（java的一個版本，VM，包括執行規範所需的運行時支持，用於運行使用jmle編譯的文件）。
jmlspec和jmlspec-gui（從Java源文件生成框架規範文件）。
jmlunit和jmlunit-gui（生成用於JUnit的單元測試代碼存根）。
jtest（結合了jmlc和jmlunit的工做）
jml-junit（JUnit的swing用戶界面的一個版本，包括CLASSPATH中的bin / jmlruntime.jar和bin / jmljunitruntime.jar文件，用於對使用jmlc編譯的文件和jmlunit生成的測試用例運行基於JML和JUnit的測試）。

3、部署JML UnintNG

檢查方法以下圖所示：

編譯後文件目錄：

 

 最終生成測試結果：

 

4、做業架構設計

 

第一次做業

第一次做業整體上來講結構比較簡單。主要說說PathContainer的數據容器選擇。爲了最大限度地下降時間複雜度，個人PathContainer使用了2個HASHSET和3個HASHMAP。其中hashset主要負責判斷特定的ID和PATH是否存在於PATHCONTAINER。前2個HASHMAP負責實現PATH到ID的查詢以及ID到PATH的查詢。最後一個HASHMAP負責儲存DISTINCTCOUNT更新。在每一次增長和刪除時更新全部的HASH數據結構。以下圖所示：

類圖以下所示：

 

經典度量結果：

第一次BUG修復

因爲第一次做業總結上結構比較簡單，同時HASHMAP的運用使得複雜度不會超標。所以在中強互測階段都未發現BUG。

第二次做業

第二次做業在第一次做業的基礎上增長了邊的概念。同時增長了2個函數，判斷2點是否連通以及最短距離。我在第一次做業的數據結構上增長了2個HASHMAP。以下圖所示：

edgeset是關於邊的HASHMAP，key String的構成方法是點的數字經過空格相連，而Integer記錄它們中間相連的邊數

connectset記錄點和點的鏈接狀況。左側的Integer是點的名字，而右側的HASHMAP表示和它相連的點以及相連的邊數，採用兩種結構大體相同的HASHMAP的確比較佔用內存，但可以在個人架構中很大的減小編程複雜度。

因爲本次做業的邊都是無權邊，所以在計算最短路徑時採用BFS遍歷方法。遍歷到特定點的層數就是最短路徑長度。相較於迪傑斯特拉斯算法複雜度明顯下降，可是對第三次做業的擴展難度比較大，須要重構算法。

類圖：

 

經典度量分析：

能夠看到在計算最短路徑以及判斷連通這兩個函數的複雜度明顯太高，緣由是對BFS以及異常處理這兩個步驟沒有進行進一步細化，想經過一個函數徹底解決。徹底能夠經過將2者分離開來下降複雜度。

第二次BUG修復

第二次做業相較於第一次做業只增長了邊的部分。因爲採用HASHMAP和BFS，複雜度並不高，所以在中強測以及互測階段都沒有發現BUG。

第三次做業

我的理解第三次做業相較於第二次做業一共只增長了2個部分。第一是CONNECTBLOCK的計算，第二是有權圖的出現。UNPLEASANT VALUE，PRICE以及TRANSFER均可以經過不一樣的有權圖進行表示，在個人結構中經過3個HASHMAP進行了存儲。對於CONNECTBLOCK，我經過一個HASHSET數組進行解決。以上的數據結構都會在PATH增長和刪除時進行更新。

對於最少UNPLEASANT VALUE/PRICE/TRANSFER，因爲圖都有權重，所以不能使用BFS，只能經過迪傑斯特拉斯算法解決。同時因爲在遍歷的過程當中會先找到其它節點的最短距離，所以能夠經過特定數據結果將其緩存下來，在PATH數據更新時將全部緩存信息刪除。

對於不一樣PATH的相同點，我採用將相同點拆成多個不一樣點，根據UNPLEASANT VALUE，PRICE,TRANSFER不一樣狀況對邊的權重賦予不一樣的值。

類圖以下所示：

因爲數據結構增多須要增長相應的調用以及修改函數，致使PATHCONTAINER顯著增長。

在實現上採用繼承的方法。GRAPH繼承PATHCONTAINER，而RAILWAYSYSTEM繼承GRAPH。

OO經典度量：

 

複雜度較高的函數主要分爲2種。第一種是CONNECTBLOCK的更新函數，因爲狀況較多，而且須要對CONNECTBLOCK進行合併，所以複雜度較高。第二類是迪傑斯特拉斯算法，儘管已經將對緩存的更新和查詢拆分紅不一樣函數，可是因爲算法自己緣由，複雜度依然較高。

第三次做業BUG修復

第三次做業的BUG分爲2部分，包括TIE BUG以及常規錯誤。

常規錯誤：經過強測共發現2個常規錯誤。第一是對ARRAYLIST.REMOVE的使用錯誤。若是使用該函數移除最後一個元素以前的元素，會將ARRAYLIST次序從新排列，而我忘記考慮這種狀況，致使錯誤發生。

第二個常規錯誤是緩存的錯誤，因爲將不一樣PATH的相同點拆成不一樣的點，所以到一個PATH點的最短距離未必是到這個點的最短距離，可能離其餘PATH的同一個點距離更近。而我忘記了這種狀況，致使錯誤。

TLE錯誤：目前還未發現解決緣由。目前判斷有2種可能狀況：

1）沒有對第二次做業的函數進行緩存

2）拆點方法很差，太過直接暴力。若是相同點在不一樣路徑數較高，將致使整個圖的邊數很是高。

5、總結心得與體會

 

這3周的做業內容包括JML的理解和對於數據結構的從新測試。相較於具備二義性而且很是不夠準確的天然語言，JML經過邏輯方法在很大程度上提升了編程的嚴謹性，保證了程序的合理性以及準確性。

但另外一方面，JML因爲其過分嚴格的要求，反過來也會產生必定的問題。首先就是可讀性，對於一個很是複雜的程序，若是隻經過JML規定規格，那麼可讀性會很是差，使程序員難以理解，實質上變相地下降了程序的準確性。第二，JML在必定程度上語言過分嚴謹。例如JML若是規定使用數組，那麼若是使用ARRAYLIST，即便函數結構徹底正確,OPENJML也會瘋狂報錯。第三，當我打開百度搜索JML，能夠發現可供查考的資料很是少。實質上人們在大多數狀況下經過簡單的規格描述就能解決問題，而JML儘管很是嚴謹，可是在通常領域使用價值彷佛並不高。

我的對JML的理解還比較初步。在個人理解下，JML主要運用於驗證階段的使用。經過嚴謹的邏輯驗證可以在DEBUG階段作到足夠的嚴謹。同時能夠作到對天然語言的補充。在編程時若是同時天然語言規格描述以及JML規格描述能夠作到2者優點互補，最大限度提升編程效率。