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能夠根據規格自動生成測試樣例,檢測程序的正確性。
測試程序:
測試過程及結果:
測試樣例主要是針對數據的邊界狀況,三個沒有經過的測試點都是由減法溢出致使的。
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算法,其餘的方法基本上都是沿用上一次的方法。
第一次做業比較簡單,沒有出現bug。
第二次做業強測wa了兩個測試點,互測被刀了兩刀,都是源於同一處bug。因爲路徑中的點並非從0開始遞增,在創建二維數組時,須要創建一個從點的id到遞增天然數的一個映射,以表示數組的index。我在每一次add和remove時,都會先將二維數組初始化,而忘記將儲存映射關係的hashmap也初始化,這就致使刪除了某些點以後,它的映射關係仍儲存在hashmap中,會出現數組越界的錯誤。
第三次做業也吸收了第二次做業的教訓,沒有出現bug。
在規格撰寫方面,在幾回上機以及理論課上的練習中,感受撰寫規格要比理解規格難一些,感受一次性很難完整寫出一個方法的規格。
至於規格理解,就要簡單不少,在熟悉JML各類表達式及規格以後,對於規格要求的理解基本上不會存在誤差。
其實本單元的做業,主要難點仍是在於算法及架構設計上,因爲CPU時間作出了要求,咱們必須充分考慮選擇算法的時間複雜度,而第三次做業增長的票價、不滿意度等計算,進一步加大了代碼設計的難度。
總的來講,規格仍是頗有用的,它能很好地規範代碼,並且能幫助程序員養成良好的代碼編寫習慣。