BUAA_OO_2020_Unit3_总结
2020年春季学期第十三周，OO第三单元落下帷幕，对这个单元的内容JML有了更深的理解，但也有了一些疑惑，下做总结：
一、JML语言以及工具链
经过课上JML语言的学习，以及实验与课下作业自己实践的理解，我认为JML语言通过一个契约对一个待实现的功能进行了一个约束，这个约束包括了我可以使用什么，使用要求是什么，得到结果应该满足什么等等。但对于怎么使用并没有做出限定。所以对于实现过程具有较大的自由度。但是由于功能的复杂性，不同的规格可能具有不同的复杂度，对应的实现过程也有不同的时间、空间复杂度。对于JML的直接翻译是一个十分不好的习惯，这也是我几次作业都出现的一些问题。由于牺牲了深层次的理解，代码必然会出现性能上或者功能上的准确性与鲁棒性。下面是针对JML level 0语法的一些总结：
| 一些常用表达式 | 对应语义 |
| requires | 前置条件限定 |
| assignable | 副作用范围限定 |
| ensures | 后置条件限定 |
| esult | 表示本方法所返回的结果 |
| old | 表示在本方法对此引用内容修改之前的内容 |
| ot_assigend(x,y,...) | 表示括号内变量不可在方法中被赋值 |
| ot_modified(x,y,...) | 表示括号内变量取值未变化 |
| forall | 表示全称量词，对应三个语句ABC，对于所有的A，若B满足，则C满足 |
| exists | 表示存在量词，对应三个语句ABC，存在一个A，当B满足时，C满足 |
| sum, product | 表示求取结果，对应三个语句ABC，对于A，当B满足时，对于C的语句执行连加（连乘）得到的结果 |
| max, min | 表示求取结果，对于三个语句ABC，对于A，当B满足时，返回C的语句中的最大值（最小值） |
| <==> | 表示等价关系 |
| ==>, <== | 表示可以从左推导得右（或从右推导到左） |
| othing, everything | 表示一个空集（全集） |
对于方法规格而言，JML有相应的语法逻辑，其往往表述为
1 /*@ public normal_behavior 2 @ requires ... 3 @ assignable othing; 4 @ ensures ... 5 @ also 6 @ public exceptional_behavior 7 @ requires ... 8 @ signals ... 9 @*/ 10 public /*@ pure @*/ int ...();
而对于类型规格，JML定义了不变式invariant，状态变化约束constraint来进行限定。
- 不变式要求在所有可见状态下都必须满足的特性
- 状态变化约束来对前序可见状态和当前可见状态的关系进行约束
工具链
本单元的工具链包括官方的OpenJML用以检测JML语法，其可与Eclipse结合进行使用，还包含自动生成测试用例的JMLUnitNG和JMLUnit等，但其测试模式较为简单，所以并不十分具有可使用价值。下面针对我配置的工具链进行介绍。
二、OpenJML
OpenJML由于其为官方开发的检测工具，其可靠性还较高一些，但其可能存在的兼容性问题，导致其不容易跑成功，比如本人尝试了官网的两种配置方法：采用jar包进行命令行配置，以及Eclipse的OpenJML配置均以不是很成功告终。
其中采用命令行配置的大致命令如下：
java -jar openjml.jar -option<check, esc, rac> -exec z3....exe sourcepath.java
其中-check代表进行JML静态检查，-esc代表利用Solver进行静态检查，-rac代表进行运行时检查，-exec对应运行相应的z3软件，后跟需要检查的java文件
但在经过多次尝试之后，命令行仍然会返回许多错误，其中不乏对于 esult等基础表达式的无法解析，至今不太清楚具体原因。
Eclipse中OpenJML的配置，本人也进行了简单的配置，获得的反馈似乎没有很多有效信息
总之可能是我的打开方式不对，也有很多同学与我有同样的问题。这个工具可能很强大但是在使用过程之中体验却不是很佳，这个工具可能仍需要改进与优化，或者由一代又一代的OO学子们涌现出的勇者来填补这个坑。
三、使用JUnitNG来对Group进行简单测试
JUnitNG的配置方法较为简单，但是配置的过程也有一番波折，需要对待测class进行一番修改，再执行相应的代码之后得到结果：
1 java -jar jmlunitng-1_4.jar MyGroup.java 2 javac -cp jmlunitng-1_4.jar *.java 3 java -cp jmlunitng-1_4.jar MyGroup_JML_Test
[TestNG] Running: Command line suite Failed: racEnabled() Passed: constructor MyGroup(0) Passed: constructor MyGroup(-2147483648) Passed: constructor MyGroup(2147483647) Passed: <<MyGroup@4fc3fcd5>>.addPerson(null) Passed: <<MyGroup@1aa7381b>>.addPerson(null) Passed: <<MyGroup@44e65172>>.addPerson(null) Passed: <<MyGroup@60eeebd5>>.addPerson(java.lang.Object@4ca6665f) Passed: <<MyGroup@26e579dc>>.addPerson(java.lang.Object@66caa894) Passed: <<MyGroup@76215e8d>>.addPerson(java.lang.Object@49011bd5) Passed: <<MyGroup@58401b4c>>.addrelation() Passed: <<MyGroup@86575d6a>>.addrelation() Passed: <<MyGroup@1761cf4e>>.addrelation() =============================================== Command line suite Total tests run: 12, Failures: 0, Skips: 0 ===============================================
通过对反馈结果我们可以看出来，JMLUnitNG可以测试的范围很有限，对数据可能更多测试的边界以及异常情况，对于测试功能可能较为有限（还是自己好好测把）
四、作业架构分析
三次作业以JML为核心，逐步构造了一个较强的功能越来越齐全的社交网络，在作业的逐步迭代的过程中，我的代码，以及对JML的理解也在逐步的完善之中。首先我的代码仍存在的问题就是，继承关系太死，不够将抽象出来的数据结构，进行类的抽象，从而只有干巴巴的group，network，person的实现类。不是说这种实现方式不好，而是从这三个类的名字来看，我们并不能看出来我们具体实现的是如何，而且层次关系也较为平淡。
- 第一次作业
第一次作业由于较为简单（也是我最惨的一次），并不需要采取什么特殊的数据结构与算法，所以我对于Person，Network里的具体数据结构都采用的ArrayList实现，也可能由于第一个单元就产生了这种直接翻译JML的陋习，后两个单元的一些地方都继承了这个习惯。导致后期进行时间估计时出现明显问题，再进一步进行改正。JML语言只是为描述其所限制的条件，而引用一些中间变量/已有pure方法，但我们需解读这些限制背后究竟求取的是什么内容。
第一次作业跟着JML规格进行翻译就可以，但由于其中的查询操作复杂度为On，甚至存在On^2的操作，所以其为第二次作业留下了一些隐患。对于第一次作业的重头戏isCircle，我用了BFS，可能这也是一个成功案例，只要对这个方法进行正常分析，理智分析，就可以获得相应更好的解决方案。
- 第二次作业
第二次作业加入了大型社交网络内小型组的表示，以及数据量的压力。其实已经是对实现的时间复杂度进行了相关要求。对不同容器的方法源码进行阅读，上网查找资料可以帮助我们更好的使用他们。HashMap会根据容量与影响因子进行扩容，ArrayList，Hashset的查找，增加方法的复杂度是怎样的。对于群组Group中的一些属性的获得操作，如果每次获取都进行计算，那在压力测试面前必定会垮掉。（更科学的方法应该是根据数据量，模拟时间进行计算来判断是否会炸掉），所以需要采用存储，更新的方式进行调用。将复杂度降低，并均摊给了其余方法之中，从而降低本算法的时间复杂度。
值得注意的是，本次作业出现了一个没有JML规格的方法，但是没有规格的限制，我们仍需要注意根据方法内容，结合具体实现中需要的细节进行逻辑书写，切不可放松警惕。
- 第三次作业
第三次作业又问我们增加了新的方法，这些方法之中的核心为MinPath，StrongLinked，BlockSum这三个。从这三个方法也能看出来本单元旨在构建一个社交关系的网络，通过网络的一些特点获取其中的信息，运用抽象出的图这个数据结构进行相应的查询操作（这三个方法都为查询操作），从相关的数据量限制也能看出来，为实现最短路，点双连通，以及连通块的查询，我们需要用相应的算法进行实现。
MinPath使用堆优化的Dijstra进行实现，可以将复杂度从O(n^2)降低到O(nlogn)，而堆的优化在于每次取出权最小的边，利用java实现的PriorityQueue即可（省时又省力）。BlockSum连通块个数若采用翻译JML进行的话，复杂度应该是O(n^4)（我一开始直接翻译时并没注意到），改用并查集进行操作时，最慢复杂度为O(n)，更快的可以保存变量，每次查询时返回即可，在addPerson时+1，在addrelation时当判断两个节点的根节点不是同一个从而合并时-1。并查集的使用可以进一步优化iscircle的实现方式，从而降低iscircle的复杂度。StrongLinked本人未采用Tarjan算法，而是采用了暴力求取的方法（事先经过估计，应该不会爆掉）。注意两个只有互相连通的点不算StrongLinked，从而需要加入特判。
下为三次作业的UML类图，可以看出功能逐步拓展。内容也逐渐优化。
五、bug分析
三次作业分别出现了不同的bug，也产生了不同程度的打击。
第一次作业由于并没有充分读懂JML规格，导致addrelation方法中对于两个id相同获得了错误的响应，从而炸掉了所有的点，也是最惨痛的教训。炸掉之后再次读JML规格，结合学长讲的“对于JML没有规定的行为，在此方法之中也不可以做任何的事”才对此问题有了更深的认识。
第二次作业是对Group方法之中O(n）的查询方法未保存值，从而构造数据卡掉了。应该归因于自己对数据量以及运行时间的把握以及极端情况下测试估计不足导致
第三次作业问题出在qmp之上，由于其没有限制数据量，所以对于我的堆优化Dij没有完全优化，从而导致CPU时间略微超过系统要求时间，从而爆掉了。这次修复bug的过程也是最难的一次过程，也体会到了只有修复到极致，找到可能浪费cpu的所有根源所在才能解决问题（才应该算解决问题）
三次作业发现bug的方案：JUnit简单覆盖测试+与朋友对拍发现问题，效果很显著，但仍欠缺诸如时间的精确把控以及遇到两人都出现的问题缺乏感知的缺陷。
六、感想与总结
第三单元炸了一次强测是最惨的（orz），不过成绩不是主要。通过作业以及实验的设计，我们可以更深层次的了解JML，以及JML背后蕴含的这种规约化的思想，才是弥足珍贵的。但是从整体难度而言，我觉得这个单元可以作为第一单元出现在OO课程之中，让JML思想先嵌入思维，使用继承，多态等行为进行实现。第三次作业也补习了算法上的一小块漏洞，提醒了下学期算法导论课的重要性。面对本学期最后一个单元的学习，也切不可放松警惕，继续前行。