OO第三次博客做業（第三單元總結）

(1)梳理JML語言的理論基礎、應用工具鏈狀況

Java 建模語言(JML)將註釋添加到 Java 代碼中，這樣咱們就能夠肯定方法所執行的內容，而沒必要說明它們如何作到這一點。有了 JML，咱們就能夠描述方法預期的功能，無需考慮實現。經過這種方法，JML 將延遲過程設想的面向對象原則擴展到了方法設計階段。

JML的核心包括如下三個部分：

前置條件：requires

後置條件：ensures

反作用：assignable/modifiable

同時它也可以對程序的各類執行條件進行劃分：normal_behavior/expectional_behavior

因爲JML具備規範性，因此能夠用JMLUnitNG/JMLUnit等工具生成測試用例，對相應的程序進行自動化測試。固然測試的正確性是有前提的：JML規格必須得寫對了。

(2)【改成選作，能較爲完善地完成的將酌情加分】部署SMT Solver，至少選擇3個主要方法來嘗試進行驗證，報告結果

這部分先跳過吧。

(3)部署JMLUnitNG/JMLUnit，針對Graph接口的實現自動生成測試用例

 在本身的電腦上根本無法部署。因爲某個我不知道的緣由，這個學期個人cmd上一直無法跑java，不管怎麼改環境變量都無論用，連個

java -version

都識別不了，別說openJML，連上學期的logisim和Mars都跑不了。

這一部分暫時先咕掉，看看有沒有什麼其餘的解決辦法。

(4)按照做業梳理本身的架構設計，並特別分析迭代中對架構的重構

我的以爲此次做業不須要怎麼畫UML圖了，由於實現的接口都是定死了的。整個單元做業的精髓在於各類實現方法的選擇，包括但不限於數據結構（容器）、算法。

 

第一次做業開始，我就採用了討論區裏所一致推崇的雙向HashMap存儲點數關係的方法，這個方法在第一次做業中主要針對DISTINCT_NODE_COUNT指令，而從整單元做業來看，這個方法爲本單元以後的兩次做業打下了良好的基礎。

在第一次做業中，我直接採用數組來做爲Path的保存容器，後來簡單起見改爲了ArrayList。

 

第二次做業開始涉及圖結構，對圖結構的保存，我採用了可能稍微特別的方法：在上次做業保存的點集基礎上，新增一個HashMap來保存邊集，而遇到最短路徑的計算時，再將點集和邊集轉化爲鄰接矩陣，運用DIjkstra算法求最短距離（如今想一想這個轉換是否有必要有待商榷），每跑一次Dijkstra算法能夠算出n組點之間的最短距離，而後再用一個HashMap保存起來，用這種滾雪球的方法對抗時間複雜度。若是遇到增刪，則在下次求最短距離時要把最短路徑HashMap，鄰接矩陣等內容進行更新（懶漢思想，不用就放着無論）。

 

第三次做業變成帶權圖，而且涉及換乘點的處理，複雜度進一步提高，牽扯到算法的選擇。想到的第一種方法是，拆開每一個換乘點，在換乘點間創建虛路徑，對這些虛路徑和實際存在的路徑按要求賦相應的權值，完成各類不一樣的要求。但這樣就涉及到了一個很要命的問題：極端狀況下，換乘點能夠高度重合（最極端的狀況是全部路徑所有重合，每一個點都是換乘點，每一個換乘點均可以換乘全部路線），這樣的話圖的點數就會爆炸，按普通Dijkstra算法的時間複雜度（O(n^2)，n爲點數）確定是不行的，儘管能夠作堆優化把複雜度降到O(mlogm)（m爲邊數），但一個現實問題是：沒找到Java版的堆優化代碼，現有的C++版代碼又看的不是很懂，並且大多數採用的是鄰接表存儲，這意味着可能要對程序的圖存儲結構進行較大調整，怎麼給每條線路拆分出一個換乘點並以合適方式進行表示也是個問題。

因此最後我採用了另外一種方式，在各條路徑內部計算出路徑上兩點之間的各類最小值，包括換乘次數（其實沒有這個，由於恆爲0），票價（其實就是最短距離），不滿意度並存儲，並存入圖中，而後在矩陣初始化時用兩點間最小值加上換乘相關的權值（好比最小換乘就是1，最低票價是2，最小不滿意度是32），在跑完Dijkstra算法後在減去相應值，就能求出最後的結果。相比上一種作法，複雜度來源主要在於路徑內部又跑了一遍Dijkstra，但因爲一條路徑上就那麼些點，因此效率還能夠，不過確定不如第一種算法。（說白了由於菜寫不出來好的實現，我寫代碼像cxk.gif）

(5)按照做業分析代碼實現的bug和修復狀況

第一次做業：最開始的反向HashMap採用的不是Path映射PathId，而是Path的Hash值映射PathId，這就致使了存在Hash值重複的狀況，雖然過了強測但互測被Hack一次。後來利用instanceof關鍵詞重寫了equals方法消除了Bug，也爲後兩次做業打下了正確的基礎。

第二次做業：沒Bug，表現不錯。

第三次做業：災難。因爲對兩條路徑糾纏在一塊兒的狀況沒有考慮到，致使初始化的時候出現問題（正常應該存兩點間最小值，但我忽略了這種狀況，按兩點間只有一個值寫的代碼，致使這個值被錯誤刷新），另外還有一處明顯的手誤沒看出來，在中測一遍過的狀況下，強測10分，互測被Hack19次。但Bug越多，每每也意外着錯誤越明顯、越簡單，總共37個Bug被一次性修復，也算是一個尷尬的紀錄了。

(6)闡述對規格撰寫和理解上的心得體會

在寫此次做業以前，我看到有人的做業中提出JML比較適合大型程序的結構描述，但我並不這麼認爲，由於從這幾回的做業和課上實驗來看，每次給出的JML規格都存在或多或少的錯誤，這就說明了一個問題：用JML語言準確描述代碼要作什麼，並非一件容易的事情，代碼越複雜，描述起來的難度就越大。具體到做業中，JML代碼描述一些規模較小、功能較簡單的方法仍是比較容易的，但描述一些功能複雜、規模較大的方法則顯得力不從心，好比最後一次做業中實現的Graph類中幾個查找函數，與其從冗長且可能存在Bug的JML描述中進行對照，不如直接從指導書get到函數的實現要點。

再者說，JML的一個好處是沒有限制實現方式，但這種沒有限制實現方式的狀況在實際的工業生產與大型程序設計中並很少見。以咱們親愛的OS實驗課爲例（固然OS確定不會用Java寫，這裏僅僅作一個假設），在OS的課程中，每一個函數之間的調用關係都很是緊密和複雜，JML代碼能不能寫對都是問題，即便寫對了，在函數體內部，每一個函數所執行的流程都很是固定，很難有自由發揮的空間，這種狀況下，寫一份JML描述幾乎和寫出程序代碼無異！好比下面的函數，我想不出若是用JML能描述出什麼花樣來，更想不出寫出的JML和程序代碼能有多大區別：

15 u_int
16 diskaddr(u_int blockno)
17 {
18 if ( super && blockno > (super->s_nblocks)) {
19 user_panic("diskaddr failed!");
20 }
21 return DISKMAP+blockno*BY2BLK;
22 }

JML能勝任的狀況，也就是在一些中小型程序（好比這種做業）中，程序員可以決定整個程序所採用的架構（尤爲是數據結構）的狀況下來描述程序，由於這種狀況下是真正的只在乎功能的正確性而不在意如何實現，而在稍微大型的系統（好比OS的小操做系統，實際上它也沒那麼大）中，架構已經定的死死的，就很難有JML發揮的餘地，這時候就只能用天然語言描述方法所指望的功能，而後由程序員套用現有的架構來實現功能。這種狀況實際上在本單元的後兩次做業中就體現了出來，在第一次做業後，Path，和PathContainer中的相關容器已經肯定，這時候再看JML中的描述，就要在頭腦內將其翻譯成用咱們對應的容器的實現方式，與其作這樣燒腦的翻譯工做，還不如直接看指導書的天然語言描述而後實現來得快呢。卻是描述一些邊界、異常狀況時，JML的準確性還算是起到了一點幫助。

另外說到準確性，從做業和實驗課JML屢次的改動中，就能看出一個致命的問題：用規格來確保程序的正確性，那麼用什麼來確保規格的正確性呢？

（提及來課程組能夠考慮組織一次關於JML的辯論，效果絕對好）

但除開JML，我在第三次做業的一堆Bug中，深入體會到了測試的重要性。由於測試不夠強（無論是本身作的測試仍是提交的中測），我強測只拿了10分，互測被各類Hack了19次（最後這37個樣例被一波帶走是最騷的）。雖然也嘗試過用JUnit來進行測試，但仍是沒能想到初始化的可能狀況，於是也構造不出複雜的樣例。從這裏就能看出隨機測試的必要性，它能覆蓋程序員沒注意到的地方，對意想不到的Bug進行發現。因此，感受測試程序的重要性真的不亞於寫出程序。但每次寫完做業後，老是感受測試的時間和精力不夠，這個問題一直困擾着我，說到底仍是但願可以好好實踐一下測試方法，尤爲是隨機測試的方法。