本次作业由于是按照以给的规格实现功能，总体来说很多函数的书写可以按照JML的书写逻辑直接照搬。但是对有些有性能要求的函数来说，其算法需要自己去书写。并且在总体函数输入输出可以保证的情况下，其内部的数据结构实现，逻辑实现完全可以自由发挥。
比如在Network类里，我的数据结构使用如下：（为了更优的查询性能，全部使用了Hashmap）
private HashMap<Integer, Person> people = new HashMap<>();
private ArrayList<HashMap<Integer, Person>> relationMap = new ArrayList<>();
private HashMap<Integer, Group> groups = new HashMap<>();
private HashMap<Integer, Message> messages = new HashMap<>();
private HashMap<Integer, Integer> emoji = new HashMap<>();
又比如在sendMessage函数中，JML要求的是新的信息应当插到信息容器的前面
@ensures (\forall int i; 0 <= i && i < \old(getMessage(id).getPerson2().getMessages().length);
@ \old(getMessage(id)).getPerson2().getMessages()[i+1] == \old(getMessage(id).getPerson2().getMessages()[i]));
@ ensures \old(getMessage(id)).getPerson2().getMessages()[0].equals(\old(getMessage(id)));
这是因为Person的getReceivedMessage函数中，需要选取最新的几个message，就是说message这个容器需要有序
但是考虑到性能方面，我实际上是采用了尾插，然后get的时候从后面反向读，一样实现了需求。
至于那几个核心的性能要求的函数，将在下面介绍
废话少说，上图（没有异常类
作业的架构大体上就是按照标准的来（甚至名字也听取了课程组的建议），Person以Group的方式组织，可以在Network里实现Message的分发，以及增添改查功能。数据结构方面，能使用Hashmap的地方完全使用了Hashmap。下面来分函数具体说一下：
HW11唯一的难点在于一个求最短路的函数send_indirect_message。显然普通的Dijkstra是满足不了需求的，所以我上网学习了堆排序改进的Dijkstra算法，并利用java的数据结构PriorityQueue来实现堆。在学习算法时，显然我并没有完全理解其优化本质。我的做法是对于每一个连通Block里的人，包装成Pair，全部加入堆中，更新到达最短路长度，poll点更新，如此反复。算法复杂度依旧很高，仅仅是把Dijkstra的找最小路径的部分简化了，但优化不大，很遗憾的强测挂了一个点。
PriorityQueue的使用实际上也是一个难点。其必须要在取出元素或者新加入元素的时候才可以排序，并且排序完的队列只可以通过特定方法依次取出，不可以擅自更改其中元素的信息。并且，由于我需要排序的是包含距离信息的Person，所以新建了一个类Pair来存储，并重写了其的compareTo方法，继承了comparable接口
public int compareTo(Pair o) {
if (distance > o.getDistance()) {
return 1;
} else if (distance < o.getDistance()) {
return -1;
}
return 0;
}
原文：https://www.cnblogs.com/tonymwt/p/14828964.html