一、JML的梳理和总结

1、jml理论基础

（1）前置条件

　　requires P;

　　使用逻辑或操作符来表示相应的约束场景： requires P1||P2;

　　要求调用者确保P为真，并且条件要求是并列，各种关系不能够重合。

（2）后置条件

　　ensures P;

　　即方法实现者必须同时满足有所并列ensures子句的要求。

 

（3）副作用范围限定

        assignable 或者 modifiable

        常用以下的形式表示  

 1 /*@ 
 2 @ ... 
 3 @ assignable \nothing;         //不可以对任何赋值
 4 @ assignable \everything;  
 5 @ modifiable \nothing;         //不可以修改任何数据          
 6 @ modifiable \everthing; 
 7 @ assignable elements; 
 8 @ modifiable elements; 
 9 @ assignable elements, max, min; 
10 @ modifiable elements, max, min; 
11 @*/

　　当然设计中也常用pure关键词，表示纯粹访问的功能方法

 

　　public /*@ pure @*/ String getName();

　（4）异常或者正常行为的区别机制

/*@ public normal_behavior
@.....
@.....
@ public exceptional_behavior
@....
@ signals (IllegalArgumentException e) true;   //signal_only
@*/

　　(5)三段式表达式

1 (\sum(\exists)(\sum)(\max)(\min) i；R(x)；P(x))
2 对于满足R(x)的x，则必须保证P(x)为真，如果是sum则求和
3 可能会因为括号位置的偏差导致对于表达式理解的错误

2、应用工具链

　　（1）OpenJML

　　　　 检查JML语法的正确性

　　　　 下载openjml包利用cmd进行命令行控制

 　　　　下载链接：http://www.openjml.org/downloads/

        （2）JMLUnitNG

　　　　根据JML规格生成对应的测试样例测试程序，并且进行正确性检测

　　　　下载链接：http://insttech.secretninjaformalmethods.org/software/jmlunitng/

二、openJML的SMT Solver的部署与验证

1、本单元jml语言的验证

采用z3-4.7.1的验证

cmd的命令大致如下：

java -jar openjml的路径 -exec 解释器的位置 -esc 需要验证规格的文件的路径

可以看到报错的都是三目运算符，改版本不支持，所以将对应规格进行修改

 1     /*@ public normal_behavior
 2       @ requires people.length == 0;
 3       @ ensures \result == 0;
 4       @ also
 5       @ public normal_behavior
 6       @ requires people.length > 0;
 7       @ ensures \result == ((\sum int i; 0 <= i && i < people.length; 
 8       @          (people[i].getAge() - getAgeMean()) * (people[i].getAge() - getAgeMean())) / 
 9       @           people.length);
10       @*/

最终没有什么报错说明还是合理的

2、构造错误的jml进行检查

 参考同学提供的一个乘除程序，进行正确性检查

 1 public class testJML{
 2     public static void main(String[] args) {
 3         testJML testjml = new testJML();
 4         System.out.println(testjml.mul(520, 521));
 5         System.out.println(testjml.div(10, 5));
 6         System.out.println(testjml.mod(10, 3));
 7     }
 8 
 9     //@ensures \result == a * b;
10     public int mul(int a, int b) {
11         return a * b;
12     }
13 
14     //@ensures \result == a / b;
15     public int div(int a, int b) {
16         return a / b;
17     }
18 
19     //@ensures \result == a % b;
20     public int mod(int a, int b) {
21         return a % b;
22     }
23 }

 

通过报错可以看出在规格中，没有规定前置条件，可能会出现一些计算溢出以及除零的状况发生。

 

三、JMLunitng构造测试样例

 在cmd中输入以下命令可以得出构造的数据

java -jar jmlunitng-1_4.jar test\MyGroup.java

  javac -cp jmlunitng-1_4.jar test\*.java

由于jml代码的不规范，如果不进行修改可能会出现如下的报错：

将其修改成二元运算即可在相应的目录下得到一些生成数据的java文件：

 

 

 

 

java -cp jmlunitng-1_4.jar test.MyGroup_JML_Test

 

 

 

 

 

 

 

 从这里可以看出运行结果较好

 

四、设计架构

1、第一次作业

　　第一次作业各个功能的实现较为简单，根据JML规格进行方法实现

　　其中较为复杂且容易出错的是isCircle方法，我一开始采用的是dfs进行查询，但是dfs的复杂度很高，且在强测前自我测试中出现了bug，我就放弃了该方法转而使用了bfs。

　　bfs就是将每个点的邻接点都放进数组里面，利用Stack结构不断的将新的邻接点加入，同时出栈结点以获得该点没有压栈的新的邻接点。

　　需要注意的是在Network中，访问网络中是否存在结点如果采用数组遍历就会带来很大的复杂度，但是如果是方法实现上HashMap的遍历复杂度则是相当的高。基于此，我参考一些容器的构造方法，构建了两个容器，一个是查询用的HashMap，一个是方便遍历用的ArrayList。牺牲空间换时间。这个小技巧为我后续新增方法带来了极大的便利。

2、第二次作业

　　第二次作业新增了一个Group类，在JML的规格方法中出现了很多n^2的方法。研讨课上同学交流分享了滚雪球的方法，我便借鉴了该方法，对于每个Person新建了一个Group缓冲数组。如果是添加关系则将改缓冲区数组，对应的权重和，结点度之和进行相应的操作。在添加Person时，遍历Group中与该Person有关系的进行操作，这样就能够将具有极高复杂度的几种方法简化成O(1)复杂度。而除了向组里面添加关系复杂度为O(n),向组添加人复杂度为O(n),并不会出现极高的复杂度。

　　第二次作业除了在复杂度下功夫，还需要注意的是JML规格，是先求和再除还是先除后求和。这是一个在强测前发现的重大bug，惊魂未定。由此我得到一个深刻的教训，就是不能直接复制规格原话，应该进行合理的理解，深刻的理解，不然就会造成严重的bug。当然不要自我修改JML要求的规格实现，事实证明很多的心存侥幸都会在强测中挂掉。

3、第三次作业

　　第三次作业最为重头戏的就是求最小通路的长度，以及求出两点之间是否双连通。

　　对于最小通路，我采用的是堆优化的Dijstra算法。通过构造新的类保存每个点现下最小的路径长度，利用compareTo方法结合优先队列进行出队，保证出队的一定是最小的权重，同时使用HashSet保证该点没有被访问确定过。这样的复杂度是最低的。

　　对于双连通的算法，我采用的是tarjan，但是由于我对于tarjan的原理不是很明白，在理解了网上的代码还是写不明白。后来在与同学沟通中了解到网上代码主要针对的是有向图求强连通分量，在与同学的交流下，我将原本的第二判断条件(!stack.contains(son))换成了（!son.equals(fa)），将出栈条件换成找到割点，由此便得到一个较为适合该方法的tarjan。但是得到所有的双连通分量并不是这次作业的要求，所以，我又进行稍微的修改，尽力的降低复杂度。

 

 1     public boolean queryStrongLinked(int id1, int id2)
 2             throws PersonIdNotFoundException {
 3         if (!contains(id1) || !contains(id2)) {
 4             throw new PersonIdNotFoundException();
 5         } else if (id1 == id2) {
 6             return true;
 7         } else {
 8             if (getPerson(id1).getAcquaintanceSum() == 1
 9                     || getPerson(id2).getAcquaintanceSum() == 1) {
10                 return false;
11             }
12             low = new HashMap<>();
13             stack = new Stack<>();
14             dfn = new HashMap<>();
15             boolean x = tarjan(id1, null, id2, 0);
16             return x;
17         }
18     }
19 
20     private HashMap<Integer, Integer> low;
21     private Stack<Integer> stack;
22     private HashMap<Integer, Integer> dfn;
23 
24     public boolean tarjan(int id1, MyPerson father, int id2, int cnt) {
25         int thisTime = cnt;
26         dfn.put(id1, thisTime);
27         low.put(id1, thisTime);
28         stack.push(id1);
29         MyPerson x = getPerson(id1);
30         ArrayList<MyPerson> sons = x.getAcquaintanceAry();
31         for (int i = 0; i < sons.size(); i++) {
32             MyPerson son = sons.get(i);
33             if (!dfn.containsKey(son.getId())) {
34                 tarjan(son.getId(), getPerson(id1), id2, cnt + 1);
35                 if (low.get(id1) > low.get(son.getId())) {
36                     low.put(id1, low.get(son.getId()));
37                 }
38                 if (low.get(son.getId()) >= dfn.get(id1)) {
39                     int newFriend;
40                     int friendSum = 0;
41                     boolean hasFriend = false;
42                     do {
43                         newFriend = stack.pop();
44                         if (newFriend == id2) {
45                             hasFriend = true;
46                         }
47                         friendSum++;
48                     } while (newFriend != son.getId());
49                     if (friendSum + 1 > 2 && hasFriend == true) {
50                         return true;
51                     }
52                 }
53             } else if (!son.equals(father)) {
54                 if (low.get(id1) > dfn.get(son.getId())) {
55                     low.put(id1, dfn.get(son.getId()));
56                 }
57             }
58         }
59         return false;
60     }

tarjan方法解决双连通

 

 

　　后来通过在bilibili学习相应的原理，我算是比较理解tarjan的思路：

　　

 

　　在这次作业中，我深刻的意识到iscircle的复杂度还是很高，在第二单元找bug的过程中，我学习了一种优化该方法简便的方法，就是讲图分成强连通图，每个图都是可达的，同时利用Arraylist的浅拷贝的优势，在addRelation进行一番操作，同时构建HashMap容器，这样查询isCircle复杂度就是O(1),极力降低了双连通的复杂度。

　　在这次作业中，因为算法图论的不扎实，导致我花很长的时间在学习构建架构中，同时因为原理不清晰，导致我出现很多的bug。debug过程也是相当的痛苦，因为在第二次作业中的优化，我在每个结点那边加了Group的缓冲区，但是Group删人的时候忘记删掉缓冲区，导致Group一些结果十分的莫名其妙。幸亏的截止时间没多久发现，否则必然就是强测炸裂。由此我得到一个教训，要对任何优化负责，否则有时候优化带来的虽然是性能上的优势，但是正确性如果没有进行严密的验证可能会导致，很大的失误。这次作业也让我深刻认识到自己脆弱的图论基础，看来还是得好好的的提升自己这方面的劣势，否则连百度都看不懂，请教同学也是难以理解算法的精妙之处。

 

五、BUG分析与构造策略

　　在这三次作业中，由于在写完程序，我进行了较为全面的功能测试，所以在强测跟互测中都没有bug。

　　在互测过程中，我针对自己的对于自己程序中出现的一些bug手动捏造数据。在第二次作业中，出现一些JML规格理解错误的bug，以及算法过于复杂导致的tle。这里需要注意的是HashMap的keySet因为要遍历两边所以复杂度是O(2n),很容易出现一些因为容器理解的错误导致的tle。第三次作业中，bug更是难找，无奈之下，我只能针对双bfs捏造数据，在同学分享的一张较为复杂的图中，构造数据并且多次访问qsl来进行hack。遗憾的是屋子里面还有一个\0的bug，我没有找出来，还是过分大意，认为在第二次作业的教训下不会出现这种bug。

 

六、总结

　　JML规格这一单元，理解JML规格是入门这单元的重点。在作业的完成中，应该严格按照规格规范实现方法，不要投机取巧。同时因为这次中测的放松难度，导致很多bug在中测难以体现，所以只能加强自己对于自己作业的测试，对于每个方法严格的测试，才能够在强测中没有WA。这一单元如同温水煮青蛙，实现虽然大多很简单，但是强测没出来，谁也不能确定自己的作业完全正确。强测的样例还是十分具有针对性，第三次作业中我有一个测试点时间高达1.5s但是我还是不知道我的算法在哪里出现较大的复杂度。同时这个单元在后续单元对于图论算法要求十分的高，要不是同学们之间的帮忙，推荐使用何种算法复杂度较低，复杂度优化细节，以及算法的交流，我可能无法平稳的过第三次单元。

　　向这单元给我提供帮忙的同学们表达十分的感谢！作为一个计算机学生还是不能忽视算法的重要性！