Fate/Beihang OO——第三单无总结
经过电梯和求导的锤炼，第三单元的难度仿佛是闹着玩一样——如果你只想实现。然而第三单元又比较“阴险”，它没有设置性能分，而是将性能分直接与对错挂钩，这直接导致我多次下定决心实施的“不优化主义”化为泡影，毕竟代价不小。
然而，一涉及到时间复杂度上的优化，各种各样的难题便接踵而至。且不说图论算法一类问题，就是JAVA语言本身的各种用法也显得举步维艰，特别是容器、容器和容器。Key, Value, Entry遍历效率不同、容器初始化对效率的影响，contain和get时各种容器效率的差别…种种问题让人头疼不已。
以上是一些牢骚，接下来进入正篇——JML单元的总结。
一、JML语言以及工具链
1. JML语言
以下内容是对《JML使用手册》的简单梳理
JML是用于对Java程序进行规格化设计的一种表示语言。
说白了，就是JML会提供一种规格，或者说规则，而实现人员则要用代码去实现这个规则。对用户而言，他不关心实现者的具体实现方式，而实现者需要做的也只是保证自己的代码能满足JML规格中的所有语句。
JML可以有效避免实现者对需求方需求理解的偏差。
关于JML语言的解读，无非像是学习一门简单（至少Level 0阶段）的语言。因为没有考虑到自己写规格的情况，学习就变得更加简单了。
- requires, ensures, assignable 代表条件、结果和限制
- forall, exists, sum表达式分别表示任意、存在和求和，这些语句需要知晓语法
- old代表旧值，result代表返回值
- normal, exceptional方法分别代表此规格属于正常执行还是会抛出异常
- pure限定方法不改变任何值
注意，在实现规格时，并不一定要按照描述的步骤中规中矩地照抄不然铁TLE。
2. 工具链
主要是以下两种，分别进行JML语法检查与自动构造测试集。
OpenJML
这是一个检查JML规格正确性的工具，可以从完整性、语法、内容正确性等多方面进行检查。
JMLUnitNG
可以通过JML规格自动生成测试集并测试，其数据多是一些边界情况。
二、SMT Solver
运用OpenJML来检查JML规格的语法正确性。
部署过程：参考J的博客 https://www.cnblogs.com/pekopekopeko/p/12920417.html
直接使用cmd调用。因为只检查某些类会出现找不到XXXX类的报错，故直接将所有类一起检查了。执行指令如下：
java -jar openjml.jar -exec Solvers-windowsz3-4.7.1.exe -esc Group.java Person.java Network.java EqualGroupIdException.java EqualPersonIdException.java EqualRelationException.java GroupIdNotFoundException.java PersonIdNotFoundException.java RelationNotFoundException.java
得到结果：
.Network.java:344: 错误: 非法的表达式开始
@ (forall int j; 0 <=& j & j < i; !isCircle(people[i].getId(), people[j].getId()));
^
.Group.java:58: 错误: 不可比较的类型: int和INT#1
/*@ ensures
esult == (people.length == 0? 0 :
^
其中, INT#1是交叉类型:
INT#1扩展Number,Comparable
.Group.java:63: 错误: 不可比较的类型: int和INT#1
/*@ ensures
esult == (people.length == 0? 0 : ((sum int i; 0 <= i && i < people.length;
^
其中, INT#1是交叉类型:
INT#1扩展Number,Comparable
3 个错误
其中第一个错误明显是手癌把 && 打散了，修改后不再报错。后两个错误意义不明，使用强制类型转换将
esult后面的表达式转换成int后不再报错。
再改完3个错误后，报了全新的3个错。
.Group.java:58: 错误: Could not find model field the
/*@ ensures
esult == (int)(people.length == 0 ? 0 :
^
错误: 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
java.lang.NullPointerException
at com.sun.tools.javac.tree.TreeMaker.Select(TreeMaker.java:597)
at org.jmlspecs.openjml.esc.JmlAssertionAdder.createUnboxingExpr(JmlAssertionAdder.java:10913)
at org.jmlspecs.openjml.esc.JmlAssertionAdder.visitTypeCast(JmlAssertionAdder.java:12420)
at com.sun.tools.javac.tree.JCTree$JCTypeCast.accept(JCTree.java:1814)
at com.sun.tools.javac.tree.TreeScanner.scan(TreeScanner.java:49)
at org.jmlspecs.openjml.vistors.JmlTreeScanner.scan(JmlTreeScanner.java:67)
at org.jmlspecs.openjml.esc.JmlAssertionAdder.convertExpr(JmlAssertionAdder.java:1504)
at org.jmlspecs.openjml.esc.JmlAssertionAdder.visitBinary(JmlAssertionAdder.java:11865)
at com.sun.tools.javac.tree.JCTree$JCBinary.accept(JCTree.java:1785)
at com.sun.tools.javac.tree.TreeScanner.scan(TreeScanner.java:49)
at org.jmlspecs.openjml.vistors.JmlTreeScanner.scan(JmlTreeScanner.java:67)
at org.jmlspecs.openjml.esc.JmlAssertionAdder.convertExpr(JmlAssertionAdder.java:1504)
at org.jmlspecs.openjml.esc.JmlAssertionAdder.convertJML(JmlAssertionAdder.java:1647)
at org.jmlspecs.openjml.esc.JmlAssertionAdder.addPostConditions(JmlAssertionAdder.java:4756)
at org.jmlspecs.openjml.esc.JmlAssertionAdder.convertMethodBodyNoInit(JmlAssertionAdder.java:1195)
at org.jmlspecs.openjml.esc.JmlAssertionAdder.visitJmlMethodDecl(JmlAssertionAdder.java:15130)
at org.jmlspecs.openjml.JmlTree$JmlMethodDecl.accept(JmlTree.java:1260)
at com.sun.tools.javac.tree.TreeScanner.scan(TreeScanner.java:49)
at org.jmlspecs.openjml.vistors.JmlTreeScanner.scan(JmlTreeScanner.java:67)
at org.jmlspecs.openjml.esc.JmlAssertionAdder.visitJmlClassDecl(JmlAssertionAdder.java:13787)
at org.jmlspecs.openjml.JmlTree$JmlClassDecl.accept(JmlTree.java:1173)
at com.sun.tools.javac.tree.TreeScanner.scan(TreeScanner.java:49)
at org.jmlspecs.openjml.vistors.JmlTreeScanner.scan(JmlTreeScanner.java:67)
at org.jmlspecs.openjml.esc.JmlAssertionAdder.convert(JmlAssertionAdder.java:1414)
at org.jmlspecs.openjml.esc.JmlEsc.check(JmlEsc.java:114)
at com.sun.tools.javac.main.JmlCompiler.esc(JmlCompiler.java:681)
at com.sun.tools.javac.main.JmlCompiler.desugar(JmlCompiler.java:439)
at com.sun.tools.javac.main.JavaCompiler.compile2(JavaCompiler.java:898)
at com.sun.tools.javac.main.JmlCompiler.compile2(JmlCompiler.java:712)
at com.sun.tools.javac.main.JavaCompiler.compile(JavaCompiler.java:867)
at com.sun.tools.javac.main.Main.compile(Main.java:553)
at com.sun.tools.javac.main.Main.compile(Main.java:410)
at org.jmlspecs.openjml.Main.compile(Main.java:581)
at com.sun.tools.javac.main.Main.compile(Main.java:399)
at com.sun.tools.javac.main.Main.compile(Main.java:390)
at org.jmlspecs.openjml.Main.execute(Main.java:417)
at org.jmlspecs.openjml.Main.execute(Main.java:375)
at org.jmlspecs.openjml.Main.execute(Main.java:362)
at org.jmlspecs.openjml.Main.main(Main.java:334)
.Network.java:58: 注: Not implemented for static checking: ensures clause containing
ot_assigned
@ old(people[i].getId()) != id2;
ot_assigned(people[i]));
^
.Network.java:183: 注: Not implemented for static checking: ensures clause containing
ot_assigned
@ ensures (forall int i; 0 <= i < groups.length;
ot_assigned(groups[i]));
^
错误: A catastrophic JML internal error occurred. Please report the bug with as much information as you can.
Reason: MISMATCHED BLOCKS
.Network.java:275: 注: Not implemented for static checking: ensures clause containing
ot_assigned
@ ensures (forall int i; 0 <= i < groups.length;
ot_assigned(groups[i]));
^
3 个错误
我已经一头雾水了，怎么BUG越改越多还看不懂的
鉴于OpenJML年久失修且我们也没有写JML规格的要求，故我选择了就此罢手，算是一个了解了。
三、JMLUnitNG/JMLUnit
这个工具可以自动生成测试样例，我自然很感兴趣，急忙拿来用了用。部署与使用仍然参考J的博客。J，永远的神
仍然使用cmd运行，直接将jmlunitng.jar放到了项目文件夹中。将所有.java与JMLUnit包放在一起后——
jdk版本没对，于是又去下了个1.8，接着执行：
java -jar jmlunitng.jar srcHisGroup.java srccomoocoursespec3mainGroup.java srcMyPerson.java srccomoocoursespec3mainPerson.java
然后报了一万个错，还有一亿个警告。众所周知，警告等于不管，所以就来看看错误。
主要有以下几类：
- 中文字符编码错误
- 非法的类型开始
- 类型变量数目错误
中文字符删除后解决。
后两个错误都是因为形如private Map<Integer, Person> people = new HashMap<>();的定义报错。尝试后发现必须写成private Map<Integer, Person> people = new HashMap<Integer, Person>();的形式。
没有消息就是最好的消息，这一条代码终于成功运行。运行之后，src中的文件井喷式增长，JMLUnit自己建了很多测试类java文件。
然后发现javac找不到，又改了一通环境变量。
然后执行：
S:OOJMLUnit>javac -cp jmlunitng.jar src*.java srccomoocoursespec3exceptions*.java srccomoocoursespec3mainGroup.java srccomoocoursespec3mainPerson.java
最后在src里执行：
java -cp jmlunitng.jar HisGroup_JML_Test
终于大功告成！
结果：
S:OOJMLUnitsrc>java -cp jmlunitng.jar HisGroup_JML_Test
[TestNG] Running:
Command line suite
Failed: racEnabled()
Passed: constructor HisGroup(-2147483648)
Passed: constructor HisGroup(0)
Passed: constructor HisGroup(2147483647)
Failed: <<HisGroup@1761e840>>.addPerson(null)
Failed: <<HisGroup@6c629d6e>>.addPerson(null)
Failed: <<HisGroup@3f102e87>>.addPerson(null)
Passed: <<HisGroup@27abe2cd>>.addValue(-2147483648)
Passed: <<HisGroup@5f5a92bb>>.addValue(-2147483648)
Passed: <<HisGroup@6fdb1f78>>.addValue(-2147483648)
Passed: <<HisGroup@51016012>>.addValue(0)
Passed: <<HisGroup@29444d75>>.addValue(0)
Passed: <<HisGroup@2280cdac>>.addValue(0)
Passed: <<HisGroup@1517365b>>.addValue(2147483647)
Passed: <<HisGroup@4fccd51b>>.addValue(2147483647)
Passed: <<HisGroup@44e81672>>.addValue(2147483647)
Failed: <<HisGroup@60215eee>>.delPerson(null)
Failed: <<HisGroup@4ca8195f>>.delPerson(null)
Failed: <<HisGroup@65e579dc>>.delPerson(null)
Passed: <<HisGroup@b065c63>>.equals(null)
Passed: <<HisGroup@768debd>>.equals(null)
Passed: <<HisGroup@490d6c15>>.equals(null)
Passed: <<HisGroup@7d4793a8>>.equals(java.lang.Object@449b2d27)
Passed: <<HisGroup@5479e3f>>.equals(java.lang.Object@27082746)
Passed: <<HisGroup@66133adc>>.equals(java.lang.Object@7bfcd12c)
Passed: <<HisGroup@42f30e0a>>.getAgeMean()
Passed: <<HisGroup@24273305>>.getAgeMean()
Passed: <<HisGroup@5b1d2887>>.getAgeMean()
Passed: <<HisGroup@46f5f779>>.getAgeVar()
Passed: <<HisGroup@1c2c22f3>>.getAgeVar()
Passed: <<HisGroup@18e8568>>.getAgeVar()
Passed: <<HisGroup@5a42bbf4>>.getConflictSum()
Passed: <<HisGroup@270421f5>>.getConflictSum()
Passed: <<HisGroup@52d455b8>>.getConflictSum()
Passed: <<HisGroup@4f4a7090>>.getId()
Passed: <<HisGroup@18ef96>>.getId()
Passed: <<HisGroup@6956de9>>.getId()
Passed: <<HisGroup@769c9116>>.getPeopleSum()
Passed: <<HisGroup@6aceb1a5>>.getPeopleSum()
Passed: <<HisGroup@2d6d8735>>.getPeopleSum()
Passed: <<HisGroup@ba4d54>>.getRelationSum()
Passed: <<HisGroup@12bc6874>>.getRelationSum()
Passed: <<HisGroup@de0a01f>>.getRelationSum()
Passed: <<HisGroup@4c75cab9>>.getValueSum()
Passed: <<HisGroup@1ef7fe8e>>.getValueSum()
Passed: <<HisGroup@6f79caec>>.getValueSum()
Passed: <<HisGroup@67117f44>>.hasPersonId(-2147483648)
Passed: <<HisGroup@5d3411d>>.hasPersonId(-2147483648)
Passed: <<HisGroup@2471cca7>>.hasPersonId(-2147483648)
Passed: <<HisGroup@5fe5c6f>>.hasPersonId(0)
Passed: <<HisGroup@6979e8cb>>.hasPersonId(0)
Passed: <<HisGroup@763d9750>>.hasPersonId(0)
Passed: <<HisGroup@5c0369c4>>.hasPersonId(2147483647)
Passed: <<HisGroup@2be94b0f>>.hasPersonId(2147483647)
Passed: <<HisGroup@d70c109>>.hasPersonId(2147483647)
Passed: <<HisGroup@17ed40e0>>.hasPerson(null)
Passed: <<HisGroup@50675690>>.hasPerson(null)
Passed: <<HisGroup@31b7dea0>>.hasPerson(null)
===============================================
Command line suite
Total tests run: 58, Failures: 7, Skips: 0
===============================================
failed NULL是因为没有考虑传入null的情况。
可以看出来，我们的JMLUnit测试选了一些极端中的极端值来进行测试，显然，这种测试更适合程设课上的那类题而不是OO。
要测试，还是得自己构造大规模压力数据，毕竟很多BUG是在大规模代码、而不是极限数据下能看出来的。
不过这也告诉了我们，还是要好好思考边缘数据毕竟卡的就是这些
四、作业架构设计
本次作业的架构不用多说，自然是根据JML规格写实现，这里主要简要说一下一些值得一提的点。
1. Person
没有什么值得大书特书的地方，用HashMap存了关系，其中Person为Key，id为value。
第三次作业中将money及其方法直接嵌入了Person类中。
2. Group
同样使用HashMap容器保存people，其中id为索引。
此外，使用变量维护了ageSum, conflictSum, relationSum, valueSum等数值，以避免不必要的O(n)级甚至O(n^2)级循环喜迎TLE。不过，这样就要注意变量的维护了。
getRelationSum, getValueSum, getAgeMean, getConflictSum
直接返回维护好的变量
addPerson, delPerson
注意在每次加入或删除Person时判断Group内新添或减少的关系，同时维护前述各种变量。
- 特别需要注意的是，Network类中的addRelation方法也可能改变relationSum, valueSum的值，这时就需要判断ar指令的两个对象是否都在组里，以此来判断是否改变相应的值
3. Network
实话说，这个类中的种种方法才是这次作业中真正考验数据结构功底的地方。
没有删除大片注释时甚至险些超过500行限制。
首先，使用HashMap储存了people与groups，都以id为索引。
其次，使用并查集保存了人际关系中的各个小圈子，以便以O(1)或O(n)的效率完成相关方法。
使用blocks维护连通分支的数量，使用一个变量big（从-1递减）指示并查集根结点的序号。
并查集算法
使用HashMap储存并查集信息，以id为索引，所对应根节点为value（根节点的value是唯一的负数）。
使用HashSet bigs指示根节点的id（BUG修复阶段增加）。
有union和find两个方法，分别将两个块合体，以及找出某id对应的根节点。
在find过程中更新简化并查集，在union时若成功合一，更新blocks。
addPerson
需要注意在并查集中增加一个新的根节点，同时更新blocks与bigs。
addRelation
需要注意合并并查集，同时遍历groups更新里面关系相关变量。
isCircle
直接通过并查集判断是否同源。
isCircle（Old ver）
BFS
但是因为对容器的不熟悉在时间上优化了许久，比如对队列的遍历可以改成重新维护一个Set，大大提高效率；对Map value的遍历效率很低；可以维护一个容器保存尚未经过的点，减少遍历量。
queryMinPath
最短路算法。
采用未经过堆优化的dijkstra算法，三个CTLE的罪魁祸首。
其实我也尝试了堆优化，不知道哪里写错了，优化率不到百分之十就放弃了
复习了一下数据结构，这是好的。
queryStrongLinked
判断点双连通的方法。
浪费了我一个下午 + 半个晚上的大恶魔
心路历程：tarjan -> 太复杂，放弃 -> 暴力DFS -> 写得越来越复杂，放弃 -> tarjan
最后结合诸多大神留下的博客用tarjan算法完成了该方法。
在暴力DFS时没想到删点调用isCircle的我真是个笨蛋
五、BUG分析
本次作业和之前两次不同，问题主要出在阅读理解上，中规中矩地读懂规格、怪怪按规格实现，自然不会出现多大问题——如果不考虑时间复杂度。可是显然，第二次和第三次作业当然不允许我们这样做。所以，我这次的BUG分析主要着眼于算法和优化方面的翻车上。
-
关于优化方面，详见第四板块，简单来说就是要通过数据结构相关知识与对JAVA容器的了解优化时间复杂度到标称以内。
-
关于并查集，我一开始忽略了负数id对记录根节点的负数序号造成的影响，直接导致第三次作业强测30分。
- 真亏得30分还进了互测
- 而且一次都没有被炸到
-
关于借钱，差点搞错是谁向谁借。
在寻找BUG方面，主要还是运用形式化验证和自行构造数据。JUnit固然用着有种快感（指看着一片绿勾勾），可使用实在太有局限性且麻烦。不过，我还是使用JUnit验证了自己的基础功能。
六、心得体会
JML是个很好的消歧用的规格工具，但实在有点古老不灵活，个人觉得实用性不太高；至于JUnit与JMLUnit测试工具，前者使用起来不够方便，不如直接“脑assert”，不过关于测试覆盖率的提示还是可圈可点的；后者构造的数据集实在过于脆弱，实用性也不是很大，毕竟我们的很多BUG需要在极端抗压状态或者大规模数据下才能测试出，而不是简简单单的极限值。不过，它也在提醒程序员，要注意极限情况的考虑。
只从难度而言，本单元需要考虑的坑与代码量、思考量显然都远不如前两个单元，不过关于数据结构的复习则完全是盲点了。
这一次作业中，我叒犯了卡DDL的错。第二次作业中，我忘记了提交最后一个优化isCircle的版本导致互测被卡了点；第三次作业中，我最后尝试修改了一些东西，此时已没时间给我等CD了，提交后CE，当时有种汗毛直竖的感觉。不过还好，CE不计CD，现在想起来仍然心有余悸。
配置环境的过程就是摸索的过程，清理Error就像挤痘痘，挤的时候不舒服，挤出来真的浑身神清气爽。