JML语言的理论基础及相关工具链
理论基础
JML(Java Modeling Language)是用于对Java程序进行规格化设计的一种表示语言。
注释结构
JML以javadoc注释的方式来表示规格，有行注释和块注释两种注释方式。其中行注释的表示方式为
//@annotation
，块注释的表示方式为
/*@ annotation @*/
。
常用JML表达式
-
\result
void
-
\old(expr)
expr
-
\forall
-
\exists
-
\sum
\product
\max
\min
\num_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语言的一些内部容器有了更多的认识。
本单元对JML的接触大多为阅读并理解，真正让我们手写的JML并不多，因此撰写JML的能力并不佳。但笔者认为，规格给予了实现人员自信，只要实现满足规格要求，就一定是正确的，同时规格也为程序测试的开展指明了方向。