OO_Unit 3 JML規格化設計總結

JML語言概述（Level 0）

概念定義

  JML(Java Modeling Language)是用于對Java程式進行規格化設計的一種表示語言。JML是一種行為接口規格語言（Behavior Interface Specification Language，BISL），基于Larch方法建構。

　　由上述定義可知，JML誕生的初衷就是對代碼進行形式化描述，試圖在用自然語言表達的需求與用代碼語言表達的實作之間建構一座橋梁，一方面可以消除自然語言可能存在的歧義與模糊，另一方面也可以屏蔽具體的代碼實作，實作另一種形式的抽象。

JML基本文法

表達式	含義
\result	方法的傳回值（非void類型）
\old( expr )	expr 在方法執行前的取值
\not_assigned(x, y, ...)	括号中的變量是否在方法執行過程中未被指派
\not_modified(x, y, ...)	限制括号中的變量在方法執行期間的取值未發生變化
(\forall T x; R(x); P(x))	全稱量詞
(\exists T x; R(x); P(x))	存在量詞
(\sum T x; R(x); expr	傳回給定範圍内的表達式的和
(\max T x; R(x); expr	傳回給定範圍内的表達式的最大值
(\min T x; R(x); expr	傳回給定範圍内的表達式的最小值
<==>	等價操作符
==>	蘊含操作符
\nothing	空集

方法規格
requires	前置條件，表達的意思是“要求調用者確定P為真”。
ensures	後置條件，表達的意思是“方法實作者確定方法執行傳回結果一定滿足謂詞P的要求，即確定P為真”。
assignable	副作用指方法在執行過程中會修改對象的屬性資料或者類的靜态成員資料，進而給後續方法的執行帶來影響。
public normal_behavior	正常功能，一般指輸入或方法關聯this對象的狀态在正常範圍内時所指向的功能。
public exceptional_behavior	異常功能，與正常功能相對
signals	結構為 signals (***Exception e) b_expr; 表示抛出異常

類型規格
invariant	不變式（invariant）是要求在所有可見狀态下都必須滿足的特性
constraint	對前序可見狀态和目前可見狀态的關系進行限制

JML工具鍊

　　通過上文，我們已經看到，JML在形式化描述上就語言規範來說已經非常完善了，可以說是把謂詞邏輯的那一套完完整整地搬了過來，很好地保證了嚴謹性，也相對代碼要更加易讀一些。

　　但是！！！這裡面有兩個問題。

　　首先，JML并不對方法的複雜度有任何限制。于是我們可以看到，在某些方法裡，比如

addRelation()

，方法本身複雜度并不高，但JML卻特别長，讓人看得很不耐煩，還不如直接看代碼來得簡潔明了；而對另一些場景，比如傳回的對象比較複雜不是一個簡單基本類型的話，就會出現關鍵字嵌套的情況，這就使得單條JML語句的複雜度也會很高，還不如拆成多行的代碼看的清楚。特别地，我尤其對于如何用JML來寫遞歸感到好奇，畢竟我依稀記得一階邏輯似乎是不完備的哦？

　　是以這時候可能就有人會說，JML不是寫給程式員看的，程式員看代碼就好了。那麼問題又來了，JML的理想服務對象是誰呢？是掌握謂詞邏輯的産品經理？不過，如果真是這樣，那我也可以接受。但似乎，JML工具鍊卻為我們指出了另一個潛在服務對象：機器。

　　簡單來說，JML工具鍊似乎就是為了能夠讓機器基于規格以形式化驗證的方式來代替人類對方法進行完備的測試而誕生的。怎麼說呢，光是看這句話就挺心疼人家機器的——這要求也忒高了吧。别說AI了，就是人，你能保證他做到絕對完備嗎？他能考慮到一個顧客進來問現在幾點了這種操作嗎？

　　為什麼說讓機器來代替人類進行測試是不現實的呢？很簡單，因為機器也是人造的，要想實作基于形式化語言的可泛化測試，而不基于具體的需求本身，就意味着你必須要僅僅憑借上面的那些關鍵字，就能枚舉出它們所有潛在可能組合，而且這個組合中的每一種情況所包含的測試樣例還必須是有窮，有階梯性的。你覺得，如果我随手寫一行一階謂詞邏輯，你有信心告訴我這玩意的所有邊界情況嗎？更何況，你知道的隻是一個謂詞集合呢？

　　或許，可能開發者的初衷是隻要我把每個前置條件與後置條件還有副作用寫清楚，機器針對不同的behavior生成不同的測試樣例這樣。但是，需要特别指出的是，同一個requires語句下的不同的邊界資料才是構造測試的關鍵，特别是面對非歐拓撲模型（很不巧，我們的Unit3就長這樣）。

　　是以啊，别難為人家開發者和機器了。指望靠JML工具實作自動測試還是等到強AI出來并且還沒來得及毀滅人類的時候吧。

　　吐槽到此結束，對于JML工具鍊的具體介紹，請參見這個傳送門。下文僅涉及openjml與JMLUnitNG的極少數方法。

OpenJML形式化驗證

　　openjml是目前相對較為完備的一套形式化驗證Kit，但是遺憾的是它在jdk1.8之後就停止更新了，于是對于我這個一開始用jdk12.0的人就很不友好（上來就把人勸退的那種）。

　　下面我們以task2中的執行個體化類RealNetwork為例，示範該工具的使用與其相應結果。假設IDEA項目所在目錄為$PATH。

Parsing and Type checking

　　運作指令：

java -jar openjml.jar -check $PATH\src\network\RealNetwork.java -sourcepath $PATH\src -encoding utf-8      

　　程式正常傳回，無任何報錯資訊。

Extended Static Checking

java -jar openjml.jar -prover z3_4_7 -exec .\Solvers-windows\z3-4.7.1.exe -esc $PATH\src\network\RealNetwork.java -sourcepath $PATH\src -encoding utf-8      

　　其中，-prover參數用于指定Solver類型，-exec參數用于指定Solver可執行程式，-esc參數指定檢查類型為Extended Static Checking。

　　傳回結果包含3個錯誤資訊和100條警告，經過簡單歸類後，大緻為以下幾類：

注: Not implemented for static checking: ensures clause containing \not_assigned

錯誤: An internal JML error occurred, possibly recoverable. Please report the bug with as much information as you can. Reason: Internal exception: class java.lang.NullPointerException

警告: The prover cannot establish an assertion (ExceptionalPostcondition:

警告: Associated declaration:

警告: The prover cannot establish an assertion (UndefinedCalledMethodPrecondition:

警告: Precondition conjunct is false:

錯誤: ESC could not be attempted because of a failure in typechecking or AST transformation: queryNameRank

至于為什麼隻找到2個錯誤，我也不知道

　　總之，給人一種不明覺厲的感覺吧。（輸出資訊有近450行，我就不放了）

Runtime Assertion Checking

java -jar openjml.jar -rac $PATH\src\network\RealNetwork.java -sourcepath $PATH\src -encoding utf-8      

　　其中，-rac參數指定檢查類型為Runtime Assertion Checking。

　　運作結果如下：

1 The operation symbol ++ for type java.lang.Object could not be resolved
  2 org.jmlspecs.openjml.JmlInternalError: The operation symbol ++ for type java.lang.Object could not be resolved
  3         at org.jmlspecs.openjml.JmlTreeUtils.findOpSymbol(JmlTreeUtils.java:291)
  4         at org.jmlspecs.openjml.JmlTreeUtils.findOpSymbol(JmlTreeUtils.java:282)
  5         at org.jmlspecs.openjml.JmlTreeUtils.makeUnary(JmlTreeUtils.java:739)
  6         at com.sun.tools.javac.comp.JmlAttr.createRacExpr(JmlAttr.java:4465)
  7         at org.jmlspecs.openjml.ext.QuantifiedExpressions$QuantifiedExpression.typecheck(QuantifiedExpressions.java:214)
  8         at com.sun.tools.javac.comp.JmlAttr.visitJmlQuantifiedExpr(JmlAttr.java:4070)
  9         at org.jmlspecs.openjml.JmlTree$JmlQuantifiedExpr.accept(JmlTree.java:2685)
 10         at com.sun.tools.javac.comp.Attr.attribTree(Attr.java:577)
 11         at com.sun.tools.javac.comp.Attr.visitParens(Attr.java:2995)
 12         at com.sun.tools.javac.tree.JCTree$JCParens.accept(JCTree.java:1661)
 13         at com.sun.tools.javac.comp.Attr.attribTree(Attr.java:577)
 14         at com.sun.tools.javac.comp.Attr.attribExpr(Attr.java:619)
 15         at com.sun.tools.javac.comp.JmlAttr.attribExpr(JmlAttr.java:6209)
 16         at com.sun.tools.javac.comp.JmlAttr.visitJmlMethodClauseExpr(JmlAttr.java:3117)
 17         at org.jmlspecs.openjml.JmlTree$JmlMethodClauseExpr.accept(JmlTree.java:2332)
 18         at com.sun.tools.javac.comp.JmlAttr.visitJmlSpecificationCase(JmlAttr.java:3361)
 19         at org.jmlspecs.openjml.JmlTree$JmlSpecificationCase.accept(JmlTree.java:2837)
 20         at com.sun.tools.javac.comp.JmlAttr.visitJmlMethodSpecs(JmlAttr.java:3423)
 21         at org.jmlspecs.openjml.JmlTree$JmlMethodSpecs.accept(JmlTree.java:2539)
 22         at com.sun.tools.javac.comp.JmlAttr.checkMethodSpecsDirectly(JmlAttr.java:1560)
 23         at com.sun.tools.javac.comp.JmlAttr.visitMethodDef(JmlAttr.java:1121)
 24         at com.sun.tools.javac.comp.JmlAttr.visitJmlMethodDecl(JmlAttr.java:6053)
 25         at org.jmlspecs.openjml.JmlTree$JmlMethodDecl.accept(JmlTree.java:1261)
 26         at com.sun.tools.javac.comp.Attr.attribTree(Attr.java:577)
 27         at com.sun.tools.javac.comp.Attr.attribStat(Attr.java:646)
 28         at com.sun.tools.javac.comp.JmlAttr.attribStat(JmlAttr.java:558)
 29         at com.sun.tools.javac.comp.Attr.attribClassBody(Attr.java:4378)
 30         at com.sun.tools.javac.comp.JmlAttr.attribClassBody(JmlAttr.java:536)
 31         at com.sun.tools.javac.comp.Attr.attribClass(Attr.java:4286)
 32         at com.sun.tools.javac.comp.JmlAttr.attribClass(JmlAttr.java:414)
 33         at com.sun.tools.javac.comp.JmlAttr.completeTodo(JmlAttr.java:492)
 34         at com.sun.tools.javac.comp.JmlAttr.attribClass(JmlAttr.java:458)
 35         at com.sun.tools.javac.comp.Attr.attribClass(Attr.java:4215)
 36         at com.sun.tools.javac.comp.Attr.attrib(Attr.java:4190)
 37         at com.sun.tools.javac.main.JavaCompiler.attribute(JavaCompiler.java:1258)
 38         at com.sun.tools.javac.main.JmlCompiler.attribute(JmlCompiler.java:479)
 39         at com.sun.tools.javac.main.JavaCompiler.compile2(JavaCompiler.java:898)
 40         at com.sun.tools.javac.main.JmlCompiler.compile2(JmlCompiler.java:712)
 41         at com.sun.tools.javac.main.JavaCompiler.compile(JavaCompiler.java:867)
 42         at com.sun.tools.javac.main.Main.compile(Main.java:553)
 43         at com.sun.tools.javac.main.Main.compile(Main.java:410)
 44         at org.jmlspecs.openjml.Main.compile(Main.java:581)
 45         at com.sun.tools.javac.main.Main.compile(Main.java:399)
 46         at com.sun.tools.javac.main.Main.compile(Main.java:390)
 47         at org.jmlspecs.openjml.Main.execute(Main.java:417)
 48         at org.jmlspecs.openjml.Main.execute(Main.java:375)
 49         at org.jmlspecs.openjml.Main.execute(Main.java:362)
 50         at org.jmlspecs.openjml.Main.main(Main.java:334)
 51 錯誤: An internal JML error occurred, possibly recoverable.  Please report the bug with as much information as you can.
 52   Reason: com.sun.tools.javac.code.Type$BottomType cannot be cast to com.sun.tools.javac.code.Type$ArrayType
 53   java.lang.ClassCastException: com.sun.tools.javac.code.Type$BottomType cannot be cast to com.sun.tools.javac.code.Type$ArrayType
 54         at org.jmlspecs.openjml.JmlTreeUtils.copyArray(JmlTreeUtils.java:1546)
 55         at org.jmlspecs.openjml.esc.JmlAssertionAdder.visitJmlMethodInvocation(JmlAssertionAdder.java:15456)
 56         at org.jmlspecs.openjml.JmlTree$JmlMethodInvocation.accept(JmlTree.java:2229)
 57         at com.sun.tools.javac.tree.TreeScanner.scan(TreeScanner.java:49)
 58         at org.jmlspecs.openjml.vistors.JmlTreeScanner.scan(JmlTreeScanner.java:67)
 59         at org.jmlspecs.openjml.esc.JmlAssertionAdder.convertExpr(JmlAssertionAdder.java:1504)
 60         at org.jmlspecs.openjml.esc.JmlAssertionAdder.visitParens(JmlAssertionAdder.java:10686)
 61         at com.sun.tools.javac.tree.JCTree$JCParens.accept(JCTree.java:1661)
 62         at com.sun.tools.javac.tree.TreeScanner.scan(TreeScanner.java:49)
 63         at org.jmlspecs.openjml.vistors.JmlTreeScanner.scan(JmlTreeScanner.java:67)
 64         at org.jmlspecs.openjml.esc.JmlAssertionAdder.convertExpr(JmlAssertionAdder.java:1504)
 65         at org.jmlspecs.openjml.esc.JmlAssertionAdder.visitBinary(JmlAssertionAdder.java:11862)
 66         at com.sun.tools.javac.tree.JCTree$JCBinary.accept(JCTree.java:1785)
 67         at com.sun.tools.javac.tree.TreeScanner.scan(TreeScanner.java:49)
 68         at org.jmlspecs.openjml.vistors.JmlTreeScanner.scan(JmlTreeScanner.java:67)
 69         at org.jmlspecs.openjml.esc.JmlAssertionAdder.convertExpr(JmlAssertionAdder.java:1504)
 70         at org.jmlspecs.openjml.esc.JmlAssertionAdder.convertJML(JmlAssertionAdder.java:1647)
 71         at org.jmlspecs.openjml.esc.JmlAssertionAdder.convertJML(JmlAssertionAdder.java:1664)
 72         at org.jmlspecs.openjml.esc.JmlAssertionAdder.convertNoSplit(JmlAssertionAdder.java:1685)
 73         at org.jmlspecs.openjml.esc.JmlAssertionAdder.visitJmlQuantifiedExpr(JmlAssertionAdder.java:16233)
 74         at org.jmlspecs.openjml.JmlTree$JmlQuantifiedExpr.accept(JmlTree.java:2685)
 75         at com.sun.tools.javac.tree.TreeScanner.scan(TreeScanner.java:49)
 76         at org.jmlspecs.openjml.vistors.JmlTreeScanner.scan(JmlTreeScanner.java:67)
 77         at org.jmlspecs.openjml.esc.JmlAssertionAdder.convertExpr(JmlAssertionAdder.java:1504)
 78         at org.jmlspecs.openjml.esc.JmlAssertionAdder.visitParens(JmlAssertionAdder.java:10686)
 79         at com.sun.tools.javac.tree.JCTree$JCParens.accept(JCTree.java:1661)
 80         at com.sun.tools.javac.tree.TreeScanner.scan(TreeScanner.java:49)
 81         at org.jmlspecs.openjml.vistors.JmlTreeScanner.scan(JmlTreeScanner.java:67)
 82         at org.jmlspecs.openjml.esc.JmlAssertionAdder.convertExpr(JmlAssertionAdder.java:1504)
 83         at org.jmlspecs.openjml.esc.JmlAssertionAdder.convertJML(JmlAssertionAdder.java:1647)
 84         at org.jmlspecs.openjml.esc.JmlAssertionAdder.convertJML(JmlAssertionAdder.java:1664)
 85         at org.jmlspecs.openjml.esc.JmlAssertionAdder.convertNoSplit(JmlAssertionAdder.java:1685)
 86         at org.jmlspecs.openjml.esc.JmlAssertionAdder.visitJmlQuantifiedExpr(JmlAssertionAdder.java:16233)
 87         at org.jmlspecs.openjml.JmlTree$JmlQuantifiedExpr.accept(JmlTree.java:2685)
 88         at com.sun.tools.javac.tree.TreeScanner.scan(TreeScanner.java:49)
 89         at org.jmlspecs.openjml.vistors.JmlTreeScanner.scan(JmlTreeScanner.java:67)
 90         at org.jmlspecs.openjml.esc.JmlAssertionAdder.convertExpr(JmlAssertionAdder.java:1504)
 91         at org.jmlspecs.openjml.esc.JmlAssertionAdder.visitParens(JmlAssertionAdder.java:10686)
 92         at com.sun.tools.javac.tree.JCTree$JCParens.accept(JCTree.java:1661)
 93         at com.sun.tools.javac.tree.TreeScanner.scan(TreeScanner.java:49)
 94         at org.jmlspecs.openjml.vistors.JmlTreeScanner.scan(JmlTreeScanner.java:67)
 95         at org.jmlspecs.openjml.esc.JmlAssertionAdder.convertExpr(JmlAssertionAdder.java:1504)
 96         at org.jmlspecs.openjml.esc.JmlAssertionAdder.convertJML(JmlAssertionAdder.java:1647)
 97         at org.jmlspecs.openjml.esc.JmlAssertionAdder.addPostConditions(JmlAssertionAdder.java:4758)
 98         at org.jmlspecs.openjml.esc.JmlAssertionAdder.convertMethodBodyNoInit(JmlAssertionAdder.java:1195)
 99         at org.jmlspecs.openjml.esc.JmlAssertionAdder.visitJmlMethodDecl(JmlAssertionAdder.java:15127)
100         at org.jmlspecs.openjml.JmlTree$JmlMethodDecl.accept(JmlTree.java:1261)
101         at com.sun.tools.javac.tree.TreeScanner.scan(TreeScanner.java:49)
102         at org.jmlspecs.openjml.vistors.JmlTreeScanner.scan(JmlTreeScanner.java:67)
103         at org.jmlspecs.openjml.esc.JmlAssertionAdder.visitJmlClassDecl(JmlAssertionAdder.java:13784)
104         at org.jmlspecs.openjml.JmlTree$JmlClassDecl.accept(JmlTree.java:1174)
105         at com.sun.tools.javac.tree.TreeScanner.scan(TreeScanner.java:49)
106         at org.jmlspecs.openjml.vistors.JmlTreeScanner.scan(JmlTreeScanner.java:67)
107         at org.jmlspecs.openjml.esc.JmlAssertionAdder.convert(JmlAssertionAdder.java:1414)
108         at com.sun.tools.javac.main.JmlCompiler.rac(JmlCompiler.java:610)
109         at com.sun.tools.javac.main.JmlCompiler.desugar(JmlCompiler.java:454)
110         at com.sun.tools.javac.main.JavaCompiler.compile2(JavaCompiler.java:898)
111         at com.sun.tools.javac.main.JmlCompiler.compile2(JmlCompiler.java:712)
112         at com.sun.tools.javac.main.JavaCompiler.compile(JavaCompiler.java:867)
113         at com.sun.tools.javac.main.Main.compile(Main.java:553)
114         at com.sun.tools.javac.main.Main.compile(Main.java:410)
115         at org.jmlspecs.openjml.Main.compile(Main.java:581)
116         at com.sun.tools.javac.main.Main.compile(Main.java:399)
117         at com.sun.tools.javac.main.Main.compile(Main.java:390)
118         at org.jmlspecs.openjml.Main.execute(Main.java:417)
119         at org.jmlspecs.openjml.Main.execute(Main.java:375)
120         at org.jmlspecs.openjml.Main.execute(Main.java:362)
121         at org.jmlspecs.openjml.Main.main(Main.java:334)
122 $PATH\src\network\RealNetwork.java:193: 注: Runtime assertion checking is not implemented for this type or number of declarations in a quantified expression
123             return groups.get(id).getRelationSum();
124                                         ^
125 $PATH\src\network\RealNetwork.java:248: 注: Runtime assertion checking is not implemented for this type or number of declarations in a quantified expression
126         Graph<AbstractPerson> newGraph = new Graph<>(personSet);
127       ^
128 $PATH\src\network\RealNetwork.java:249: 注: Runtime assertion checking is not implemented for this type or number of declarations in a quantified expression
129         return newGraph.isReachable(oriPerson, dstPerson);
130                        ^
131 $PATH\src\com\oocourse\spec2\main\Group.java:33: 注: Runtime assertion checking is not implemented for this type or number of declarations in a quantified expression
132       @          (\sum int j; 0 <= j && j < people.length && people[i].isLinked(people[j]); 1));
133                   ^
134 $PATH\src\com\oocourse\spec2\main\Group.java:38: 注: Runtime assertion checking is not implemented for this type or number of declarations in a quantified expression
135       @          (\sum int j; 0 <= j && j < people.length &&
136                   ^
137 $PATH\src\com\oocourse\spec2\main\Group.java:45: 注: Runtime assertion checking is not implemented for this type or number of declarations in a quantified expression
138       @ ensures (\exists BigInteger[] temp;
139                  ^
140 1 個錯誤      

View Code

　　目測似乎是openjml程式内部什麼地方出現了一些奇怪的bug，不是很清楚，因為沒有去看源碼。但有一點應該可以确定，那就是這個工具的開發者盡早棄坑是灰常明智的選擇。

JMLUnitNG測試

　　本測試針對RealGroup類，依次運作以下3條指令：

java -jar ..\jmlunitng.jar network\RealGroup.java -cp .
javac -cp ".;..\jmlunitng.jar" network\RealGroup_JML_Test.java
java -cp ".;..\jmlunitng.jar" network.RealGroup_JML_Test      

　　所得結果如下：

1 [TestNG] Running:
 2 Command line suite
 3 
 4 Failed: racEnabled()
 5 Passed: constructor RealGroup(-2147483648)
 6 Passed: constructor RealGroup(0)
 7 Passed: constructor RealGroup(2147483647)
 8 Failed: <<network.RealGroup@80000000>>.addPerson(null)
 9 Failed: <<network.RealGroup@0>>.addPerson(null)
10 Failed: <<network.RealGroup@7fffffff>>.addPerson(null)
11 Passed:<<network.RealGroup@80000000>>.equals(null)
12 Passed:<<network.RealGroup@0>>.equals(null)
13 Passed:<<network.RealGroup@7fffffff>>.equals(null)
14 Passed: <<network.RealGroup@80000000>>.equals(java.lang.Object@574caa3f)
15 Passed: <<network.RealGroup@0>>.equals(java.lang.Object@64cee07)
16 Passed: <<network.RealGroup@7fffffff>>.equals(java.lang.Object@1761e840)
17 Passed: <<network.RealGroup@80000000>>.getAgeMean()
18 Passed: <<network.RealGroup@0>>.getAgeMean()
19 Passed: <<network.RealGroup@7fffffff>>.getAgeMean()
20 Passed: <<network.RealGroup@80000000>>.getAgeVar()
21 Passed: <<network.RealGroup@0>>.getAgeVar()
22 Passed: <<network.RealGroup@7fffffff>>.getAgeVar()
23 Passed: <<network.RealGroup@80000000>>.getConflictSum()
24 Passed: <<network.RealGroup@0>>.getConflictSum()
25 Passed: <<network.RealGroup@7fffffff>>.getConflictSum()
26 Passed: <<network.RealGroup@80000000>>.getId()
27 Passed: <<network.RealGroup@0>>.getId()
28 Passed: <<network.RealGroup@7fffffff>>.getId()
29 Passed: <<network.RealGroup@80000000>>.getPeopleSum()
30 Passed: <<network.RealGroup@0>>.getPeopleSum()
31 Passed: <<network.RealGroup@7fffffff>>.getPeopleSum()
32 Passed: <<network.RealGroup@80000000>>.getRelationSum()
33 Passed: <<network.RealGroup@0>>.getRelationSum()
34 Passed: <<network.RealGroup@7fffffff>>.getRelationSum()
35 Passed: <<network.RealGroup@80000000>>.getValueSum()
36 Passed: <<network.RealGroup@0>>.getValueSum()
37 Passed: <<network.RealGroup@7fffffff>>.getValueSum()
38 Passed: <<network.RealGroup@80000000>>.hasPerson(null)
39 Passed: <<network.RealGroup@0>>.hasPerson(null)
40 Passed: <<network.RealGroup@7fffffff>>.hasPerson(null)
41 Passed: <<network.RealGroup@80000000>>.hashCode()
42 Passed: <<network.RealGroup@0>>.hashCode()
43 Passed: <<network.RealGroup@7fffffff>>.hashCode()
44 Passed: <<network.RealGroup@80000000>>.updateRelation(-2147483648)
45 Passed: <<network.RealGroup@0>>.updateRelation(-2147483648)
46 Passed: <<network.RealGroup@7fffffff>>.updateRelation(-2147483648)
47 Passed: <<network.RealGroup@80000000>>.updateRelation(0)
48 Passed: <<network.RealGroup@0>>.updateRelation(0)
49 Passed: <<network.RealGroup@7fffffff>>.updateRelation(0)
50 Passed: <<network.RealGroup@80000000>>.updateRelation(2147483647)
51 Passed: <<network.RealGroup@0>>.updateRelation(2147483647)
52 Passed: <<network.RealGroup@7fffffff>>.updateRelation(2147483647)
53 
54 ======================================
55 Command line suite
56 
57 Total tests run: 49, Failures: 4, Skips: 0
58 
59 ======================================      

　　可以看到，所有的測試該通過的都通過了，沒通過的那幾個是因為

addPerson()

本來就沒指望輸入會有null的情況。但是另一方面，仔細觀察它的這些測試樣例，我們不難發現，它好像測了個寂寞？

　　首先，方法與方法之間的測試是割裂的，jmlunitNG顯然并不具備構造複合測試用例的能力，也就不可能适應的了動态更新緩存的場景，而這正是RealGroup類為了性能優化而做出的改進之一。此外，作為面向對象的語言，測試卻是一副面向過程的做派。C可忍，J不可忍！

　　其次，這貨對于測試邊界資料的定義顯然非常可愛：基本資料類型就直接取邊界資料（MAX_VALUE, MIN_VALUE, 0）,自定義對象就來個

null

，真的是很傻很天真，蠢萌蠢萌的那種。隻是可惜了，程式員的世界可沒你想象的那麼美好，還要加油啊，少年。

模型架構設計

　　本單元的核心任務是建構一個社交網絡模型，對于這一模型，需要在基于規格實作的準确性基礎上做到盡可能高的性能優化。同時我們注意到，社交網絡的本質是一個圖結構，本單元則是權重無向圖，是以在架構上，一個基本的出發點就是做到算法層與應用層的最大解耦，算法層負責性能的優化，應用層負責進行簡單的初始化與異常判斷。這樣做的結果，不僅僅是做到了降低類的複雜度，同時也提高了算法與模型的複用性，畢竟誰知道以後會不會再用到呢，就讓輪子一直是輪子好了。

　　于是乎，我在底層的模型類中，大量使用了泛型與内部類，參考HashMap的實作，将Unit3中用到的Graph, UnionFindSet, Heap乃至均值方差的動态更新都單獨拎了出來構造類，并保證在之後的作業中可以随時複用之。

　　整體架構如下圖所示：

　　這張看的可能反而有點亂，再來個清楚的：

│  Main.java
│
├─com
│  └─oocourse
│      └─spec3
│          ├─exceptions
│          │      EqualGroupIdException.java
│          │      EqualPersonIdException.java
│          │      EqualRelationException.java
│          │      GroupIdNotFoundException.java
│          │      PersonIdNotFoundException.java
│          │      RelationNotFoundException.java
│          │
│          └─main
│                  Group.java
│                  Network.java
│                  Person.java
│                  Runner.java
│
├─network
│      AbstractGroup.java
│      AbstractPerson.java
│      RealGroup.java
│      RealNetwork.java
│      RealPerson.java
│
└─utils
   Graph.java
   Heap.java
   HeapNode.java
   Node.java
   Pair.java
   StatKit.java
   UnionFindSet.java      

　　可以看到，所有的模型類全部被放到了utils包中，且由于采用泛型的思想，是以其複用性極高，而不隻是限于本次作業。但是，這在一定程度上也帶來了一些隐患，因為在某種意義上，調用者與被調用者的關系，就像是需求方與實作方之間的關系。如果出現了上層以為下層考慮到了，下層以為上層給它屏蔽了這樣的尴尬情況的話，就有點贻笑大方了。

　　除此之外，為了在不改變課題組提供的代碼的前提下将模型解耦，我專門設計了

Abstract*.java

接口，用于封裝一些原接口中未聲明但需要的方法，以及将Graph對應的節點Node特征在不經過

`Person

接口的前提下令

RealPerson.java

繼承之，進而減少不必要的Graph的備援存儲，而是利用Node提供的

getNeighbors()

方法以鄰接表的形式對節點進行通路和周遊。

算法分析

　　Task3中，由于涉及到對連通性、最短路、割點等内容的應用，是以必要的算法是必不可少的。由于點連通分量與割點我也是第一次接觸其具體應用，是以也經曆了一個逐漸疊代的過程，在此将所有嘗試的算法列舉如下：

假設節點數為n，邊數為m

isCircle(): 采用并查集實作（路徑壓縮+秩優化），攤還複雜度為，其中為阿克曼函數的逆函數，現實中值一般不超過4

queryMinPath(): 采用Dijkstra算法實作，最終版由于使用了堆優化，是以複雜度降為，尤其适合本單元的稀疏圖

isStrongLinked(): 最終版采用tarjan算法，複雜度為O(n+m)，通過将DFS中的邊壓棧來保證不會漏掉割點

測試與bug分析

　　Unit3對我而言有着特殊的意義，這種意義很大程度上不是因為jml，不是因為算法，而是因為測試。它為我提供了一個契機，讓我重新去思考測試的意義，思考究竟怎樣的測試是有效的，怎樣的測試是合理的。

　　首先，測試應該包含以下三個部分：

1. 構造測試樣例
2. 批處理擷取使用者程式輸出
3. 檢驗輸出正确性

  這三部分，對于不同的場景，挑戰性各不相同。

  對于第一單元，由于課程組提供了标準輸出scipy與基于抽樣的正确性檢測方法，是以2和3部分的難度可以忽略不計，關鍵在于如何構造測試樣例。而對于表達式這種模型，整體上規律還是很強的（畢竟可以寫成正則），是以大規模随機就可以有很好的效果，再加上一些極邊界情況的資料，正确性就能夠覆寫個十之八九了。

  但即使如此，自己在task2的時候還是錯了一個點，原因就是沒有考慮到不合法的空白符。試想如果每一個測試點都加上這麼一個不合法的空白符，那麼自己task2不就直接0分了？

  對于第二單元，由于是強制線上，是以第2部分的難度陡然增加，畢竟單純的循環等待效率實在太低，這就需要我們使用多程序并發的方式進行測試；但是由于乘客的請求資料結構也非常之簡單，并且輸出可以通過流程驗證來檢查整個電梯系統的狀态遷移與輸入之間是否合法，是以第1部分與第3部分的難度并不高，是以就還算OK。

　　但是因為使用者程式也是多線程的，而多線程本身具有一些非常隐蔽的如死鎖一樣的極難複現的bug，是以這也客觀上增加了100%debug的難度。可以說，在多線程的世界裡，你永遠無法保證自己的程式是絕對正确的。

　　那麼現在，故事兜兜轉轉來到了第三單元。

　　第三單元的任務具有什麼特征呢？

　　首先，由于是社交網絡的模拟，是以方法種類很多，這就展現在輸入種類的極大豐富上；其次，單方法的内容相對簡單，基本可以靠人眼判斷。但是，這些方法之間的組合所誕生的可能性卻很多，是以乍一眼看去往往會給人一種無從下手的感覺。最後，在結果的判定下，由于不存在第一單元的标程與第二單元的流程驗證，是以總體正确性很難進行判斷。

　　也就是說，第三單元的測試在第1部分與第2部分的挑戰性都比較大。正是這一特征，使得黑盒測試的優勢不再，基于Junit單元測試的白盒測試才有了它的用武之地。

　　但事實上，單元測試雖然能夠一定程度上簡化1和3，但不可能将其簡化到0的地步。具體而言，輸出的正确性還是需要你進行

assert*()

驗證，而輸入更是要你基于不同的可能場景構造相應的輸入樣例。

　　此外，單元測試也不應停留在以單個方法為基本單元的測試上，它也必須要有一定的組合能力。事實上，對于非常簡單的方法，形式化驗證要比單元測試更有效果。

　　單元測試能夠起效的另一個關鍵之處在于構造合适的測試樣例。或者不如說，構造樣例永遠是任何測試最重要的一環：如果你構造測試資料的時候就沒有考慮到全部的情況，那麼無論你再怎麼測你的程式都永遠會是對的。而Unit1，Unit2自己在這上面嚴重依賴于随機生成，是以并未及時認識到手動構造樣例的重要性。

　　綜上，我們可以對第三單元的測試得出以下結論：

1. 總體應以單元測試為主，形式化驗證為輔
2. 單元測試應隻是提供一個架構，有意義的測試資料才是靈魂
3. 要考慮多種方法組合的複雜情況

  那麼，現在回到Unit3本身。

　　在Unit3中，自己在task1, task3均未出現bug，在task2卻出現了一個極為緻命的bug：除零異常導緻的RE。也就是在建立一個Group但還沒有向其中加人之前就詢問該組的平均年齡，我的方法就會報錯。

　　之是以出現此問題，從事後諸葛亮的角度來看，大概可以歸結為以下幾點：

1. 直接原因：讀規格設計的時候對三元運算符不敏感，被public_nomal_behavior的定式套路限制了，下意識地以為同一個normal_behavior可以在同一個分支邏輯下完成，無需再進行特判。（而且我來回讀了那麼多遍tm愣是一次都沒發現我也是醉了）
2. 間接原因：在task2的時候，自己還沒有大幅度引入單元測試，而是僅用其進行單方法的壓力測試，對于方法的正确性檢查自己主要依靠形式化驗證，也就是肉眼比對代碼與規格；這一方法在task1證明了其很強的高效性，由于task2單方法的複雜度沒有顯著上升，是以我也直接拿來用了。但這就為1中問題的出現埋下了隐患。
3. 間接原因：在task1的時候，自己就有意識地對應用與算法進行解耦合，task2中，這一思想更是發揮到了極緻——我選擇了通過分包來表現這樣的區分關系。但這麼做，某種意義上也割裂了上層與下層之間直接交流的通道。于是，對于這種特判情況，我在看Group的規格時對照的是RealGroup中的那一行get方法，真正的實作卻藏在算法層。兩者之間無法有效銜接。這種情況下，如果每一個normal_behavior對應的情況相同，那就不會出現什麼問題；但對于1中的場景，難免就贻笑大方了。
4. 根本原因：在task2裡，我仍然沒能認識到測試的關鍵所在，總覺得如果自己能夠通過比對規格判斷代碼邏輯是否正确的話，再用Junit架構寫一遍這個過程又有什麼必要呢？但事實上，如前所述，junit的意義在于通過構造合适子集的測試樣例檢驗程式在局部的正确性，局部不意味着單個方法，子集不意味着一種情況。而自己出現的這個bug正是自己沒能将多個方法進行真正意義上的結合，沒能夠構造出區域性的測試樣例的結果。

  那麼，這樣的經驗教訓對于今後自己在寫代碼的時候又有什麼啟發式的意義呢？

　　簡單來說的話，就是一定要考慮全面，審題一定要再仔細些這樣。具體來講的話呢，

1. 基于資料的測試與基于形式的測試在任何場景下都很重要，後者适用于對局部的流程進行正确性檢查；前者則尤其适用于對程式整體，或者是一個子集，也就是對多個獨立方法的組合進行正确性檢查，當然還有壓力檢測。
2. 規格最大的用處是寫給人看的，是以如果這玩意不是自己親自寫出來的東西的話，還請務必一行一行給我看清楚，一個字都不許漏掉。
3. 請不要輕視每一件事。錯誤永遠不會發生在你最重視的那個山頭上，反倒是康莊大道更容易給你使絆子。

感想與總結

再談規格

　　規格啊，真的挺有趣的，我并不否定它存在的意義，但我同時也認為不應該賦予其過多的意義。

　　聯系我們平時的學習場景，究竟什麼時候需要用到規格呢？

　　如果自己既是産品經理又是程式員，那麼隻要用自己能夠了解的一套符号把所有的需求全部表達清楚就好了，根本沒有使用那麼嚴謹的語言的必要，寫着還勞神勞力，第二天看的時候還極有可能對自己發出靈魂三問，實在是算了算了。

　　但将來，自己可能不會同時扮演這些角色了，而這時候規格的用處就展現出來了。我想，這可能是課程組在第三單元選擇規格設計為主題的初衷吧。在一個大型項目中，我們如果不是首席架構師，就沒必要考慮的那麼面面俱到，但我們必須準确地完成上層所布置的任務。為了使這個過程不出現二義性，就必須要又這樣一種既屏蔽實作又絕對準确的形式化語言來作為媒介。是以，規格就顯得至關重要了。

　　不過怎麼說呢，重新審視第三單元，雖然自己的總體成績不如前兩個單元。但說實在的，我認為這個單元的總體挑戰度确實要低于前兩個單元。我想，這可能是課程組為了突出規格的重要性而不小心忽略掉了整個項目作為一個整體的自身的複雜度的建構吧。

　　複雜度主要展現在縱向的層次感，但反觀第三單元，為了可以增大規格的篇幅，核心的方法完完全全是并行的，是一個非常寬非常shallow的架構，那麼多的query，本質上卻都是在詢問一個圖模型的各種資訊而已，縱向的層次趨近于0。而且，這一單元的指導書雖然大道至簡，但是規格給出的具體規約卻比前兩個單元的指導書管的還要寬，連Person類的具體細節都不放過。這兩個原因，直接使得同學們作為具體的實作者的操作空間非常有限，算是提前體驗了一把在大公司的那種感覺？

　　那麼，要想做出改進，該怎麼做呢？

　　我覺得一個可行的思路就是繼續延續前兩個單元指導書的風格。首先，現在Unit3的這種情況給人一種好像隻有Unit3配擁有規格的感覺一樣。但顯然，Unit1，Unit2中指導書的那些要求也完全應該可以用規格實作才對（否則規格的泛化性展現在哪裡）。是以，Unit3應該在選擇場景時保持不低于前兩個單元的水準，然後在給出要求的時候以潤物無聲的方式将規格融入到核心方法的要求上去，替代原先要在指導書中表達的内容。（你想想如果把現在Unit3的規格翻譯成人話寫成指導書，那篇幅）。而對于一些間接用到的内部方法，就完全沒必要給出規格了吧講道理。

　　或者，還有一個簡單粗暴的思路。那就是把Unit3移到Unit1去。因為說白了，規格就是離散數學裡邏輯的那一套東西，如果對于模型複雜度要求不高的話，可能相比于現在的Unit1，對于大部分同學而言反而要更加友好一些，又沒有性能的壓力，又沒有來回嵌套的複雜模型，豈不美滋滋？也許課程組現在的思路是想首先展示面向對象的核心，也就是類的繼承層次等關系。但，怎麼說呢，這些思想其實在整個OO中都是一直貫徹的，Unit3裡展現的反而不是很強烈，是以，慢慢來或許會更好。

　　最後的最後，是自己的一點小感想，請課程組利益相關的人士忽略。

　　嘛，都說了忽略了我幹嘛還要寫在這裡啊？真是傻的不行。