JML理論基礎
簡介
JML(Java Modeling Language)是一種用於對JAVA程序進行規格化設計的語言，其通過定義接口所包含方法的行為，來約束實現接口的類的行為。本章作業就是實現課程組提供的用規格定義好的接口，來學習如何根據規格寫方法。
JML表達式
原子表達式
| 關鍵字 | 含義 | 示例 |
|---|---|---|
| \result | 定義返回值 | \result == getPerson(id1).getAge() |
| \old(expr) | expr在執行方法前的取值 | groups.length == \old(groups.length) + 1; |
| \not_assigned(x) | 括號中的變量是否倍賦值 | \forall int i; 0 <= i < groups.length; \not_assigned(groups[i]) |
其中有一點容易混淆。\old(group.length)代表的是group在執行方法前的長度。而\old(group).length == group.length，指的是方法執行后的長度。這是由於在方法執行過程中，並沒有改變group指向的對象，只是改變了其指向對象的值。
量化表達式
| 表達式 | 含義 | 示例 |
|---|---|---|
| \forall | 對於范圍內的每個元素遍歷 | (\forall int i; 0 <= i < groups.length; \not_assigned(groups[i])); |
| \exists | 范圍內存在一個元素滿足后續條件 | (\exists int i; 0 <= i && i < groups.length; groups[i].getId() == id) |
| \sum | 范圍內滿足條件的表達式的和 | (\sum int i; 0 <= i < people.length && people[i].getAge() >= l && people[i].getAge() <= r; 1) |
方法規格
在此，以作業提供的接口方法規格為例，依次分析方法規格的組成部分。
1 /* 2 @ public normal_behavior 3 @ requires contains(id); //前置條件 4 @ assignable \nothing; //副作用限定 5 @ ensures (\exists int i; 0 <= i && i < people.length && people[i].getId() == @id;money[i] == \result); //后置條件 6 @ also 7 @ public exceptional_behavior //異常行為 8 @ signals (PersonIdNotFoundException e) !contains(id); 9 @*/
-
前置條件
通過requires子句表示，要求確保其表達式為真才可進行正常行為操作。
-
后置條件
通過ensures子句表示，要求確保方法執行后其表達式為真
-
副作用限定
通過assignable或modifiable表示，限定方法能夠修改的對象
-
異常行為
通過signals (ExceptionType e)為了提高程序魯棒性，在不滿足requires表達式時，需要進行其他異常行為操作（比如拋異常）。
一般通過public normal_behavior和public exceptional_behavior來區分正常行為和異常行為，但是對於正常行為設計多種條件分支（if-else語句）時，也可以把每個正常/異常分支使用public xxx_behavior區分開，以提高可讀性。（在本次作業提供的規格中多是這樣，所以閱讀規格時按照其分開，就可理清各種個各種if-else情況，方便輸寫）
類型規格
| 類型 | 含義 | 示例 |
|---|---|---|
| invariant | 不變式，在可見狀態下必須滿足的條件 | invariant seq_nodes != null |
| constraint | 狀態變化約束，前序和當前狀態之間關系的約束 | constraint counter == \old(counter)+1; |
工具鏈
OpenJML
檢查JML語法。不支持高版本java，環境很難配。
JMLUnitNG
根據規格自動生成測試。環境很難配。
Junit
單元測試。根據規格自行構造測試，可以檢查覆蓋率，盡量保證覆蓋率高（但不是全部覆蓋就沒bug）。
由於OpenJML和JMLUnitNG功能有限，所以本單元中主要還是采用單元測試的方法。
OpenJML驗證
整個src的檢測結果：
結果非常申必。
調整后：
發現以上的bug。
有時候會冒出上百個warning。為了美觀就不放了。
JMLUnitNG測試
以上為使用JMLUnitNG進行UserGroup類的測試。
可以看到，其主要對於邊界情況進行簡單測試。
我的架構設計
第一次作業
容器選擇
第一次作業要求比較簡單，實現了官方提供的三個接口。為了使得訪問更加方便，多使用HashMap作為容器。例如：在User類（實現Person接口）中，使用HashMap<id, value>來存儲熟人和value值。
並查集
另外，針對isCircle方法，為了降低復雜度，選擇並查集。在Network中，實現HashMap<id,father_id>存儲每個用戶和其祖先的id。在addPerson方法中，新增id對應的鍵值對，將father_id設為自己。在addRelation方法中，合並兩個人的father_id。另實現find方法，路徑壓縮+返回祖先。在isCircle方法中，對兩個id分別find出祖先，以判斷二人是否連通。
在find方法進行路徑壓縮時，需要注意先將find其父節點的返回值保存，再替換和返回，及采用如下寫法：
1 private int find(int id) { 2 if (father.get(id) == id) { 3 return id; 4 } 5 int ans = find(father.get(id)); 6 father.replace(id, ans); 7 return ans; 8 }
若使用如下的簡寫方法，會在成鏈情況&人多的時候出現棧溢出：
1 private int find(int id) { 2 if (father.get(id) == id) { 3 return id; 4 } 5 father.replace(id, find(father.get(id))); 6 return father.get(id); 7 }
第二次作業
本次作業新增Group接口，在設計過程中需要注意其中方法的性能。如果直接找着JML寫，會出現O(n^2)復雜度，而出現CTLE錯誤。因此，采用在向Group中加人的時候預處理relationSum，valueSum，conflictSum，ageSum，ageVar（由於向Group中加人有指令條數限制）。預處理方法如下：
1 public void addPerson(Person person) { 2 // renew people 3 people.put(person.getId(), person); 4 // renew conflictSum 5 conflictSum = conflictSum.xor(person.getCharacter()); 6 // renew ageSum 7 ageSum = ageSum + person.getAge(); 8 int meanAge = getAgeMean(); 9 ageVar = 0; 10 // renew relationSum 11 // renew valueSum 12 // renew ageVar 13 for (Integer next : people.keySet()) { 14 ageVar = ageVar + 15 (people.get(next).getAge() - meanAge) * (people.get(next).getAge() - meanAge); 16 if (people.get(next).isLinked(person)) { 17 relationSum = relationSum + 2; 18 valueSum = valueSum + (people.get(next).queryValue(person)) * 2; 19 } 20 } 21 ageVar = ageVar / people.size(); 22 relationSum = relationSum - 1; 23 }
采用這種方法不要忘記，在addrelation的時候可能會造成relationSum、valueSum的變化，因此還需要新建方法如下：
1 public void updateRelation(int value) { 2 relationSum = relationSum + 2; 3 valueSum = valueSum + 2 * value; 4 }
第三次作業
本次作業難點在於最短路算法和點雙連通分量算法。
最短路
最短路采用堆優化迪傑斯特拉算法，如果不堆優化可能會被卡。具體實現方法為，新建Pair類，包含屬性id和dis（表示到起點的距離），並繼承comparable接口，重寫compareTo方法。
1 @Override 2 public int compareTo(Pair o) { 3 if (dis > o.getDis()) { 4 return 1; 5 } else if (dis < o.getDis()) { 6 return -1; 7 } 8 return 0;
}
點雙連通分量
由於對tarjan不熟悉，怕寫bug，再加上時間足夠，因此采用暴力方法。
-
首先如果people.size == 2，一定不滿足條件，直接return false。
-
如果!isCircle(id1,id2)，一定不滿足條件，直接return false。
-
若isLinked(id1, id2)，則將兩人分別從acquaitance中移除，及刪掉兩人之間的邊，再dfs。若兩人依然連通，則return true。否則return false。
-
若!isLinked(id1, id2)針對所有出了起點、重點的人，將他們從圖中刪除（具體實現方法為，設置lock=id），然后dfs判斷id1和id2的連通性。若一直連通，則return true。否則return false。
還有一種常數優化，就是再遍歷所有點的時候，如果該點和id1不isCircle，可以直接continue，不進行dfs，因為去掉其一定不會影響兩點之間本來的連通性。
關於測試和bug
第一次
第一次作業比較簡單，在自己寫代碼的時候發現的bug就是find()方法棧溢出問題，已在架構設計中詳述。
互測和公測都沒有出現bug，屋里十分安靜。
第二次
第二次作業在自己測試中，一開始沒有考慮到addRelation對Group類的relationSum、valueSum的影響，通過Junit單元測試發現。
從本次作業開始采用對拍，不驗證輸出的正確性，而是橫向比較多人的輸出，若出現不同則有人有bug。
在公測和互測中沒有被發現bug。
互測中，共hack到兩個bug：
-
一位同學在使用O(1)求ageVar的時候，采用如下寫法：
(ageSquaredSum - 2 * mean * ageSum) / people.size() + mean * mean;
這種寫法的錯誤在於，第一個因子的分子部分可以是負數，而java整除對於負數向上取整。用如下數據就可以hack：
ag 1 ap 1 1 1 4 ap 2 1 1 5 ap 3 1 1 6 atg 1 1 atg 2 1 atg 3 1 qgav 1
-
一位同學由於時間復雜度高導致CTLE
第三次作業
第三次作業的易錯點比較多，依然采用對拍，不驗證輸出的正確性，而是橫向比較多人的輸出，若出現不同則有人有bug。在本地測試時發現了一下易錯問題：
-
針對qsl，只有兩人的情況可能需要特判。
-
使用優先隊列時，必須調用add方法才會更新排序，直接修改queue中元素時不會觸發重新排序的。
-
Group類中的ageVar會溢出int范圍（但是由於java不是到什么神奇的機制，並不會出現錯誤），但是需要注意，如果多項式中某一項轉long而某一項沒轉，可能會出問題。
-
delPerson的時候可能需要考慮除0問題。
在公測和互測中沒有被發現bug。
在互測中，發現了一下5個bug。
-
delPerson的時候沒有考慮除0。
-
采用靜態數組，出現越界問題。
-
在delPerson的時候沒有更新relationSum，valueSum
-
暴力求qsl寫的有點過於暴力，導致CTLE
-
qmp不完備，由對拍發現bug，由於可讀性不太好，沒有深究是什么問題。
測試
-
Junit單元測試，用於輸寫一些數據量較小的邊界情況，盡量覆蓋所有情況，測試基本功能。在此舉例：
View Code1 @Test 2 public void testQueryStrongLinked() throws Exception { 3 //TODO: Test goes here... 4 net.addPerson(new User(0, "a", new BigInteger("63"), 22)); 5 net.addPerson(new User(1, "a", new BigInteger("1"), 21)); 6 assertEquals(false,net.queryStrongLinked(0,1)); 7 net.addPerson(new User(2, "a", new BigInteger("1"), 21)); 8 // only two + not linked 9 assertEquals(false,net.queryStrongLinked(0,1)); 10 net.addRelation(0,1,5); 11 // only two + linked 12 assertEquals(false,net.queryStrongLinked(0,1)); 13 net.addRelation(0,2,5); 14 assertEquals(false,net.queryStrongLinked(0,1)); 15 // triangle 16 net.addRelation(1,2,5); 17 assertEquals(true,net.queryStrongLinked(0,1)); 18 net.addPerson(new User(3, "a", new BigInteger("63"), 22)); 19 net.addPerson(new User(4, "a", new BigInteger("1"), 21)); 20 net.addRelation(2,3,5); 21 net.addRelation(3,4,5); 22 net.addRelation(4,2,5); 23 // eight 24 assertEquals(false,net.queryStrongLinked(0,3)); 25 assertEquals(true,net.queryStrongLinked(3,4)); 26 }
-
對拍。在提交之前，邀請一些好友參加對拍，自動生成數據，橫向比對輸出結果和運行時間。第二次作業幫助多人共de出2-3個bug，第三次幫助多人共de出>5個bug，效率還是蠻高的。但是，由於對拍數據量較小，對於一些小數據邊界情況（比如qsl的僅兩人）可能不太友好，所以充足的本地單元測試是必要的。
感想
由於本單元沒有動手寫JML規格，所以對於其輸寫過程還是比較陌生。
在根據JML輸寫代碼時，看懂JML和按照其寫出滿足要求的方法不難，但是很多時候需要意會其中的深意，並且考慮性能上的優化。例如，queryblocksum方法是在求連通分量的數量，如果分析出這點，通過動態維護blocksum或者根據並查集求都是很簡便的，但如果完全仿照JML的寫法，雙重循環，會使得性能上有很大的損失。