理論基礎
jml是用於對j**a程式進行規格化設計的一種表示語言
注釋結構
jml以j**adoc注釋的方式來表示規格，每行都以@起頭。有兩種注釋方式，行注釋和塊注釋。其中行注釋的表示方式 為//@annotation，塊注釋的方式為/* @ annotation @*/。按照j**adoc習慣，jml注釋一般放在被注釋成分的 近鄰上部
jml表示式
2.1 原子表示式：
\result表示式：表示乙個非void型別的方法執行所獲得的結果，即方法執行後的返回值
\old( expr )表示式：用來表示乙個表示式expr在相應方法執行前的取值。
\not_assigned(x,y,...)表示式：用來表示括號中的變數是否在方法執行過程中被賦值。
\not_modified(x,y,...)表示式:該表示式限制括號中的變數在方法執行期間的取 值未發生變化。
\nonnullelements( container )表示式：表示container物件中儲存的物件不會有null
\type(type)表示式：返回型別type對應的型別(class)
\typeof(expr)表示式：該表示式返回expr對應的準確型別。
2.2 量化表示式
\forall表示式：全稱量詞修飾的表示式，表示對於給定範圍內的元素，每個元素都滿足相應的約束。
\exists表示式：存在量詞修飾的表示式，表示對於給定範圍內的元素，存在某個元素滿足相應的約束。
\sum表示式：返回給定範圍內的表示式的和。
\product表示式：返回給定範圍內的表示式的連乘結果。
\max表示式：返回給定範圍內的表示式的最大值
2.3 集合表示式
集合構造表示式：可以在jml規格中構造乙個區域性的集合（容器），明確集合中可以包含的元素。
2.4 操作符
jml表示式中可以正常使用j**a語言所定義的操作符，包括算術操作符、邏輯預算操作符等。此外，jml專門又定義 了如下四類操作符。
(1) 子型別關係操作符：e1<:e2>
(2) 等價關係操作符：b_expr1<==>b_expr2或者b_expr1<=!=>b_expr2
(3) 推理操作符：b_expr1>b_expr2或者b_expr2
(4) 變數引用操作符：\nothing指示乙個空集；\everything指示乙個全集
方法規格
應用工具鏈
public class sub9 10 public static void main(string args)
13 }首先，對jml語言進行檢查。
1 j**a -jar ../openjml/openjml.jar -check sub.j**a > re.txt1 j**a -jar jmlunitng-1_4.jar sub.j**a
2 j**ac -cp jmlunitng-1_4.jar *.j**a
3 j**a -jar ../openjml/openjml.jar -rac sub.j**a
4 j**a -cp jmlunitng-1_4.jar sub_jml_test
第一次作業：
第一次作業要求為實現容器類path和pathcontainer，path為節點序列，pathcontainer需要實現pathid和path的檢索以及容器內不同節點個數的查詢。
具體實現為：path類通過arraylist儲存路徑，hashset儲存點集；pathcontainer通過兩個hashmap解決路徑檢索，維護乙個hashmap記錄不同節點的個數。
第二次作業：
在第一次作業的基礎上要求實現graph類，需要實現對任意節點間最短距離的查詢。
我實現了graphquery類來完成對所有圖相關查詢指令的處理。最短距離的計算，我選擇使用floyd法，由於節點的id為int型別，需要首先將其對映到從0開始的連續整數。在graphquery中維護乙個hashmap記錄該對映關係。每次增加路徑時，graph類呼叫graphquery的add方法，為新增的所有新節點分配對映關係，初始化floyd矩陣並計算。每次刪除路徑時，重新初始化floyd矩陣並計算。
第三次作業：
在第二次作業的基礎上要求實現railwaysystem類，實現對任意節點間最少換乘、最少票價和最少不滿意度和圖的聯通塊數目的查詢。
圖的聯通塊數目我採用bfs染色進行計算。
對於三種最短路的計算，我採用討論區著名的wjy演算法，將每一條路徑先構造成完全圖，對於最少換乘，將一條路徑上所有點間的權值設為1；對於最少票價，則將權值設為兩點間的距離+換乘費用也就是2；對於最少不滿意度，將權值設為兩點間的不滿意度+換乘不滿意度即32；如此對任意查詢，求其對應圖的兩點間最短路徑即可。
具體架構：由於每條路徑都需要重新建圖，且該圖是稀疏圖，因此我採用spfa法計算對不同查詢要求計算兩點間的新權值。首先封裝了spfacalculator用於對一張圖的最短距離計算，每增加一條路徑，例項化乙個updater，記錄該路徑對應的鄰接矩陣並呼叫spfacalculator計算，返回新圖。在railwayquery中維護三個矩陣分別對應三種需求，對每一條路徑，呼叫updater獲取小圖並更新大圖，之後進行floyd運算。
第一二次作業均沒有bug出現，第三次作業對相同節點的contains edge出了問題，通過floyd矩陣中對應位置元素的大小是否為1來判斷，但在初始化該矩陣時跳過了對角元的初始化，導致總是返回無窮大。
jml語言更加精準的描述了乙個類或者方法的行為，先寫jml再實現對應類或方法，可以明確方法的邊界行為，並對降低程式的耦合度很有幫助。而本次作業的迭代開發的過程，也讓我對繼承的具體實現有了更多的認識。
OO第三單元總結
一 實現規格的設計策略 1.基於規格，設計方法 大部分需要我們寫的方法，都可以根據規格直接寫出來，這些方法一般都是比較簡單的，比如查詢有沒有這個元素 返回某個元素 增加或刪除某個元素。2.根據規格，了解方法功能，自行設計方法 規格怎麼描述，方法怎麼寫也是可行的，但是了解了方法功能，自行設計會更快，比...
OO第三單元作業總結
在起初剛學習完jml規格語法的時候，由於對jml規格不夠熟練，我選擇了讓自己的 與規格 基本保持一致來完成作業。意思是，jml使用陣列實現，我也會使用陣列實現 jml使用兩層for迴圈實現，我也會使用兩層for迴圈實現。並且，我選擇了每讀乙個方法的jml，就完成乙個方法。顯然，這樣的策略不會讓我產生...
北航OO第三單元總結
本單元作業為jml規格的學習與應用，要求我們在閱讀jml規格之後實現出完全符合規格要求的方法。當然在完成作業之前我又需要從0開始學習jml規格，但好在jml的入門難度並不大，短短幾個小時後就可以讀懂作業中的jml規格了。而其實規格就像是乙個指導你具體實現方法的說明書，它會為你指定這個方法的前置後置條...