需求：根据接口文件中的JML规格描述，实现一个初步社交模拟网络的模型。
对于大部分普通的方法，它的方法名就已经体现出它所要实现的大致行为。我们可以先通过方法名猜测基本功能，再通过JML规格验证。这种策略适用于细节比较少的方法。
对于比较核心的方法，实现细节比较多，需要我们认真啃大段的JML。首先我们可以通过各normal_behavior和exceptional_behavior的前置条件requires根据情况种类建一个大致框架，在每个情况种类下，理解每个ensures的真实意义，将其翻译成通俗易懂的点，进而理解每种情况下需要实现的行为。初始阅读时可能会有困难，阅读比较多的JML时容易发现某些大段的JML固定的对应于某些想要表达的意思。
当然，对于规格中的描述，我们需要理解其实现的本质，从而寻找合适的算法来实现。JML为了描述方便常会使用多重循环的方式来传达含义，如果我们在实现中也使用多重循环，那么性能自然会很拉跨，很容易被卡。比如如下表达：
/*@ ensures \result == (\sum int i; 0 <= i && i < people.length;
@ (\sum int j; 0 <= j && j < people.length &&
@ people[i].isLinked(people[j]); people[i].queryValue(people[j])));
@*/
此外，对于我们的迭代式开发，同样需要对于之前实现过的方法的JML进行关注，以防忽略方法发生了的变化。实际上可以写一个自动对比工具检查已经实现过的方法的JML规格的变动，可以大大提高效率。
以IDEA为例，配置好相关插件后可以自动生成测试框架，然后自己构造一些测试数据，通过assert语句进行判判断（assertTrue,assertEquals等）。
自动数据生成实现起来很简单，只是比较繁琐。结合讨论区同学推荐的NetworkX库可以对一些方法进行测试。但我们的指令操作比较多，只靠这个库来判断正确性会很难。
所以我们还可以找几个同学来进行黑盒测试，对比输出。
有时候重新阅读的时候收获还是蛮大的，注意一下细节（边界数据等），看是否遗漏操作，基本就没什么问题了。
对于常见容器，我之前也整理过，不过对于许多底层原理并没有深究。
对于List接口的具体实现，常用的主要有：
ArrayListLinkedList两者之间，LinkedList本质使用链表结构存储数据，因此比较适合数据的动态插入和删除。我们在Person类中存储的messages需要有序存储，并且需要频繁增删，因此用LinkedList比较合适。值得注意的是，对于存放Integer类型数据的ArrayList，当我们的remove方法传入的是Integer类型的数据，那么删除的就是第一次出现的Integer。如果传入的是int类型的数据，那么删除的就是int下标处的元素。
对于Queue接口的具体实现，常用的主要有：
PriorityQueue：优先队列ArrayDeque：基于数组的双端队列我们可以使用PriorityQueue来模拟小顶堆。
对于Map接口的具体实现，常用的主要有：
HashMapLinkedHashMapLinkedHashMap使用双向链表来维护key-value对的次序，其顺序与键值对的插入顺序一致，但因而查找效率有所降低。HashMap拥有O(1)+O(len(List))的读效率和写效率，如果将id存在key中，可以获得很高的查找效率，因此该容器使用比较多。
几次作业中的核心方法/容易出现性能问题的方法主要有：
第一次作业：
queryBlockSum，查询连通块数量第二次作业：
getValueSumgetAgeMeangetAgeVar第三次作业：
sendIndirectMessage，需要求解单源最短路对于连通块的合并、查询，如果刷过算法题的话应该比较容易想到并查集。当然tarjan也可以，但实现起来更复杂。对于第二次作业的几个方法，如果单次复杂度按照JML规格来写，为$O(N^2)$，很容易被卡。我们可以缓存valueSum、ageSum、ageVarSum，在每次addPerson和delPerson时更新所有缓存的值。对于单源最短路径问题，dijkstra和spfa用的比较多，我们的网络中没有负权边，所以dijkstra比较合适。听说裸的dijkstra可能会被卡，所以还是加一个堆优化更保险一点。毕竟priority_queue已经封装好了，不需要自己搓一个堆，加进去还是很容易的。
个人在第二次作业的几个方法中没有缓存，虽然苟过了强测，但在互测中被hack出了CTLE。
第三次作业：
本单元由于是实现官方接口，所以架构基本没有太大操纵空间。个人只是把所有的exception类放到exception包中方便管理。在第三次作业中多加了一个Pair类（jdk1.8还没有实现Pair...），用于存储每个节点的信息（id和距离）
并查集主要用于解决一些关于元素分组的问题，适用于需要频繁对于分组查询、合并操作的情况，单次查询时间复杂度为O(logN)
因此在本单元作业中，我们可以将并查集这一数据结构运用到查询连通块数量中。
Dijkstra 适用于求单源最短路径问题。算法中一个很大的性能浪费在于遍历所有的连接边，寻找距离最近的点，这样寻找的时间复杂度为O(N)。如果我们将距离用一个堆（优先队列）来存储，就可以将寻找点的时间复杂度降为 O(logN)
在第三次作业的sendIndirectMessage操作中，需要我们非直接相连点的最短路，可以采用该算法来实现。
从初读大段JML的生涩，到现在有了一个良好顺畅的阅读体验，本单元的学习也收获颇丰。印象比较深刻的是JVM垃圾回收机制的模拟和补全，这种与实际理论知识的结合和实现给我的体验要比模拟一个公交车行止更好，不过确实随之带来了一些难度上的增加。或许oo课程组可以考虑之后将单元任务与一些具体的知识背景相结合？这样带来的感觉更像是解决实际业务。
JML对于团队开发的规范确实有良好的效果，但其本身写起来很复杂。学生阶段的小团队或个人开发囿于时间精力的限制可能还是会追求短平快，写JML的时间可能和做整个项目的时间差不多，学了之后想必在之后的项目开发中还是很少会写JML。。但它的作用其实是更长期的，像比较大型的公司对于提交的代码都有严格的审查流程，例如巨硬，提交100行代码可能需要先自己写测试代码100+行，在这种大型团队配合的工作中，规格和测试的重要意义就会逐渐体现。
原文：https://www.cnblogs.com/mcrae/p/14836775.html