title: 2020 OO 第三單元總結 date: 2020-05-21 10:10:06 tags: OO categories: 學習
第三單元終於結束了，這是我目前為止最慘的一單元，第十次作業強測20分，互測殺成狗……雖然都知道只關注分數沒有什么意義，我更應該去體會的是通過JML學習對於程序設計理念的認知，但是……心真的很痛。下面就進入單元總結：
1. JML語言理論基礎與工具鏈
1.1 JML語言是什么
參考課程組下發的《JML(Level 0)使用手冊》，JML語言的定義如下：
JML(Java Modeling Language)是用於對Java程序進行規格化設計的一種表示語言。JML是一種行為接口規格語言（Behavior Interface Specification Language，BISL），基於Larch方法構建。
也就是說，JML是一種對代碼語言的抽象——不同的語言有着不同的語法，而JML通過自己的規則對代碼進行了形式化的表述，一旦規格確定，除非涉及復雜的算法要求，實現代碼就變成了一個相對簡單的事情。
1.2 JML語言基本語法
JML的核心在於用表達式對規格進行描述，首先從常見的表達式說起，給人的感覺類似離散數學：
| 表達式 | 含義 |
|---|---|
| \result | 方法的返回值（非void類型） |
| \old(expr) | 表達式expr在方法執行前的取值 |
| \not_assigned(x, y, ...) | 括號中的變量是否在方法執行過程中未被賦值 |
| \not_modified(x, y, ...) | 限制括號中的變量在方法執行期間的取值未發生變化 |
| \forall | 全稱量詞 |
| \exists | 存在量詞 |
| \sum | 返回給定范圍內的表達式的和 |
| \product | 返回給定范圍內的表達式的連乘結果 |
| \max | 返回給定范圍內的表達式的最大值 |
| \min | 返回給定范圍內的表達式的最小值 |
| \num_of | 返回指定變量中滿足相應條件的取值個數 |
| <: | 子類型關系操作符 |
| <==> | 等價關系操作符 |
| ==> | 推理操作符 |
| \everything | 全集 |
| \nothing | 空集 |
表達式中容易錯的地方在於\old(expr)表達式，作為一般規則，任何情況下，都應該使用\old把關心的表達式取值整體括起來。
| 方法規格 | 含義 |
|---|---|
| requires | 表達的意思是“要求調用者確保P為真” |
| ensures | 表達的意思是“方法實現者確保方法執行返回結果一定滿足謂詞P的要求，即確保P為真” |
| assignable/modifiable | 副作用范圍限定，副作用指方法在執行過程中會修改對象的屬性數據或者類的靜態成員數據，從而給后續方法的執行帶來影響。assignble表示可賦值，而modifiable則表示可修改 |
| pure | 純粹訪問性的方法，不會對對象的狀態進行任何改變，也不需要提供輸入參數 |
| public normal_behavior | 正常功能，一般指輸入或方法關聯this對象的狀態在正常范圍內時所指向的功能。 |
| public exceptional_behavior | 與正常功能相對 |
| signals | 結構為signals (***Exception e) b_expr;，意思是當b_expr為true時，方法會拋出括號中給出的相應異常e |
最后是類型規格，指針對類或接口所設計的約束規則。
| 類型規格 | 含義 |
|---|---|
| invariant | 不變式，只針對可見狀態(即當下可見狀態)的取值進行約束 |
| constraint | 狀態變化約束，對前序可見狀態和當前可見狀態的關系進行約束 |
1.3 應用工具鏈情況
在網絡上查找JML工具鏈，搜索到的大多是OO博客的內容。工具主要包括OpenJML、JMLUnitNG等。
-
OpenJML: http://www.openjml.org/
-
JMLUnitNG: http://insttech.secretninjaformalmethods.org/software/jmlunitng/
在編寫三次作業時，我用的java版本是JDK13，無法使用相關工具鏈，於是也在作業中並沒有使用；撰寫本次博客時重新安裝了JRE1.8，具體使用在下面的部分描述。
2. SMT Solver驗證
參考了J哥的教程（https://www.cnblogs.com/pekopekopeko/p/12920417.html#4581709），進行OpenJML的組件SMT Solver驗證，文件樹如下：
PS G:\STUDY\BUAA-2020-OO\Week12> tree /F
卷 辦公 的文件夾 PATH 列表
卷序列號為 AA85-2D30
G:.
│ Group.java
│ Person.java
│
└─openjml-0.8.44-20200413
│ epl-v10.html
│ jml-reference-manual.pdf
│ jmlruntime.jar
│ jmlspecs.jar
│ LICENSE.rtf
│ openjml-template.properties
│ openjml.jar
│ OpenJMLUserGuide.pdf
│ VERSION_INFO
│
├─Solvers-linux
│ cvc4-1.6
│ z3-4.3.0
│ z3-4.3.1
│ z3-4.7.1
│
├─Solvers-macos
│ cvc4-1.6
│ z3-4.3.1
│ z3-4.5.0
│ z3-4.6.0
│ z3-4.7.1
│
└─Solvers-windows
cvc4-1.6.exe
z3-4.3.2.exe
z3-4.7.1.exe
先運行靜態驗證指令：java -jar .\openjml.jar -exec .\Solvers-windows\z3-4.7.1.exe -esc ..\Group.java，得到初步結果：
public class Person {
^
..\Group.java:34: 警告: A non-pure method is being called where it is not permitted: Person.isLinked(Person)
@ (\sum int j; 0 <= j && j < people.length && people[i].isLinked(people[j]); 1));
^
..\Group.java:40: 警告: A non-pure method is being called where it is not permitted: Person.isLinked(Person)
@ people[i].isLinked(people[j]); people[i].queryValue(people[j])));
^
..\Group.java:40: 警告: A non-pure method is being called where it is not permitted: Person.queryValue(Person)
..\Group.java:47: 警告: A non-pure method is being called where it is not permitted: Person.getCharacter()
@ temp.length == people.length && temp[0] == people[0].getCharacter();
^
..\Group.java:49: 警告: A non-pure method is being called where it is not permitted: Person.getCharacter()
@ temp[i] == temp[i-1].xor(people[i].getCharacter())) &&
^
..\Group.java:59: 警告: A non-pure method is being called where it is not permitted: Person.getAge()
^
..\Group.java:58: 錯誤: 不可比較的類型: int和INT#1
/*@ ensures \result == (people.length == 0? 0 :
^
其中, INT#1是交叉類型:
INT#1擴展Number,Comparable
@ (people[i].getAge() - getAgeMean()) * (people[i].getAge() - getAgeMean())) /
^
..\Group.java:64: 警告: A non-pure method is being called where it is not permitted: Person.getAge()
@ (people[i].getAge() - getAgeMean()) * (people[i].getAge() - getAgeMean())) /
^
..\Group.java:63: 錯誤: 不可比較的類型: int和INT#1
^
其中, INT#1是交叉類型:
INT#1擴展Number,Comparable
3 個錯誤
8 個警告
報錯和警告主要有兩種，在不允許的地方調用非純方法，以及不可比較的類型（貌似是不能識別三目運算符？），動態驗證的信息就更多了。
總之我感覺看着結果雲里霧里的，SMT Solver目前好像也無法對exist等進行驗證，不過作者一直在更新，相信下一屆的同學們可以享受到更加舒適的SMT Solver的！
3. JMLUnitNG/JMLUnit自動生成測試用例
辛辛苦苦以10KB/S的速度下載下來，一運行傻了——
到百度求助，表示版本太低，然而我已經下載了官網最新的1.8版本……另外發現這中間似乎插了句人話：錯誤: 非法的類型開始 value = new ArrayList<>();，感情必須要寫成value = new ArrayList<Integer>();的形式？這也太OUT了吧……
之后又出現了群里提到的神秘的++，觸發了JmlInternalError,更加迷惑了。
org.jmlspecs.openjml.JmlInternalError: The operation symbol ++ for type java.lang.Object could not be resolved
簡要分析
最后我折騰了很久還是不行……運行完什么結果也沒有……我也很疑惑為什么運行SMT Solver時就相對順風順水但JMLUnitNG怎么整都不行（對幫我一起慘兮兮找問題的PB深表歉意）。因為我的電腦不能生成，所以就看了很多同學的博客，這里引用@VOIDMalkuth的測試結果：
從同學們的結果來看，JMLUnitNG自動生成的樣例可以檢測到一定的錯誤，對於INT數據測試了極端情況等與實際應用不符合的數據輸入，要成為真正有用的工具，還有很長的路要走……
4. 架構設計梳理與模型構建策略分析
4.1 第九次作業
UML類圖如下：
本次作業只要對着規格就能完成大部分任務，架構上使用的MyPerson、MyNetwork均繼承課程組所給的接口。
需要考慮算法實現的是isCircle，我采用了BFS廣度優先搜索，從每個Person內調出鄰接表搜索，復雜度為O(N+E)。
4.2 第十次作業
UML類圖如下：
第十次作業與第九次作業相比新增了Group，在MyNetwork中調用MyGroup。我直到周四才開始動筆，此時同學們已經把雷區排得差不多了……於是在Group的方法上我采用了緩存法的形式。需要特別注意的是緩存法在addRelation時也要更新緩存，我采用的方式為為Group增加更新的檢索方法：
public void addRelation(int id1, int id2, int value) {
if (people.containsKey(id1) && people.containsKey(id2)) {
relationSum += 2;
valueSum += (2 * value);
}
}
而在計算方差時，則出現了過度化簡導致誤差的問題，同樣需要注意。
另外需要注意的是初始化問題，HashMap默認容量為16，當當前的size超過容量×常數時就會進行擴容，而擴容操作需要耗費的時間較多，因此我直接將關系表初始化為8192容量。
4.3 第十一次作業
UML類圖如下：
第十一次作業對算法的考察增加了：
-
在queryBlockSum我采用了並查集，進而isCircle的復雜度降至O(1)；
-
queryMinPath則采用了堆優化的Dijkstra，沒有手寫堆，而是采用自帶的PriorityQueue進行維護；
-
queryStrongLink原本在想要不要學tarjan，但發現助教給的標程復雜度很寬容，所以就用了兩步BFS，特判第一次BFS找到的為直連路徑的情況，我寫了一個忽略某點的BFS函數：
private boolean searchIgnore(int id1, int id2, int ignore) {
if (id1 == ignore || id2 == ignore || id1 == id2) {
// err("meet id1 == ignore || id2 == ignore || id1 == id2");
return false;
}
HashSet<Integer> visited = new HashSet<>(1024);
Queue<Integer> queue = new LinkedList<>();
queue.add(id1);
while (!queue.isEmpty()) {
int currentId = queue.poll();
if (visited.contains(currentId)) {
continue;
}
ArrayList<Integer> points = ((MyPerson) getPerson(currentId)).getAcquaintance();
for (Integer i : points) {
if (i == id2) {
// err("Succeed! searchIgnore");
return true;
} else if (!visited.contains(i) && i != ignore) {
queue.offer(i);
// err("queue update to " + queue);
}
}
visited.add(currentId);
// err("point " + currentId + " has been searched");
}
return false;
}
如果第一次找到的路徑長度為2，那么就遍歷起點的鄰接表，找到一條不經過起點就能到終點的路徑就返回成功；否則依次忽略第一次BFS路徑中的點，如果每次都能找到路徑就返回成功。最后在研討課也學了tarjan，在求割點的過程中求出所有雙連通分量，進而判斷點雙。
這樣的結構導致MyNetwork非常臃腫，我因此將並查集、堆優化的Dijkstra單獨抽象為一個類。
5. 代碼bug和修復情況
第九次、第十一次作業均未出現Bug。
第十次作業
第九次作業整體相對簡單，也就讓我放松了警惕，在第十次作業時，我最后改了一行代碼，卻忘了測試：
return (HashSet<Integer>) acquaintance.keySet();
就是這行代碼，讓我直接RE了大部分測試點……在編寫時想當然地以為HashMap的KeySet可以用強制類型轉換為HashSet，之后又沒有做哪怕一次對isCircle的測試，於是強測直接爆炸……在互測屋里，看到了沒有除零直接RE的同學；看到了緩存更新不及時的同學，看到了好多Bug一起犯的同學……是一次難忘的體驗。
第十一次作業
在第十一次作業，吸取了第十次作業的慘痛教訓，用Junit對新加入的函數進行單元測試，優化算法，沒有出現Bug。
JML作為一種統一的規格化語言，在對代碼進行了形式化的表述的同時，也給機器理解程序提供了一種可能性。
雖然從目前來看，JML相關的工具或是陳舊不堪，或是Bug滿天飛，而撰寫規格甚至比寫程序還要復雜得多，比如對於一些Contains方法，JML的表述雖然嚴謹，但為人的閱讀與理解提供了更大的負擔。