OO第三單元做業小結

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

理論基礎

1.JML表達式程序員

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

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

\foall:全稱量詞修飾的表達式。架構

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

<==>:等價關係操做符。工具

==>:推理操做符。post

\nothing:變量引用操做符,指示一個空集。測試

\everything:變量引用操做符,指示一個全集。ui

2.方法規格spa

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時間作出了要求,咱們必須充分考慮選擇算法的時間複雜度,而第三次做業增長的票價、不滿意度等計算,進一步加大了代碼設計的難度。

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

相關文章
相關標籤/搜索