JML语言的理论基础及相关工具链
理论基础
JML(Java Modeling Language)是用于对Java程序进行规格化设计的一种表示语言。
注释结构
JML以javadoc注释的方式来表示规格，有行注释和块注释两种注释方式。其中行注释的表示方式为//@annotation，块注释的表示方式为/*@ annotation @*/。
常用JML表达式
-
esult表达式：表示一个非void类型方法执行后的返回值。 -
old(expr)表达式：表示一个表达式expr在相应方法执行前的值。 -
forall表达式：全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。 -
exists表达式：存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束。 -
sum、product、max、min、um_of表达式。 -
等价关系操作符
<==>、推理操作符==>。
方法规格
-
前置条件，通过
requires子句来表示，给出方法调用的约束。 -
后置条件，通过
ensures子句来表示，给出方法执行结果的限制。 -
副作用约束，通过关键词
assignable或modifiable指定，给出方法在执行过程中会修改的属性数据或者类的静态成员数据。 -
纯粹访问性方法，通过关键词
pure指定。 -
异常功能规格，通过
public exceptional behavior、signals等句式来表示。
类型规格
-
不变式，要求类成员在所有可见状态下都必须满足一些特性。
-
状态变化约束，要求类成员在状态变化时满足一定条件。
相关工具链
-
OpenJML，笔者未能成功部署环境，但听闻该工具多年未维护，JML语法支持面小，功能有限。
-
JMLUnitNG，用于随机生成测试用例，主要对边界情况进行考察。总体而言，数据覆盖度较低，测试效果较差。
-
JUnit，成熟的单元测试工具，笔者在测试程序的基本功能方面，有较好的体验。
作业架构
本单元的作业着重考察图论算法，可剥离社交网络的外壳而抽象出一个图类，针对不同的操作动态建图，但课程组下发的Person接口已经足够完善，无需额外封装，故笔者并未尝试完成这项工作。
本单元架构明显，人作为点，关系作为边，实现差异主要体现在两方面——容器选择、算法选择。容器选择方面，笔者的理念是，尽可能多的使用性能良好的HashMap。算法选择方面，笔者的理念是，在不超时的情况下，尽可能多的使用朴素易懂的简单算法。
第一次作业
容器选择方面：
-
MyPerson类持有一个HashMap<Person, Integer>对象，存储与之相关的人和关联值，人作为key，关联值作为value。 -
MyNetwork类持有一个HashMap<Integer, Person>对象，存储关系网中的所有人，人的id作为key，人作为value。
算法选择方面：
第一次作业仅涉及到两点的连通性问题，算法具有多中选择，如深度优先搜索算法、广度优先搜索算法、并查集算法等。笔者选用了朴素的广度优先搜索算法。
第二次作业
第二次作业新增组的概念，组是人的集合。
容器选择方面：
-
MyGroup类持有一个HashMap<Integer, Person>对象，存储组中的人，人的id作为key，人作为value。 -
MyNetwork类持有一个HashMap<Integer, Group>对象，存储关系网中的所有组，组的id作为key，组作为value。
算法选择方面：
组的属性均可以进行维护，且仅在两种情况下需要维护：在向组中添加人时、在向身处同组的两个人间添加关系时。
第三次作业
第三次作业新增组内人员可删去的情况，同时涉及到了求图中连通块个数、求两点最短路径权值、判断两点是否在同一环路中等问题。
算法选择方面：
-
由于本次作业更多的涉及到了两点连通性的询问，笔者为了加速两点连通性的判断以及捎带求图中连通块个数，更换广度优先搜索算法为并查集算法。
MyNetwork持有一个HashMap<Person, Set<Person>>对象，人作为key，人所处的连通块作为value。每当向图中新增人时，新增一个仅包含此人的连通块。
每当向图中新增关系时，判断此关系涉及的两人是否在同一个连通块里，若不在，则合并两人所在的两个连通块。
此时，判断两点是否连通，即判断两点是否在同一个连通块中，时间开销大大降低。
-
由于本单元作业有较多的动态加点和动态加边操作，笔者在求两点最短路径权值的问题上，放弃了Floyd算法，选择了堆优化的Dijkstra算法。算法详解可参考《算法导论》。
-
本次作业讨论区中出现了笔者闻所未闻（太菜了555）的点双连通分量等概念，于是笔者学习了相关知识，在判断两点是否在同一环路中的问题上，选择了Tarjan算法。算法详解可参考《数据结构与算法分析》。
代码实现bug
笔者在三次作业中均未发现bug，互测房间其他人的bug主要为运行超时，原因多为算法实现问题，如：第二次作业中不对组的属性进行动态维护、第三次作业中在判断两点是否在同一环路中时使用复杂度较高的算法等。
心得体会
在完成本单元作业的过程中，笔者更多的还是专注到了图论算法中，回顾了很多漂亮的算法实现，也对java语言的一些内部容器有了更多的认识。