JML(Java Modeling Language) 是用于对 Java 程序进行规格化设计的一种表示语言。JML 是一种行为接口规格语言（Behavior Interface Specification Language，BISL），基于 Larch 方法构建。
一般而言，JML 有两种主要的用法：
（1）开展规格化设计。这样交给代码实现人员的将不是可能带有内在模糊性的自然语言描述，而是逻辑严格的规格。
（2）针对已有的代码实现，书写其对应的规格，从而提高代码的可维护性。这在遗留代码的维护方面具有特别重要的意义。
本单元考察的为JML的第一种用法，通过课程组所提供的接口和其完善的JML规格来实现所有的功能。
常见的JML语法（课程范围）：
前两次作业主要是通过课程中测，以及充分理解JML规格并且检查是否严格满足前置和后置条件，第三次作业通过与其他同学对拍，查找bug。实际上，在有完整的JML规格的情况下，可以使用JMLUnitNG、Junit等第三方工具验证JML规格的正确性。虽然在三次作业中没有使用相关工具，但在这简单介绍一下以下相关的工具链：
检查JML语法。不支持高版本java，环境很难配，可能会有很多报错或者warning。
根据规格自动生成测试，主要是对边界情况进行简单的测试。
单元测试。根据规格自行构造测试，可以检查覆盖率，尽量保证覆盖率高（但不是全部覆盖就没bug）。
本次作业实现了Network类和Person类。其中容器的选择，由于每个person都有着独一无二的id，那么使用Hashmap容器可以通过id快速获得对应的person，时间复杂度为O(1)，如果使用ArrayList遍历的话，如果person数量过多，可能会超时。
//Person
private final HashMap<Person, Integer> acquaintance;
//Network
private final HashMap<Integer, Person> idToPerson;
本次作业中，唯一可能产生较高复杂度的就是isCircle方法和queryNameRank。
其中queryNameRank方法由于数据条数的限制，按照JML规格通过循环判断的方法也不会造成很大的时间开销。如果希望让程序变得更快，可以使用平衡树、FHQTreap等数据结构来优化。
isCircle方法是查询两个人是否是连通的（在同一个社交圈子），如果使用dfs的话可能会TLE，因此笔者采用并查集，并且将并查集算法新建一个类UnionFind。
public Person find(Person p) {
if (p != personUnion.get(p)) {
int tmp = find(personUnion.get(p));
personUnion.put(p, tmp);
}
return tmp;
}
public void union(Person p, Person q) {
Person p1Root = find(p);
Person q1Root = find(q);
if (p1Root == q1Root) {
return;
}
if (personNum.get(p1Root) < personNum.get(q1Root)) {
personUnion.remove(p1Root);
personUnion.put(p1Root, q1Root);
int tmp = personNum.remove(q1Root);
personNum.put(q1Root, tmp + personNum.get(p1Root));
} else {
personUnion.remove(q1Root);
personUnion.put(q1Root, p1Root);
int tmp = personNum.remove(p1Root);
personNum.put(p1Root, tmp + personNum.get(q1Root));
}
count--;
}
本次作业强测和互测都没有bug，同时互测中同屋房间用同学被卡TLE，从侧面也验证了这次作业所采用的数据结构可以避免超时。
本次作业添加了Group类和Message类，但接口根据JML规格严格实现没有难度。
本次作业中的Group类中依旧采用Message独一无二的id作为键值，使用Hashmap存储。但Person中新增的对Message的管理由于需要根据添加的顺序完成相应的接口，因此Person中的Message容器使用ArrayList，并每次使用add(0, message)添加到头部。
本次作业新增的Group中有很多属性，并且Network中新增对这些属性的某些特征值的访问，如果按照JML规格所描述的get方法中进行值的获取，随着相关操作的次数增加，很可能出现TLE。因此笔者在addPerson以及delPerson中对相关特征值进行维护。例如addPerson中：
public void addPerson(Person person) {
people.put(person.getId(), (MyPerson) person);
ageSum += person.getAge();
int meanAge = getAgeMean();
ageVar = 0;
for (Person item : people.values()) {
ageVar = ageVar + (item.getAge() - meanAge) * (item.getAge() - meanAge);
if (item.isLinked(person)) {
valueSum = valueSum + item.queryValue(person) * 2;
}
}
ageVar /= people.size();
}
值得注意的是，在Network中的addRelation方法中，如果两个人已经在同一个Group中，那么此时需要更新Group中的valueSum。
本次作业由于粗心大意，在public int getAgeMean()方法中，没有严格按照JML规格考虑前置条件人数为0的情况，因此出现了除0的错误，强测中所有点全RE，因此最终也没有参与互测。
本次作业中，添加了不同类型的Message类，但均继承自Message接口，因此原有的数据结构不需要做出任何改变。
本次作业新添加的容器类型为优先队列PriorityQueue，用来对Dijkstra的堆优化。堆优化时间复杂度为\(O(mlogm)\)，不优化时间复杂度为\(O(n^{2})\)，容器中使用Pair类来保存到达每个点的最长路径，并添加comparable接口。实现方法为：
PriorityQueue<Pair<Integer, Integer>> queue = new
PriorityQueue<>(Comparator.comparingInt(Pair::getValue));
在deleteColdEmoji方法中，有对容器中的键对进行删除，如果在遍历过程中进行删除，可能会产生CurrentModification 错误，因此可以使用removeIf或者迭代器Iterator遍历删除。
如上面所说，本次新增的内容中，需要优化的是sendIndirectMessage方法，即在两个人之间寻找最短路并返回最短路的长度。
HashMap<Integer, Integer> distance = new HashMap<>(); //记录最短路
HashMap<Integer, Boolean> isVis = new HashMap<>(); //记录是否遍历过
distance.put(id1, 0);
queue.add(new Pair<>(id1, 0));
while (!queue.isEmpty()) {
Pair<Integer, Integer> pair = queue.poll();
int k = pair.getKey();
if (isVis.getOrDefault(k, false)) {
continue;
}
HashMap<Person, Integer> path = ((MyPerson) getPerson(k)).getPath();
for (Person person : path.keySet()) {
int val = distance.get(k) + path.get(person);
if (distance.getOrDefault(person.getId(), Integer.MAX_VALUE) > val) {
distance.put(person.getId(), val);
queue.add(new Pair<>(person.getId(), val));
}
}
isVis.put(k, true);
}
本次作业与其他同学对拍，因此强测中未发现bug。互测中被hack了一个数据点，发现是第二次作业遗留的bug，可能因为未参与互测，因此没被发现。具体原因为在delPerson方法中对所有属性进行更新的时候，通过年龄为0来判断是否人数为0，但年龄可以为0。
本单元的难度应该说是最低的，课程组提供了较为完备的JML规格，只需要按照规格一一去实现就不会出现正确性问题。但是给出的JML规格还有很多地方的不完善，比如语法、前置条件或后置条件的缺漏，希望课程组能够不断完善。
这也反映一个问题，JML规格在完备的优点下，对于其编写的复杂只会随着接口的功能增加而不断增加，几行的代码变成JML规格就会成为几十行，如果一个接口的功能较多，那么阅读理解JML规格就真的成为阅读理解了。这种机制实际上应用于合作开发的情况下实用率又会有多高。个人认为，JML规格可以用来培养规范的习惯，但到实际应用中不如使用正常的语言来描述，就像java官方包中的注释那样。并且目前完备的验证只能依靠人力，机器的验证只能是逻辑中很小的一部分，这一部分还需要很严格的规范体系。
原文：https://www.cnblogs.com/ycg1209/p/14824983.html