JML 规格设计分析

一、设计分析

1. 路径容器的规格设计

• 第一次作业需要实现一个路径管理系统，可以通过输入各种指令来进行数据的增删改查等操作。同时这一单元的三次作业中，都没有性能分的要求，有的只是受限制的 CPU 时间，这一次作业的 CPU 时间是 10 秒以内，又因为第一次作业设计的部分很少，所以只要不玩的太脱，几乎不会超时，换句话说，第一次作业几乎是人人满分。
• 我的程序架构中，使用了 ArrayList 作为 Path 类的存储结构，包含一条路径中的结点；使用三个 HashMap 作为 PathContainer 的存储结构，前两个分别是 pathid -> path 和 path -> pathid 的 HashMap，最后一个 HashMap 用于计算容器中每个点存在的次数，方便了 DISTINCT_NODE_COUNT 方法的计算，直接返回这个 HashMap 的 size 即可。

• 下面是第一次作业程序的 UML 类图：
  

• 从 UML 图可以看出我仿照着 Path.java 和 PathContainer.java 实现这两个类中的方法。

• Method 复杂度分析：
  

• Class 复杂度分析：
  

• 这两者的复杂度都控制得比较正常。

2. 图的规格设计

• 第二次 JML 的作业也不算很难，只是我觉得有点偏向数据结构的知识了，需要实现一个图的管理，图中包含路径，路径包含点。需要实现的方法中，最复杂的是找两个点之间的最短路径；这次作业限制的 CPU 时间为 20 s，这就比较严格地限制了我们不能在每次求最短路径时重新算整个路径，要不然很容易超时。
• 我第二次作业的程序架构，Graph 类包括了上次容器类的方法，然后另外建立了一个 HashMap 存储每个点的领结点，然后在需要求最短路径时再通过 Dijkstra 算法算得每个点与其他点的最短路径，并储存在上述 HashMap 中，这个设计是因为在我们的指令中，图结构变更仅有很少的 20 条，但是取最短路径的指令可以有 7000 条之多，所以，存储每次获取的最短路径，可以有效解决每次求最短路径都需要用 Dijkstra 算法检索一遍的问题，而可以直接在 HashMap 中搜索相关数据即可。

• 以下是第二次作业的 UML 类图：
  

• 和上次一样，使用了官方给的 Graph.java 并将容器类的方法添加在其中。

• Method 复杂度分析（只截取了复杂度较高的方法）：
  

• Class 复杂度分析：
  

• 从第二次作业开始，路径间互动的算法复杂度变高了起来。

3. 地铁系统的规格设计

• 最后一次 JML 作业需要实现一个地铁系统，新加入了票价、换乘、不满意度的概念，这导致了我们这次的作业复杂度成指数倍地增加，因为每一种计数方式都需要遍历所有的路线，并找到最小值，但是这次的 CPU 时间给的比较宽松—— 35 s，这次给了我们足够的想象空间，去构建我们想完成的数据结构。
• 第三次作业，我的想法是每个有多条路径通过的点来构造一个根点来连接其他所有的真实的点，再把这些真实的点当作伪点来连接当前路径中它要连接的点，说白了就是一个复杂的拆点，只不过这样可以大大减少我构造的图中的边的数量，从而大大减少 Dijkstra 从优先队列中取出最短路径的次数，缩短程序运行时间。
• 在构造完我所说的跟点的 HashMap 后，就可以将三种不同的算法各自构造一个 HashMap 作为点的边权来进行 Dijkstra 的计算，然后和上次作业一样把边权存储起来方便下次调用。
• 还有一个特殊的指令是获取地铁系统中所以连通块的数量，这个指令我是通过把容器中每一条路径的第一个点取出来，判断它们是否相连。

• 下面是最后一次 JML 作业的 UML 类图：
  

• 因为内部的方法比较复杂，我就不打开 method 展示了。

• Method 方法复杂度：
  

• Class 方法复杂度：
  

• 这次的复杂度比上次大大增加了，因为我在每次图结构变化的时候，都需要重构我的四个 HashMap ，所以相当于 50 次左右的重构图结构；相应的，获取四种最短的方法调用次数也有所增加。

二、Bug 分析

• 遗憾的是，这三次作业中，我都没有在互测中找到别人的 bug，我找 bug 的方式是利用输入相同的数据，然后判断两位同学的输出是否相同，来找出它们的错误，可惜的是三次互测中我给每组同学运行了上千组随机数据，他们都没有出现一例错误，可能这是因为 A 组大佬们太强了吧（得益于这个单元没有性能分，三次作业我在强测中都是满分）。
• 那下面我就来说说我自己程序在编写过程中遇到的 Bug ，或是超时问题：
  • 第一次我求最短路径时，每次调用两个点间的最短路径，我会遍历全部的点求得整个图的边权，后来我改进为只求当时那个点的边权，这样在图结构发生变化时，有效减少程序运行时间；
  • 第一次作业中的容器类，我原本用的是 ArrayList 存储 Path，但后来我发现这样用 pathid 来搜索 path 时，速度明显变慢，因为 ArrayList 本质上是一个数组结构，搜索时需要一个个按照索引来搜索，比 HashMap 通过 key-value 来搜索要慢的很多，所以后来我采用 HashMap 来存储。

三、JML 理论基础和工具链

• 这一单元我们的编程需求完完全全来自于 JML，所以 JML 知识的掌握对我们来说尤为重要；
• JML 又名 Java 建模语言，用于制定 Java 模块的行为，但是它又不需要完全精确到代码细节的实现，而是对某一个模块的行为进行规范；
• 一个正常的 JML 可以包含下面几个部分：前置条件、后置条件、会改变的元素和属性、不会改变的元素和属性、不正常的行为发生时抛出异常；这些具体实现的表达式也已经在我们的指导书中详细地介绍了，我在这里也简单梳理一下：
  • JML 中常用的表达式：
    • \old(expr) 表达式用来表示一个表达式 expr 在相应方法执行前的取值；
    • \result 表达式表示方法的执行返回结果；
    • \forall 表达式是全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束；
    • \exists 表达式是存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束；
    • \sum 表达式表示返回给定范围内的表达式的和；
    • \product 表达式表示返回给定范围内的表达式的连乘结果；
    • \max \min 表达式分别表示返回给定范围内的表达式的最大值和最小值；
    • <==> <=!=> 等价关系操作符： b_expr1<==>b_expr2 或者b_expr1<=!=>b_expr2 分别表示表达式相等或不等；
    • ==> <== 推理操作符： b_expr1 ==> b_expr2 或者 b_expr2 <== b_expr1 。
  • JML 中常用方法规格：
    • 前置条件 requires ：requires P 表示要求调用者确保 P 为真；
    • 后置条件 ensure ：ensures P 表示方法实现者确保方法执 行返回结果一定满足谓词P的要求，即确保 P 为真；
    • 副作用范围限定：关键词 assignable 表示可赋值，modifiable 表示可修改；
    • pure ：表示方法是纯粹的访问方法，不会对对象进行任何修改；
• JML 的工具链我熟悉的有以下两种：
  • OpenJML 用于验证模块是否完成 JML 规定的功能；
  • JMLlauncher 图形用户界面工具的启动器；
  • JMLdoc 包含 JML 规范信息的 javadoc 版本；
  • JMLUnit 用于自定义测试模块是否符合需求，之后会详细讲述。

四、部署 JMLUnit 并测试模块

• 部署 JMLUnit 的过程不算很复杂，从 GitHub 下载相应 jar 包，IDEA 安装 JUnit plugin，导入 jar 包，生成 JUnit 测试类即可；在 JUnit 测试类中用 assert 语句可以完成测试，如果不符合 assert 的要求则会报错，否则继续运行。
• 下面是我手动编写的部分测试程序：

/**
*
* Method: containsEdge(int fromNode, int toNode)
*
*/
@Test
public void testContainsEdge() throws Exception {
//TODO: Test goes here...path3 = new MyPath(1, 1);graph.addPath(path3);System.out.println("Test contains edges.");Assert.assertTrue(graph.containsEdge(1, 1));
}/**
*
* Method: getShortestPathLength(int fromNode, int toNode)
*
*/
@Test
public void testGetShortestPathLength() throws Exception {
//TODO: Test goes here...graph = new MyGraph();path1 = new MyPath(10, 11, 12, 13);path2 = new MyPath(13, 14, 15);path3 = new MyPath(11, 15);graph.addPath(path1);graph.addPath(path2);graph.addPath(path3);System.out.println("Test get shortest path.");Assert.assertEquals(graph.getShortestPathLength(10, 15), 2);}

• 下面是我的 JUnit 运行情况：
  

• 可以看出对我想要测试的类都完成了测试，并正确输出。

五、收获与总结

• 通过这个单元的三次 JML 作业，我认识到了 JML 的强大之处，它相当于调用者与函数之间的一个承诺，我给你一个输入，你必须返回相应的输出或抛出异常，这也是今后工作中会比较常见的完成工作的方式，需求通过 JML 给我们，我们完成相应的算法。
• 虽说这个单元是 JML 规格的练习，但在实际编写程序时，我反而不会细细研读 JML ，因为从指令的要求以及方法名也能看出某个方法的作用是什么，所以我希望多增加一些类似实验课上写 JML 的练习，可以督促我们更深刻地学习到 Java 建模语言。
• 话说回来，这个单元的三次作业其实也不算难，部分简单的 JML 中甚至给出了完成这个算法的方法，不过尤其是第三次作业，我觉得太偏向数据结构了，我甚至在地铁系统中用了不下十个 HashMap ；总的来说，这次规格的单元作业，我又掌握了新的领域的内容，收获还是蛮丰富的。