JML語言的理論基礎及相關工具鍊
理論基礎
JML(Java Modeling Language)是用于對Java程式進行規格化設計的一種表示語言。
注釋結構
JML以javadoc注釋的方式來表示規格，有行注釋和塊注釋兩種注釋方式。其中行注釋的表示方式為
//@annotation
，塊注釋的表示方式為
/*@ annotation @*/
。
常用JML表達式
-
\result
void
-
\old(expr)
expr
-
\forall
-
\exists
-
\sum
\product
\max
\min
\num_of
- 等價關系操作符
<==>
==>
方法規格
- 前置條件，通過
requires
- 後置條件，通過
ensures
- 副作用限制，通過關鍵詞
assignable
modifiable
- 純粹通路性方法，通過關鍵詞
pure
- 異常功能規格，通過
public exceptional behavior
signals
類型規格
- 不變式，要求類成員在所有可見狀态下都必須滿足一些特性。
- 狀态變化限制，要求類成員在狀态變化時滿足一定條件。
相關工具鍊
- OpenJML，筆者未能成功部署環境，但聽聞該工具多年未維護，JML文法支援面小，功能有限。
- JMLUnitNG，用于随機生成測試用例，主要對邊界情況進行考察。總體而言，資料覆寫度較低，測試效果較差。
- JUnit，成熟的單元測試工具，筆者在測試程式的基本功能方面，有較好的體驗。
作業架構
本單元的作業着重考察圖論算法，可剝離社交網絡的外殼而抽象出一個圖類，針對不同的操作動态建圖，但課程組下發的
Person
接口已經足夠完善，無需額外封裝，故筆者并未嘗試完成這項工作。
本單元架構明顯，人作為點，關系作為邊，實作差異主要展現在兩方面——容器選擇、算法選擇。容器選擇方面，筆者的理念是，盡可能多的使用性能良好的
HashMap
。算法選擇方面，筆者的理念是，在不逾時的情況下，盡可能多的使用樸素易懂的簡單算法。
第一次作業
容器選擇方面：
-
MyPerson
HashMap<Person, Integer>
key
value
-
MyNetwork
HashMap<Integer, Person>
id
key
value
算法選擇方面：
第一次作業僅涉及到兩點的連通性問題，算法具有多中選擇，如深度優先搜尋算法、廣度優先搜尋算法、并查集算法等。筆者選用了樸素的廣度優先搜尋算法。
第二次作業
第二次作業新增組的概念，組是人的集合。
-
MyGroup
HashMap<Integer, Person>
id
key
value
-
MyNetwork
HashMap<Integer, Group>
id
key
value
組的屬性均可以進行維護，且僅在兩種情況下需要維護：在向組中添加人時、在向身處同組的兩個人間添加關系時。
第三次作業
第三次作業新增組内人員可删去的情況，同時涉及到了求圖中連通塊個數、求兩點最短路徑權值、判斷兩點是否在同一環路中等問題。
- 由于本次作業更多的涉及到了兩點連通性的詢問，筆者為了加速兩點連通性的判斷以及捎帶求圖中連通塊個數，更換廣度優先搜尋算法為并查集算法。
MyNetwork
HashMap<Person, Set<Person>>
key
value
每當向圖中新增人時，新增一個僅包含此人的連通塊。
每當向圖中新增關系時，判斷此關系涉及的兩人是否在同一個連通塊裡，若不在，則合并兩人所在的兩個連通塊。
此時，判斷兩點是否連通，即判斷兩點是否在同一個連通塊中，時間開銷大大降低。
- 由于本單元作業有較多的動态加點和動态加邊操作，筆者在求兩點最短路徑權值的問題上，放棄了Floyd算法，選擇了堆優化的Dijkstra算法。算法詳解可參考《算法導論》。
- 本次作業讨論區中出現了筆者聞所未聞（太菜了555）的點雙連通分量等概念，于是筆者學習了相關知識，在判斷兩點是否在同一環路中的問題上，選擇了Tarjan算法。算法詳解可參考《資料結構與算法分析》。
代碼實作bug
筆者在三次作業中均未發現bug，互測房間其他人的bug主要為運作逾時，原因多為算法實作問題，如：第二次作業中不對組的屬性進行動态維護、第三次作業中在判斷兩點是否在同一環路中時使用複雜度較高的算法等。
心得體會
在完成本單元作業的過程中，筆者更多的還是專注到了圖論算法中，回顧了很多漂亮的算法實作，也對java語言的一些内部容器有了更多的認識。
本單元對JML的接觸大多為閱讀并了解，真正讓我們手寫的JML并不多，是以撰寫JML的能力并不佳。但筆者認為，規格給予了實作人員自信，隻要實作滿足規格要求，就一定是正确的，同時規格也為程式測試的開展指明了方向。