OO第三單元做業小結

1、JML理論基礎及應用工具鏈狀況

理論基礎

1.JML表達式

\result：表示方法執行後的返回值。

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

\foall：全稱量詞修飾的表達式。

\exists：存在量詞修飾的表達式。

<==>：等價關係操做符。

==>：推理操做符。

\nothing：變量引用操做符，指示一個空集。

\everything：變量引用操做符，指示一個全集。

2.方法規格

requires：表示前置條件(pre-condition)。

ensures：表示後置條件(post-condition)。

assignable：表示反作用範圍限定(side-effects)。

3.類型規格

invariant：不變式，要求在全部可見狀態下都必須知足的特性。

constraint：狀態變化約束，對前序可見狀態和當前可見狀態的關係進行約束。

應用工具鏈

OpenJML能夠對規格進行檢查，包括語法正確性檢查、靜態檢查、運行時檢查。

JMLUnitNG能夠根據規格自動生成測試樣例，檢測程序的正確性。

2、部署JMLUnitNG/JMLUnit，實現自動生成測試用例

 測試程序：

測試過程及結果：

測試樣例主要是針對數據的邊界狀況，三個沒有經過的測試點都是由減法溢出致使的。

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

第一次做業

MyPath類裏，用一個arraylist來存路徑中的全部點，以及一個hashmap來存全部不一樣的點。方法都是按照規格完成，值得一提的是從大佬那裏學來了簡單的重寫hashCode()的方法——直接return類中arraylist的hashCode()，由於對於arraylist來講，相同內容的兩個arraylist，它們的hashCode是相同的。

MyPathContainer類裏，因爲MyPath重寫了hashCode()方法，直接創建以id做爲key、path做爲value和以path做爲key、id做爲value的雙向hashmap。另外對於全部不一樣點的個數，創建一個以點的id做爲key，點的出現次數做爲value的hashmap，在add和remove path時，對這一hashmap進行維護，將增長或刪除的路徑中的全部點的出現次數在這一hashmap中的value值進行加或減，次數爲0時直接刪除，這樣在獲取不一樣點個數時就能夠直接return這一hashmap的size()。

第二次做業

第二次做業採用的是floyd算法求最短路徑，每次add或者remove，都根據graph中存儲的全部path創建一個二維矩陣，而後用floyd算法求解。

第三次做業

第三次做業仍採用floyd算法，基本方法參考討論區大佬的不拆點方法（這方法真的太強了），維護四個二維矩陣，而且對於每一個路徑的不滿意度和票價矩陣都用一次floyd，最後在每一次add和remove時，都從新初始化四個矩陣並各自floyd，以獲得最終結果。

這三次做業其實基本上沒有太多重構，由於第二三次都是用的floyd算法，其餘的方法基本上都是沿用上一次的方法。

4、按照做業分析代碼實現的bug和修復狀況

第一次做業比較簡單，沒有出現bug。

第二次做業強測wa了兩個測試點，互測被刀了兩刀，都是源於同一處bug。因爲路徑中的點並非從0開始遞增，在創建二維數組時，須要創建一個從點的id到遞增天然數的一個映射，以表示數組的index。我在每一次add和remove時，都會先將二維數組初始化，而忘記將儲存映射關係的hashmap也初始化，這就致使刪除了某些點以後，它的映射關係仍儲存在hashmap中，會出現數組越界的錯誤。

第三次做業也吸收了第二次做業的教訓，沒有出現bug。

5、闡述對規格撰寫和理解上的心得體會

 在規格撰寫方面，在幾回上機以及理論課上的練習中，感受撰寫規格要比理解規格難一些，感受一次性很難完整寫出一個方法的規格。

至於規格理解，就要簡單不少，在熟悉JML各類表達式及規格以後，對於規格要求的理解基本上不會存在誤差。

其實本單元的做業，主要難點仍是在於算法及架構設計上，因爲CPU時間作出了要求，咱們必須充分考慮選擇算法的時間複雜度，而第三次做業增長的票價、不滿意度等計算，進一步加大了代碼設計的難度。

總的來講，規格仍是頗有用的，它能很好地規範代碼，並且能幫助程序員養成良好的代碼編寫習慣。