标签：pop contain 需要 直接 数据结构 理论 理解 增加 一般来说
一、JML理论基础
JML是设计者提供给开发者的说明书，除了消除自然语言的歧义和可供自动化测试，在大工程中规格注释可能是开发人员间效率最高的交流方式。
JML设定规格，同时有比较高的自由度，如类型规格不限制层次继承结构的设计（满足规格继承前提），抽象数据类型不限制实际使用的数据结构。
JML的注释结构和javadoc相同，行注释表示方法为 //@annotation，块注释为 /* @annotation @*/。
@ public normal_behavior / @ public exceptional_behavior （表示正常行为或异常行为）
@ requires people.length > 0; （前置条件）
@ assignable \nothing; （副作用）
@ ensures \result == BigInteger.ZERO; （后置条件）
注意方法规格中的后置条件，其为了描述所采取的逻辑并不是对实现细节的规定。
@ signals (Exception e) para1 == para2; （触犯异常）
JML表达式中定义了一系列操作符和原子表达式，用于断言(assertion)语句和相关注释体。如\result, \old, \not_assigned,和\forall, \exists等谓词量化表达式。
二、应用JMLUnitNG进行测试
按照jyc大佬博客中的方法建文件树配置jdk8魔改person和group后进行测试，依然遇到报错。
JMLUnitNG.processAllCompilationUnits中报错，未能加载文件。
三次作业严格按照规格中的层次，都没有自主设计扩展接口，造成MyNetwork类中的方法数越来越多，难以管理。可以将Network中的方法分类，针对涉及Person,Group,Money的分别抽象为PersonOperation,GroupOperation,MoneyOperation接口。
第一次作业是读懂简单JML规格，不能想当然。因为isLinked的id相等判断强测0分。
第二、三次作业难在算法复杂度的估计和实现。第三次作业求强连通使用了tarjan算法，简单地将无向图看作有向图的拓展来求点双，在解决了直接邻接情况和{(1,2),(2,3),(3,4),(2,4)}单次回溯的情况后，在强测中被8字图的情况hack，发现远不是简单增加特判就能完全解决的。于是改为O(N*N)复杂度的暴力枚举删点方法。
getBlocksum和isCircle使用并查集，但因为没按find+join的标准写法，导致关系判断出现bug。
四、bug分析
在用Hashset存储可变元素时，对元素的更改可能导致，foreach无法真正地遍历Hashset中的元素。
在试图使用HashSet<HashSet<MyPerson>>实现并查集时遇到如下问题
1 HashSet<HashSet<MyPerson>> blocks = new HashSet<>();
2 HashSet<MyPerson> subSet = new HashSet<>();
3 subSet.add(new MyPerson(1,"1",BigInteger.valueOf(1),1));
4 blocks.add(subSet);
5 for (HashSet s :
6 blocks) {
7 System.out.println(blocks.contains(s));
8 }
?
>>> true
此时结果正常，为true。
1 HashSet<HashSet<MyPerson>> blocks = new HashSet<>();
2 HashSet<MyPerson> subSet = new HashSet<>();
3 blocks.add(subSet);
4 subSet.add(new MyPerson(1,"1",BigInteger.valueOf(1),1));
5 for (HashSet s :
6 blocks) {
7 System.out.println(blocks.contains(s));
8 }
?
>>> false
但调换3,4两行，结果为false，也就是先add添加元素后改变元素，竟导致foreach无法实现正确的语义！
能力有限，目前未能找到原因。
另一种情形，
1 HashSet<MyNetwork> mySet = new HashSet<>();
2 mySet.add(new MyNetwork());
3 mySet.add(new MyNetwork());
4 System.out.println(mySet.size());
>>> 2
此时程序正常，但将MyNetwork换成Arraylist（或其他java容器类）就会出现问题
1 HashSet<ArrayList<Integer>> mySet = new HashSet<>();
2 mySet.add(new ArrayList<>());
3 mySet.add(new ArrayList<>());
5 System.out.println(mySet.size());
5 System.out.println(mySet.add(new ArrayList<>()));
>>> 1
>>> false
此时add返回值为false，说明集合中已存在此对象。验证如下
1 ArrayList<String> arrayList1 = new ArrayList<>();
2 ArrayList<String> arrayList2 = new ArrayList<>();
3 System.out.println(arrayList1.hashCode());
4 System.out.println(arrayList2.hashCode());
5 System.out.println(arrayList1.equals(arrayList2));
?
>>> 1
>>> 1
>>> true
五、心得体会
通过三次作业认识到，使用规格和一些抽象数据可以表达很复杂的逻辑，但在真正实现的时候不需要考虑规格描述的逻辑，只要在理解需求的基础上，可以自由地选择最优的算法。但也要充分测试不能想当然。
标签：pop contain 需要 直接 数据结构 理论 理解 增加 一般来说
原文地址：https://www.cnblogs.com/Gawson/p/12943671.html
