标签：程序 log 时间复杂度 关于 测试 效率 心得体会 mlu href
理论基础
定义：
JML是用于对Java程序进行规格化设计的一种表示语言
| 关键字 | 解释 | 举例 |
|---|---|---|
| 方法执行后的返回值 | \result = p1.getId() == p2.getId(); |
|
\old(expr) |
相应方法执行前的取值 | add方法 list.length == \old(list.length)+1; |
\not_assigned(x,y,...) |
表示括号里的变量在方法执行过程中是否被赋值。是，返回true。 | not_assigned(x); |
\not_modifoed(x,y,...) |
与not_assigned类似 |
----- |
\notnullelements(container) |
表示container对象中存储的对象不会有null |
notnullelements(set) |
\forall |
全称量词 | (\forall int i; 0 <= i < groups.length; \not_assigned(groups[i])); |
\exist |
存在量词 | !(\exists int i; 0 <= i && i < groups.length; groups[i].equals(group)); |
\sum |
返回指定范围的和 | (\sum int i; 0 <= i && i < people.length;1) |
\product |
返回指定范围的连乘 | \product int i; 0<i&&i<10; i) |
\max |
返回给定范围的最大值 | (\max int i; 0<i&&i<10; i) |
\min |
返回给定范围的最小值 | (\min int i; 0<i&&i<10; i) |
\num_of |
返回指定变量中的满足条件的个数 | (\num_of int i; 0<i&&i<10; i%2!=0) |
<: |
子类型关系 | x.TYPE <: y.TYPE |
<==> |
等价关系 | expr1<==>expr2 |
==> |
推理关系 | expr1==>expr2 |
\nothing \everything |
空集、全集 | ----- |
requires |
前置条件 | ----- |
ensures |
后置条件 | ----- |
assignable |
副作用范围限定 | ----- |
signals |
判断异常情况 | ----- |
invariant |
不变式 | ----- |
constraint |
状态变化约束 | ----- |
JMLUnitNG:根据规格自动化生成测试样例，进行单元测试。 下载地址：
从官网下载好openjml
开始验证，由于官方JML位于接口中，为了便于对相关内进行验证，需重新将JML与实现代码放置在一起，本博客以Person接口的实现Personn为例，主要验证的三个方法，equals()/isLinked()/compareTo()。
输入java -jar MYPATH/openjml.jar -exec MYPATH/openjml/Solvers-windows/z3-4.7.1.exe -check src/Personn.java -encoding UTF-8进行对JML语法进行检验，下面仅展示修改JML后无报错的情况。 
输入java -jar MYPATH/openjml.jar -esc src/Test.java进行验证，结果如下：
在IDEA中导入jmlunitng.jar（本文参考了一位同学的配置方法https://www.cnblogs.com/xishufan/p/12923474.html），这样比完全命令行相比，少去了编译的过程。
在pro目录输入java -jar MYPATH/jmlunitng.jar src/MyGroup.java src/com/oocourse/spec3/*生成自动化测试代码，对Group接口的实现MyGroup进行测试。
按照JUnit的方法运行MyGroup_JML_Test.java文件，可以发现，生成的测试代码就是JUnit格式的测试文件。
运行结果如图 
通过运行结果发现，jmlunitng生成的测试用例主要是对边界情况的测试用例，如Integer.MAX_VALUE、Integer.MIN_VALUE或null，但也会生成一般的测试用例。分析结果发现，failed的测试点，是因为MyGroup类中addPerson(Person p)未判断p为null的情况，导致出错。但是在network调用之前我们已经避免了p为null的情况。所以程序本身从整体来说并没有出错。局部来看有一定问题。
第一次作业
本次作业大致来说就是按照规格实现代码，没有考虑架构方面的问题。
其中选择了ArrayList作为容器存储Person，本次作业由于数据相对简单，并没有出错，但是在之后的作业中这样的设计就会暴露出弊端了。
另外关于isCircle()，本次作业选取了bfs的方法判断，并且增加visSet记录已经访问的节点，减少不必要的访问。
第二次作业
本次作业主要新增缓存机制，以及采用HashMap进行查找的设计思路。
缓存机制类似于Cache，动态维护MyGroup类中我们需要的结果，注意，不仅需要在MyGroup类addPerson()时更新，并且还需要在MyNetwork类addRelation()时判断是否需要更新。
另外，考虑到需要多次进行查询的工作，采用HashMap进行查询，相较于ArrayList进行查询，时间负责度从O(n)下降了O(1)，减少了不必要的性能损失。
同时考虑到HashMap扩容机制会造成不必要的性能损失，所以初始化时进行了一定的考虑。
第三次作业
本次作业主要是考察图的有关操作。
本次作业，判断两节点是否连通和qbs采用了并查集算法，qmp采用了堆优化的dijkstra算法，qsl起初是暴力dfs加回溯，强侧后应为CTLE改为暴力枚举节点删除的算法。
第一次作业
本次作业未出现bug，采用JUnit对代码进行测试。
第二次作业
本次作业强侧有2个点CTLE，原因是最初未采用缓存的机制，这样导致了如果需要访问Group类中的数据，特别是qrs和qvs都需要O(n^2)的时间复杂度，当某个Group类中的Person人数过多时，并且频繁进行qrs和qvs时，时间复杂度过高，导致爆掉。
修复采用了缓存机制，动态维护有关结果。
第三次作业
本次作业真的算爆掉了，强侧整整7个点爆掉CTLE，本来以为只有qsl会爆掉，没想到qmp页爆了。
通过JProfile分析时间复杂度较高的方法，发现尽管qmp采用了堆优化的dijkstra算法，但是在判断isCircle()的时候，还是使用了第一次作业中的bfs方式，这样导致，每调用一次qmp，都要进行一次bfs，如果两节点是直接islinked()，浪费了大量的时间！！。修复之后，采用了效率更高的并查集算法。
关于qsl，如果采用dfs暴力加回溯的方式，复杂度可能极高，在面对复杂的图时（比如一个简单图和一个极其复杂的完全图相连）一旦dfs进入复杂的完全图，需要极长的时间才能回到简单图，如果仅仅只是想查询简单图上两节点是否qsl，这样性能太难看了。修复之后，采用课程组标程采用的暴力枚举算法。
本单元的体会就是规格，规格还是规格！！虽然强调规格，但是死照着规格写必然会爆炸，所以如何正确理解规格，以及具体实现规格显得尤为重要。还有一点体会比较深，就是满足规格，和完全照着规格写诗是两码事，如何在满足规格的前提下，选择性能较高的算法以及数据结构，通过这一单元的训练令我感触颇深（数据结构没学好的后果），自己需要这方面进行反思与提高。
另外，本单元需要大量数据数据进行对拍，这也是我欠缺的地方，不能仅测试边界数据，小数量级的数据总归是不保险的。
标签：程序 log 时间复杂度 关于 测试 效率 心得体会 mlu href
原文地址：https://www.cnblogs.com/zhouh1999/p/12931114.html
