1、注释结构
行注释：//@annotation
块注释：/*@ annotation @*/
2、JML表达式
1.1原子表达式
esult表达式：表示一个非 void 类型的方法执行所获得的结果，即方法执行后的返回值。
old( expr )表达式：用来表示一个表达式 expr 在相应方法执行前的取值。
ot_assigned(x,y,...)表达式：用来表示括号中的变量是否在方法执行过程中被赋值。
ot_modified(x,y,...)表达式：与上面的 ot_assigned表达式类似，该表达式限制括号中的变量在方法执行期间的取 值未发生变化。
onnullelements( container )表达式：表示 container 对象中存储的对象不会有 null 。
ype(type)表达式：返回类型type对应的类型(Class) 。
ypeof(expr)表达式：该表达式返回expr对应的准确类型。
1.2量化表达式
forall表达式：全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。
exists表达式：存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束。
sum表达式：返回给定范围内的表达式的和。
product表达式：返回给定范围内的表达式的连乘结果。
max表达式：返回给定范围内的表达式的最大值。
um_of表达式：返回指定变量中满足相应条件的取值个数。
3、方法规格
(1) 前置条件：requires
（2）后置条件：ensures
（3）副作用范围限定：assignable或modifiable
4、类型规格
(1)不变式invariant：是要求在所有可见状态下都必须满足的特性，语法上定义 invariant P ，其中 invariant 为关 键词， P 为谓词。
(2)状态变化约束constraint ：对象的状态在变化时往往也许满足一些约束，这种约束本质上也是一种不变式。
1.OpenJML：检查JML规格的正确性，提供对程序的静态和动态检查。
由于各种报错等问题，本人openjml的布局失败。。。
2.JMLUnitNG：根据JML自动生成测试数据来验证正确性。
首先，将(稍加修改的)MyGroup.java和openjml，junitng的jar包放在同一目录下，然后命令行运行如下命令：
java -jar jmlunitng.jar test/Group.java javac -cp jmlunitng.jar test/*.java java -jar openjml.jar -rac test/Group.java test/Person.java java -cp jmlunitng.jar test.Group_JML_Test
经过一系列尝试之后，终于是有结果了，以下是本人运行结果的片段，由于测试样例大多为一些边界数据，并不是所有的点都是pass，下图仅为pass的部分点:
前言
第三单元的作业以JML语言主题，以人际关系网络为背景，分三次要求逐步增加，难度逐步提高。这三次作业，让我进一步理解了java编程语言，明白了规格和实现之间的关系，使得我在编程上更为严谨。
以下是我对于这三次作业的总结，希望能给我以后得到作业和今后的编程道路提供帮助和参考。
第一次作业
架构分析：第一次作业主要是基于规格填写代码，难度不高。在isCircle方法中，本人使用了DFS，这并不是效率很高的算法，但对于本次作业的数据规模来说足够通过。
bug分析：本人在本次作业中并未被测出bug。
第二次作业
架构分析：第二次作业也主要是基于规格填写代码，增加了Group类，数据规模相对于第一次大大增加，本人不得不对其做一些优化；本人将isCircle方法改为了查并集，并且对于组内的关系合，平均年龄等数据采用了缓存机制；这些优化对于这种高访问低修改的数据效果十分明显。
bug分析：本人在这次作业中因为没要看到一行规格的描述(选择性忽略)，导致强测挂了4个点；具体来说是group的人数小于1111，本人检查工作和测试工作做的十分不到位。
第三次作业
架构分析：第三次作业的难度相对于一，二次作业有了明显的提升，尤其是qmp(最短路径查询)，qsl (环路查询)方法，本人前者采用了Dijkstra算法，后者采用了DFS环路查询算法，然而这两者复杂度较高，为强测和互测埋下隐患。
bug分析：本人在这次作业中的qmp和qsl均出现了tle问题，导致强测直接挂了5个点，本人不得不进行优化算法；参考了讨论区大佬和一些博客之后，本人qmp采用了优先队列的Dijkstra算法，qsl采用了枚举删点判断联通的方法，性能大大提高。
每一个极大连通子图都抽象为一个群体，拥有共同的祖先(ancestor)，每个人都有唯一的父亲结点(parent)，每次进行isCircle，只需对两个结点循环找父亲结点 (追根溯源)，直到找到祖宗(祖宗的父亲为其本身),两者的祖宗结点相同，则必连通。
int ancestor1 = p1.getParent(); while (ancestor1 != p1.getId()) { p1 = MygetPerson(ancestor1); ancestor1 = p1.getParent(); } int ancestor2 = p2.getParent(); while (ancestor2 != p2.getId()) { p2 = MygetPerson(ancestor2); ancestor2 = p2.getParent(); }
p1.setParent(ancestor1);
p2.setParent(ancestor2); return ancestor1 == ancestor2;
同时，在addrelation的时候，需要循环查找两者的祖先，若祖先不相同，则将后者的祖先的parent设置为前者的祖先，这样可以保证查找祖先路径的唯一性；
同时，为了进一步提高效率，本人采取了压缩路径的方法，每一次循环找祖先(adderlation,isCircle)，都将结点的parent直接设置为自己的祖先，下一次访问课大大减少循环次数。
2.queryMinPath--优先队列的Dijkstra算法
此算法借鉴了一些博客，做了一些修改以适应本人的体系，采用java的核心类PriorityQueue，并将人抽象为id-distance二元对，用Weight类来表示这个二元对，并增加MyComparator类(继承Comparator，重写compare方法，为优先队列内部的堆排序提供比较原则)
MyComparator myComparator = new MyComparator(); PriorityQueue<Weight> que = new PriorityQueue<Weight>(myComparator); HashMap<Integer, Integer> visit = new HashMap<Integer, Integer>(); HashMap<Integer, Integer> distance = new HashMap<Integer, Integer>(); Weight nweight = new Weight(id1, 0); distance.put(id1, 0); que.add(nweight); while (!que.isEmpty()) { Weight now = que.poll(); int id = now.getId(); if (visit.containsKey(id)) { continue; } if (id == id2) { break; } int min = now.getWeight(); visit.put(id, 1); MyPerson top = MygetPerson(id); for (int i = 0; i < top.getAcquaintanceSum(); i++) { MyPerson np = top.getAcquaintance(i); if (!visit.containsKey(np.getId())) { if (!distance.containsKey(np.getId()) || min + top.queryValue(np) < distance.get(np.getId())) { int update = min + top.queryValue(np); Weight next = new Weight(np.getId(), update); distance.put(np.getId(), update); que.add(next); } } } } return distance.get(id2);
3.queryStrongLink--删点寻通路
这个方法也是询问了大佬，本人一开始是用DFS找环路这种朴素的方法实现的，但无奈这个算法效率过于低下
此方法分为两种情况
1）.两点直接相连：将连点之间的边(关系)删去，并进行DFS查找通路，若存在，则两点必成环
if (p1.isLinked(p2)) { //System.out.println("mode1"); visit = new HashMap<Integer, Integer>(); final int value = p1.queryValue(p2); p1.delAcquaintance(p2); p2.delAcquaintance(p1); final boolean isfind = findPath(id1, id2); p1.addAcquaintance(p2); p2.addAcquaintance(p1); p1.addValue(value); p2.addValue(value); return isfind;
｝
注意，由于这次背景架构的特殊性，删边即删除关系(熟人列表)，由于arraylist顺序存储的特性，本人的Person类的熟人和Value集合位置是一一对应的，暂时删除人的时候关系值也要一并删除，加回的时候，要一并加回；
2），不直接相连：将除两点外的点一个个删去判断删除后有无通路，在一个个加回，事实上，若两点成环，删去任意一个点，不影响两者之间的连通性(找割点)，实际上这只是一个必要条件，无法涵盖第一种情况，所以需要分类讨论，较为统一得到做法是直接删边，但这样更为复杂，遂放弃。
else { for (int i = 0; i < people.size(); i++) { int id = people.get(i).getId(); if (id == id1 || id == id2) { continue; } else { visit = new HashMap<Integer, Integer>(); MyPerson np = peomap.remove(id); //System.out.println("Remove:" + np.getId()); if (!findPath(id1, id2)) { peomap.put(id, np); //System.out.println("Fail:" + np.getId()); return false; } peomap.put(id, np); } } return true; } }
同时要注意，由于数据规模的问题，visit采用数组，Person在arraylist中的位置对应数组中的index这样会炸tle，因为从id得知其位置需要一个遍历操作，才能知道其有无被访问过，然后遍历操作不可怕，可怕的是在循环中的遍历，更可怕的是在循环中的DFS中的每一次递归中的遍历；可取的做法是采用Hashmap，将id和是否被访问的标志为存的二元对存放。