JML（Java Modeling Language）是用于对Java程序进行规格化设计的一种表示语言。ML是一种行为接口规格语言(Behavior Interface Specification Language, BISL)，基于Larch方法构建。BISL提供了对方法和类型的规格定义手段。所谓接口即一个方法或类型外部可见的内容。（源自JML使用手册）
JML在Java代码中增加了一些符号，这些符号用来标识一个方法是干什么的，却并不关心它的实现。如果使用JML的话，我们就能够描述一个方法的预期的功能而不管他如何实现。通过这种方式，JML把过程性的思考延迟到方法设计中，从而扩展了面向对象设计的这个原则。
\result
\old()
\not_assigned()
\not_modified()
\nonnullelements()
\type()
\typeof()
\forall
\exists
\sum
\product
\max
\min
\num_of
E1<:E2
// 如果 E1是 E2的子类型或者与 E2类型相同，则返回真
// 注意任何类型都是 Object类型的子类型
123
b_expr1<==>b_expr2
b_expr1<=!=>b_expr2
// <==> 比 == 的优先级低
// <=!=> 比 != 的优先级低
1234
b_expr1==>b_expr2
// 当 b_expr1==false || b_expr1==true || b_expr2==true 时，为 true
b_expr2<==b_expr1
123
assignable \nothing
// 当前作用域下每个变量都不可以在方法执行过程中被赋值
主要是实现 person 类和network类，包裹对简单社交关系的查询和模拟，并且理解基础JML入门级规格。
Person类中根据acquaintance和value的特性选择了Hashmap存储，根据本次作业JML中的整体理解猜测可能在社交网络模拟当中对这两个容器的查询比例较大，在取舍之下采用Hashmap来减少时间复杂度。
Network类中也考虑到实现当中需要不断地查询people当中的每一个Person，所以也采用了Hashmap来存储信息。
本次作业主要是严格按照JML规格来实现操作，没有什么算法方面的策略实现，第一次作业在isCircle和queryBlockSum这两个方法中采用的是深度遍历方法，比较无脑，时间复杂度很高（O(n2)），没有考虑优化，第一次作业可能没有严格考察时间复杂度，为后续的翻车埋下伏笔。
本次作业整体设计比较简单没有考虑太多，但是在最关键的地方却犯了错误，就是在实现queryBlockSum的时候在iterator迭代器实现hashmap的迭代的时候出现了疏忽，导致强测出现了问题。最后对比学习了一下hashmap的foreach和iterator遍历
foreach:
import java.io.IOException;
import java.util.HashMap;
import java.util.Map;
public class Test {
public static void main(String[] args) throws IOException {
Map<Integer, Integer> map = new HashMap<Integer, Integer>();
map.put(1, 10);
map.put(2, 20);
// Iterating entries using a For Each loop
for (Map.Entry<Integer, Integer> entry : map.entrySet()) {
System.out.println("Key = " + entry.getKey() + ", Value = " + entry.getValue());
}
}
}
iterator:
import java.io.IOException;
import java.util.HashMap;
import java.util.Iterator;
import java.util.Map;
public class Test {
public static void main(String[] args) throws IOException {
Map map = new HashMap();
map.put(1, 10);
map.put(2, 20);
Iterator<Map.Entry> entries = map.entrySet().iterator();
while (entries.hasNext()) {
Map.Entry entry = (Map.Entry) entries.next();
Integer key = (Integer) entry.getKey();
Integer value = (Integer) entry.getValue();
System.out.println("Key = " + key + ", Value = " + value);
}
}
}
在第一次作业的基础上完善社交网络的模拟，使得对社交网络中数据的操作更加丰富。
原有的容器并未改变。
在Person类当中出现了新增的messages类型，对其操作的观察发现主要是获取一个Person当中的messages列表，所以综合考量对时间复杂度的影响以及操作的简化采用了Arraylist类型来存储。
在Network当中新增了两种类型messages和groups，通过Network接口中JML规格的观察分析，发现对group当中涉及到的查询age、value等数据操作比较多，而message操作更多的涉及到增加和删除。
所以在综合考量之下：groups采用了Hashmap容器减少查询时间复杂度，messages则采用Arraylist容器简化操作、减少增删的时间复杂度。
主要设计也没有采用很巧妙的方法，在Group类当中设计了几个全局成员变量用来保存年龄之和以及people的size大小。
private int tage;
private int size;
public void addPerson(Person person) {
people.add(person);
tage += person.getAge();
size += 1;
}
主要是减少了后续查询当中再次遍历的时间，也算是一点小小的优化。
这里要强调的就是别忘记了在最后del操作中对其进行处理：
public void delPerson(Person person) {
people.remove(person);
size -= 1;
tage -= person.getAge();
}
本次作业的大BUG就是来自于第一次作业对于性能的忽视，导致强测结果很惨，立马灰溜溜的去修改了前面的伏笔，isCircle采取了并查集的办法：
主要思路就是将一组关系加入到一个hashmap当中，然后需要使用时递归查询两组关系的是否有最近的共同祖先。
private HashMap<Integer, Integer> father;
public int getF(int id) {
int idF = father.get(id);
if (id == idF) {
return id;
}
father.replace(id, getF(idF));
return father.get(id);
}
public void addPerson(Person person) throws EqualPersonIdException {
int ida = person.getId();
if (contains(ida)) {
throw new MyEqualPersonIdException(ida);
}
people.put(ida, person);
people1.add(person);
father.put(ida, ida);
}
public boolean isCircle(int id1, int id2) throws PersonIdNotFoundException {
if (!contains(id1)) {
throw new MyPersonIdNotFoundException(id1);
}
else if (!contains(id2)) {
throw new MyPersonIdNotFoundException(id2);
}
return getF(id1) == getF(id2);
}
这样来看使用并查集大大简化了时间复杂度，同样也简化了操作复杂度，值得反思。
本次作业完善了社交网络中的消息传递，增加了几种消息类型并实现了对消息的分析处理。
在Network当中新增了emojiId和emojHeat两种数据类型，这里的选择还是根据其中具体的操作实现来选择合适的容器。通过对JML的阅读，发现emojiId当中添加删除与查询的操作比例相当，所以在权衡时间情况以及代码简化方面采取了Arraylist来存储，而emojHeat当中涉及到的查询与修改操作较为频繁所以采用了Hashmap存储。
由于吃了第二次作业的亏，这次实现策略方面好好考虑了一下，其中三个Message的子类严格按照JML实现就OK。
主要是在sengIndirectMessage当中要判断两者之间的社交网络最短路径，主要是使用了迪杰斯特拉算法，但是在与同学交流之后，学习采用了实验上机当中官方代码的堆来维护图，使得算法稳定性更强。
首先新建一个容器存储每一个Person所连接的people.size()，这里使用了Hashmap来存储，可以更加直观的查询到每一个person所对应的社交人数。
private HashMap<Integer, Integer> idIndex;
//实现在需要修改Person的关系时
idIndex.put(ida, people1.size());
然后使用java面向对象的思路设计一个Gv数组和Ev类分别表示节点以及直接路径。
public class Ev implements Comparable<Ev> {
private int t1;
private int w1;
Ev(int t, int w) {
this.t1 = t;
this.w1 = w;
}
public int getT() {
return t1;
}
public int getW() {
return w1;
}
@Override
public int compareTo(Ev o) {
return w1 - o.w1;
}
}
//Network
private static ArrayList[] Gv = new ArrayList[5005];
//增添关系时
Gv[in1].add(new Ev(in2, value));
Gv[in2].add(new Ev(in1, value));
最后实现最短路径寻找：和经典算法一样设计两个数组记录两点之间的最短路径和是否访问，通过while的迭代查找，每次不断替换较小的路径，这里使用了优先队列来维护每次替换后的结果，优化了迪杰斯特拉算法。
private int minPath(int s, int n) {
boolean[] visited = new boolean[5001];
int[] path = new int[5001];
Arrays.fill(path, 0x7fffffff);
Arrays.fill(visited, false);
PriorityQueue<Ev> que = new PriorityQueue<>();
que.add(new Ev(s, 0));
path[s] = 0;
while (!que.isEmpty()) {
int u = que.poll().getT();
if (visited[u]) {
continue;
}
visited[u] = true;
for (int i = 0; i < Gv[u].size(); i++) {
Ev temp = (Ev) Gv[u].get(i);
if (path[temp.getT()] > path[u] + temp.getW()) {
path[temp.getT()] = path[u] + temp.getW();
que.add(new Ev(temp.getT(), path[temp.getT()]));
}
}
}
return path[n];
}
这次出现的BUG很玄学，首先是在addMessage当中实现了三个异常的处理，但是在更改的JML之前，在方法声明的异常只有两种······，后面修改了之后一直没有发现push版本的忘记修改了·······最后自己本地也是正确的只有库里是错误的。非常的悲伤，也提醒自己在完成代码项目的时候要统观全局，多回头看看。
总结来说本单元的难度很小，相比于前一个单元无伤通关来说，这一单元值得反思，在阅读JML的时候容易疏忽，而且在这种代码补充的训练当中没有统筹全局，只顾着自己的小部分，反而丢失了之前的严谨审查、前后逻辑推理的习惯，只关注JML当中的内容，最终总是出现一些小问题导致失分，这一单元汲取了很多教训，也希望自己以后能够更加认真细致。
同样在JML规格的阅读和实现当中学习到了很多，首先从阅读方面提升了代码阅读能力，对JML的理解加深了不少。然后从规格的角度加深了对功能实现以及测试的理解，学习到了更加严谨规范的方法。最后收获还是不少，同样在这一单元的迭代训练中对面向对象的理解和实现也加深了不少。
原文：https://www.cnblogs.com/Aaron-Huang0101/p/14818953.html