一、JML初探 作為一種形式化語言，可以約束 代碼中類和方法的狀態和行為形成規格，通過將一系列具體代碼實現抽象成明確的行為介面，可以形成一種契約式編程模式， 設計者無需考慮實際的數據結構與演算法，可以聚焦於程式的整體邏輯， 形式化語言的無二義性能讓實現者準確理解介面功能，根據問題需要選擇合適的實現 ...
一、JML初探
JML(Java Modeling Language)作為一種形式化語言，可以約束Java代碼中類和方法的狀態和行為形成規格，通過將一系列具體代碼實現抽象成明確的行為介面，可以形成一種契約式編程模式，JML設計者無需考慮實際的數據結構與演算法，可以聚焦於程式的整體邏輯，JML形式化語言的無二義性能讓實現者準確理解介面功能，根據問題需要選擇合適的實現方式，同時JML可以幫助實現者開展代碼測試與形式化驗證，當然這時就要分析出模型語言映射到具體代碼的抽象函數了。
JML表達式
JML可以內嵌在.java內，很方便，以// @行註釋或/* @ ... @ */塊註釋，JML表達式支持Java表達式作為基礎。針對更複雜的邏輯引入了量詞表達式，\forall關鍵字類似數學中的∀，用法為\forall v; P(v); Q(v)，等價於∀v(P(v) → Q(v))；\exists關鍵字類似數學中的∃，用法為\exists v; P(v); Q(v)，等價於∃v(P(v) ^ Q(v))；這是在本單元比較常用的，當然還有\max, \sum, \min等實用的關鍵字。
還可以使用特殊操作符==> <==>表示蘊含與等價關係，使用這種操作符可以增強JML的可讀性，同時還有\nothing, \everything表示當前作用域下的空集全集
方法規格
本單元我們聚焦於JML中的方法規格，方法規格針對類中各種方法（構造、修改、查詢、生成）的返回值與行為進行約束，方法規格的三大關鍵是前置條件、後置條件、副作用範圍。
前置條件通過對參數施加約束，從而區分不同的處理操作，大體可分為normal_behavior，expcetional_behavior，各有各的前置條件，從而通過JML可以直觀看出何時需要對異常輸入處理，何時是正常輸入，當然二者的條件不能有交集。若輸入均不滿足前置條件，我們在實現中是沒有理由進行處理的，因此方法的調用者為了保證結果的可控必須瞭解前置條件。對於前置條件，使用requires P;要求輸入滿足命題P
後置條件對方法調用之後的對象狀態與返回值約束，規定方法行為，使用關鍵字ensures規定後置條件，對於查詢(query)方法，特別是只關心返回值不改變數據的方法，可以在訪問修飾符後加上/*@pure@*/ 標記，對於返回值(\result)的表示，一般使用ensures P(\result);
當然可能在查詢中可能也會修改對象，比如惰式更新，修改方法(modify)也要修改對象，為了表示出修改與其範圍，我們需要調用前的狀態，ensures P針對的是調用後狀態，\old(obj)關鍵字就可以看作對象/基本類型在方法調用前的快照。比如對於涉及容器的數據管理類，經常使用增刪Add, Remove方法，\old就派上用場了，可以使用P(\old(obj)) ==> Q(obj)描述新的對象狀態，當然這對對象的新狀態是一種弱約束，比如不能保證Add後不會加入不期望的元素，可以在另一方向再加一個條件(constains(obj) && !isforadd(obj)) ==> \old(constains(obj))進行最小化，可見利用requires, ensures已經可以基本描述方法了
還有一個方面就是副作用範圍(side effect)了，我們可以列出本方法中可能修改的類中（靜態）屬性，對調用者而言，可以輕鬆get到是否會修改自己關心的敏感屬性，通常使用assignable(modifiable)來列出可能修改的屬性表assignable v1, v2, ...;，也可以使用JML中的全集，空集
上面提到的expcetional_behavior是針對Java的異常特性的，使用signals關鍵字規範了異常的拋出時機與類型，用法為signals (<Exception Class> e) P;，等價於當P == true時throw異常，本單元對程式魯棒性的考量也在此體現
類型規格
類型規格就是對類中屬性數據的約束，類似Java，JML可在變數名前加修飾符，non_null保證容器內無null，遵從這個規約可有效避免訪問空引用，也有static, instance區分靜態屬性，當然JML想訪問類中private屬性時，相關屬性可加/*@spec_public@*/，但我們的實現大可不必完全按規格來，規格描述也不該關心具體實現中的數據（這一點是在實驗課中體會到的），本單元JML描述中容器都用數組表示，但我們只要符合規格的約束條件，可以選擇更合適的數據結構。本單元代碼中未涉及不變式invariant、狀態變化約束constraint，這兩個是比較強的約束條件，前者規定每次屬性修改後的規約，後者表示屬性修改相對於修改前狀態的規約
總之JML對代碼實現者很實用，本單元寫代碼時官方JML已經給出了整體的結構與邏輯，JML中還有不少很實用的用法，值得日後深入學習一哈
| 關鍵字 | 作用 |
|---|---|
| \not_assigned(x,y,...) | 變數是否在方法執行過程中未被賦值 |
| \not_modified(x,y,...) | 變數在方法執行期間的取值是否未發生變化 |
| \type(type) | 返回類型type對應的類型 |
| \typeof(expr) | 返回expr對應的準確類型 |
| \num_of | 返回變數中滿足相應條件的元素個數 |
二、JML之工具鏈
IDEA貌似沒有插件式的JML工具，還是挺可惜的，JML官網有相關工具的介紹
OpenJML
OpenJML可用於JML的語法檢查分析，下載解壓到項目文件夾下運行
java -jar openjml.jar -exec Solvers-windows\z3-4.7.1.exe -esc com\oocourse\spec3\exceptions\*.java com\oocourse\spec3\main\*.java
發現提示int與#INT1不同啥的，是JML中三目運算符的解析好像有點問題，把Group介面中三目修改成
/*@ ensures (\result == 0 && (people.length == 0) || (people.length != 0) && \result ==
@ ((\sum int i; 0 <= i && i < people.length; people[i].getAge()) / people.length));
@*/
JMLUnitNG
JMLUnitNG可基於JML對代碼實現自動生成測試代碼並開展測試，使用java -jar jmlunitng.jar 介面 源碼生成了測試代碼
與同學交流貌似需要在JDK 8環境下才能運行，在IDEA中Project Structrue -> Project Settings -> Project language level設置成8，運行一下針對Group介面的測試代碼
可見JMLUnitNG是針對極端數據的，說好也是驗證了程式的基本功能，說壞數據覆蓋面並不廣，對本單元作業的幫助有限。
其他
JMLEclipse：針對Eclipse的JML插件JMLOK：介紹是說隨機數據對JML實現的測試AspectJML tool, JML4c：運行時規格驗證
三、架構與Java性能提升
本次作業要求是對社交關係網路的模擬，很顯然是一種圖論模型，Person介面作結點，Network作圖，Group作子圖，JML規格將層次描述的很清楚，強制Person管理邊集，層次按圖的層次就好，在hw9, 10我還專門引入了邊類MyFriend，主要考慮到可能迭代會出現Person的子介面。而且針對hw10的isCircle還保留了BFS和Disjoint Sets兩個版本的，主要考慮到最後可能會加入刪邊操作，並查集的刪邊操作至少也得是O(V + E)了，然而都並沒有,whatever,本單元這一點相當友好，筆者終於不用重構了
選用數據結構方面，考慮到id範圍，類中容器全部選擇以id為鍵值的Hashmap<>，當然用兩個Hashmap<>建立起結點輸入id到數組下標index的可逆函數 + 靜態數組也很不錯，為了可維護性選了前者
為什麼要說"Java性能"
JML設計者只關心類可見的狀態，並不關心具體實現的類內部狀態，這也是同學們發揮的空間，但那種直接對著規格照葫蘆畫瓢的代碼是很危險的，筆者仍然記得hw10用互測規模數據都可以把Group.getAgeVar朴素遍歷卡到1e9級複雜度(運行分鐘級)，震驚了。反正適合實際問題的方法才是最好的！其次，Java還有c++這種面向對象語言，但凡涉及到字元串String，容器(container)之類的，抽象層次一高，就很難針對問題進行優化，導致執行效率低，反正很慢就是了，而且根據數據本單元T的還不少，所以提高性能很關鍵，這一部分圍繞幾個圖架構下的關鍵矛盾方法開扯
連通塊-isCircle & queryBlockSum
前者查詢是否為同一連通塊內，後者查詢連通塊數，最優解為並查集(Union-find Sets)，具體原理老生常談了。isCircle()兩次find操作，同時在圖內維護連通塊數k，增加結點addPerson時k++，增加邊addRelation時進行merge操作，若為不同連通塊合併,k--，在i條指令下複雜度為O(E + i)
當然hw10中的並查集有很大的隱患，遞歸形式的find操作在退化成單鏈的圖中遞歸層數為V，筆者通過壓力測試發現四千多層就爆棧了，StackOverFlow由遞歸層數，JVM設置的棧大小以及函數參數，局部變數大小決定，筆者決定穩他一手，將find路徑上的結點暫存一下，找到父節點後統一設置父節點，就不遞歸了
像開頭說的，並查集如果面對刪邊deleteRelation很棘手，由於查並集路徑壓縮信息丟失，不能單純的改父節點，我們需要遍歷點集找到涉及的兩個連通塊的點集，再遍歷一遍打上標記，刪邊，對於有標記的點展開BFS重新記錄下父節點,O(V) / O(V + E)，但如果deleteRelation有條數限制，那又是另一種權衡了
記憶化-Group介面
Group用於查詢子圖信息，為了提高效率維護內部屬性，反正一堆東西在addPerson / delPerson時更新就好，平均值維護年齡和suma，方差維護年齡平方和suma^2，套公式(suma^2 + mean^2 * size - 2 * size * suma) / size特別地，子圖內的增加邊(ar)可以繞開Group，所以ar的時候得更新一下邊的數據，沒啥可操作的，但必須我們對變數的維護這個優化要符合JML（比如hw11再維護int suma^2就溢出了，一定得保證正常情況合法結果），對拍走起
點雙連通分量-queryStrongLinked
通讀一下規格，查詢兩個結點是否在某個階數大於2的環路上，在討論區大手子指點下可以解讀為兩個結點是否在某個階數大於2的點雙連通分量上，學習了一下資料，點雙連通分量竟然是tarjan？筆者只用過神奇的塔尖求過有向圖的強連通分量啊...然後其實把求有向圖的強連通分量的tarjan的DFS樹的出棧條件改一下就好了：遞歸遍歷子節點後再出棧改成每個子節點遞歸後出棧。上張簡單圖（數字是DFS順序，箭頭是DFS大概的方向）
可以看到我們2次回溯到1，根據塔尖的遞歸更新，2, 3 / 4，5的low都會標記成1正好對應兩個分量，但在求強連通分量時要等到1無子節點時再出棧；改改代碼，每次回溯到根節點出棧就ok，當然註意不能出棧根節點，它可以處在多個分量中，並且註意特判階數，O(V + E)
單源帶權最短路-queryMinPath
經典帶權最短路，經典Dijkstra，堆優化後O(Vlog(V))
Java中想要搞一個小頂堆，PriorityQueue / TreeSet就夠用，兩者分別基於靜態數組與紅黑樹，當然註意不能修改堆比較器中涉及的類屬性，這將破壞堆維護的性質並導致意料之外的Bug，只能冗餘加或先刪除再添加，PriorityQueue就不要先刪再加了，畢竟只能按引用查找遍歷到下標再刪，O(n)，紅黑樹的增刪都是O(log(n))
public boolean remove(Object o);
private int indexOf(Object o);
為啥筆者還是TLE一個點，排查後原來是結點聯結邊集Hashmap<>(initalSize)初始化容量太大了，Hashmap迭代器遍歷的核心函數為
final HashMap.Node<K, V> nextNode() {...
if ((this.next = (this.current = e).next) == null && (t = HashMap.this.table) != null)
while(this.index < t.length && (this.next = t[this.index++]) == null);
...}
可見要一次迭代器遍歷要遍歷哈希表到最後一個鍵值對，複雜度是容器的線性，所以說容量不能設太大，或者說這種無序型容器就不適合進行頻繁的遍歷操作，我們可以冗餘存儲一個順序容器。當然對於qmp, qsl這種頻繁訪邊點權的操作，建立起結點輸入id到數組下標index的可逆函數 + 靜態數組進行離散化就很香了，再把那個圖中的邊集直接一給MyNetwork管理，採用鏈式前向星，就純數組，繞過低效的容器和對象，甚至可以搬自己的c代碼了，起飛
次序，區間查詢
queryAgeSum()單點更新，區間查詢，教科書的樹狀數組，queryNameRank在查詢次數遠大於節點數時可以二分下界查找，本次作業應該不太實用
四、Bug們和修複
JUnit單元測試
這是一個可以快捷開展針對特定方法測試的框架，很實用，因為本單元我們要抓住關鍵矛盾，測試複雜方法就好了，用@Before標記可以在測試前初始化數據，用@Test開展一次測試，一般測一個函數就好了，Junit可以把不同測試的stdout分開，關於測試方式，我們往往要優化代碼，所以我們可以在測試類中模擬這些方法的朴素版，比如Group的，然後隨機構造數據，通過Junit的斷言Assertion機制來驗證一下優化版是否保證了正確性，當然可以調用c來對拍，Junit內嵌於Java相當靈活，還可以用於拋出異常的測試和運行時間的分析，是非常有用的Debug工具
自測 & 公測 Bugs
- 首先是之前說的優先隊列內元素不隨意修改，筆者竟然沒註意到
Java只能傳引用的特性；修複： 冗餘加入的時候clone()一下 Group.getAgeVar沒註意到size == 0的情況，divide by zero，hw10強測翻皮水- 上文說了
qmp在設置哈希表容量過大時不要迭代器遍歷，TLE一個點
五、規格設計心得體會
JML作為一種形式化語言，表意很準確，我覺得結合介面API文檔使用也就更直觀了，本單元作業沒有涉及不變式跟繼承關係下的規格啥的。但其實主要讓筆者體會到了規格設計中的契約式編程方法，設計者和實現者分離，我們在作業中扮演的實現者就是要在JML規格之下考量可維護性，執行效率，可讀性，採用最合適的。這是一種高效的開發模式，對我們在團隊項目、工作中很有用處
