這三周的作業主要是圍繞以JML來約束代碼開發，以確保程序的正確性與魯棒性。
Part 1：三次作業的實現與bug
第一次作業沒有任何算法和數據結構上的難度，對于Path和PathContainer的各個方法的實現按照給出的規格復讀即可。唯一的難點（大約也不算難點）便是將NodeId進行映射，用hashmap就好，不過注意不要做一個調包俠，hashmap中有的方法譬如遍歷很慢，雖然看上去只差常數，但是這個常數巨大，如果在第一次作業中不加處理就會在第二次作業中TLE。
第一次作業也讓我們了解了拋異常，我個人認為JML對于拋異常的處理是值得稱道的，通過這樣的約束可以控制程序在犯了一些明顯的錯誤后及時停止而不是越錯越遠浪費計算資源，造成更嚴重的后果。
?
第二次作業是在第一次的基礎上寫一個Graph類，這個類繼承PathContainer，將不同的Path匯總成一個圖，并能夠查詢最短路。
對于第二次作業，首先要吐槽的是給出的接口，在需要繼承的情況下應該聲明為protect，才能更好地實現數據的繼承，而給出的接口使用了private，給我們的選擇便只有重新聲明數據，每當使用的時候get一次以更新或者將第一次PathContainer的代碼復制到Graph中，我為了偷懶選擇了后者，結果第三次就只能靠瘋狂壓行來改正代碼風格。
對于第二次圖的實現，介于圖中邊權均為1，求最短路和是否連通均可以使用BFS。在BFS中將查找到的點均進行更新就好，這樣，在詢問兩點是否連通或者他們的最短路時，可以先查找對應圖中兩點間值是否為初始值，若是則BFS查找更新，否則直接返回結果。同時只有當需要查找兩點間最短路或者連通情況且Path有過remove或add且上一次Path改變后沒有更新才更新圖。
?
對于第三次作業，其實是在求帶權最短路。這里再使用BFS就不太合適了。
對于連通塊數量，可以使用并查集，也可以選擇圖中一個點開始BFS，終止后若沒有遍歷所有點則選擇一個未遍歷的點繼續BFS，如此往復至圖中所有點被搜索過即可。這兩者后者更快。
對于三種不同的最短路，王嘉儀同學給出的關于圖的數學性質是正確的，利用這個性質我們可以更簡潔的完成最短路。
以最短花費為例，設邊權為1，跨路徑一次消耗2，則最終消耗=邊數+2*換乘數-2，此時，對于同一路徑內任意兩點，我們先求出圖內floyd最短路圖，將其中的值全部加上2，再將這些圖合并后使用迪杰斯特拉求出兩點間最短路，得到的值減去2就是正確答案。注意求起點a到終點b的最小花費時，使用迪杰斯特拉算法更新的點答案均是正確的，所以若是詢問的兩點的最短路值不是初始值就可以直接輸出了。其余幾種最短路可以類推。
?
這三次作業只有最后一次有bug，我將最短路的圖設置為了1000，沒想到UnpleasentValue的最小值超過了1000.
關于這三次作業的不足，我覺得最大的問題在于繼承復用上。因為接口里給出的類型是private，沒有辦法使用protected繼承數據，導致繼承時需要把所以數據使用時get一次，而我選擇了偷懶的辦法，直接將被繼承的代碼寫入了新的代碼中，這導致我第三次作業的Railway很長很丑。
Part 2：關于JML
?JML(Java Modeling Language)是用于對Java程序進行規格化設計的一種表示語言。
JML能夠用形式化語言來規范代碼，提高代碼可維護性。
JML以注釋形式存在，每行以@開始，分為行注釋（表示為//@......）和塊注釋（表示為/*@......@*/）。
JML有原子表達式，量化表達式，集合表達式等等，以及約束類型的類型規格和約束方法的方法規格。
原子表達式有\result和\old()兩種，前者用來約束一個方法的返回值，后者用來表示括號內內容在方法執行前的內容。
量化表達式有forall，\exists和\sum，forall表示某范圍內的元素均應滿足某條件，為全稱量詞，相應的\exists為存在量詞，而\sum返回的是給定范圍內表達式的和。
集合表達式則構造一個容器，明確其包含的元素。
操作符包含子類型操作符<，等價操作符<==>，不等價操作符<=!=>，推理操作符==>，上述操作符均返回bool型值。
對于方法規格，我們通過requires語句約束前置條件，通過ensures語句約束后置條件，同時JML也給出了副作用、異常的約束，通過saaignable和modifiable來約束副作用，并利用signals來拋異常。
對于類型規格，主要利用不變式invariant P來進行約束。
部署JML UnitNG/JML Unit
安裝后，編寫測試樣例如下：
測試結果如下：
關于JML的使用，我個人感覺它只應該是一種嚴格的約束。事實上，我們的代碼和JML都是形式化語言，而我們使用JML是為了自然語言表述不清導致代碼bug。
我認為，規格應該是宏觀的，整體的，針對于方法的輸入輸出形式，而不應該是對于代碼實現的全盤描述，若是后者，那寫代碼豈不成為了對于規格的翻譯？那我們為什么不直接寫規格？規格應該是規范而不涉及具體的內部實現。
舉個例子，形式化的規格語言可以作為偽代碼來描述算法，我們利用這種形式化的語言來詳盡的描述算法，在用java語法來翻譯規格語言，這顯然是在做重復無謂的工作。
在這幾次作業中，尤其是最后一次作業，我們可以發現，新增的方法具有大量的規格，不少同學都吐槽過這個規格又臭又長，而我發現這些又臭又長的規格真正有用的部分是在于對于輸入輸出數據合法性判斷以及拋異常的部分，剩下的部分其實是在表達算法思想，而我認為描述算法不應該是規格應該做的。
