OO Unit 3 JML

目录

• 梳理JML语言的理论基础、应用工具链情况
  • JML语言理论基础
  • 各种工具支持
• 部署JMLUnitNG/JMLUnit
  • OpenJML的检查
  • JMLUnitNG的部署。
• 按照作业梳理自己的架构设计，并特别分析迭代中对架构的重构
  • 架构设计
    • 关于数据结构
    • 算法实现设计
      • 最短路径Floyd算法
      • 最低票价、最少换乘、最小不满意度
      • 复杂度优化
• 按照作业分析代码实现的bug和修复情况
  • 关于JUnit测试
• 阐述对规格撰写和理解上的心得体会

梳理JML语言的理论基础、应用工具链情况

面向对象编程思想中有一个重要原则就是尽量推迟过程性的思考。在实现一个程序时，首先考虑的不是先做什么后做什么，而是以具体的事物为单位，考虑它的属性和行为动作。就像先把主人公和主人公做的事情放进故事中，然后再填充人物之间的对话和交往。

JML语言理论基础

JML是一种规范java语言的程序，使用前置、后置和不变量等等约束，形成一种契约式设计。JML作为java的注释可以写入源文件，并且可以使用openJML进行检查。通过JML的规约来检查代码静态、动态时候的正确性。
语法
requires 定义了一个先决条件
ensures 定义了一个后置条件
signals 定义了后续方法抛异常时的后置条件
assignable 定义了允许继续执行了后面方法的条件
pure 声明一个方法是没有副作用的
invariant 定义了一个方法的不变的属性
esult 定义了返回值需要满足的要求
old(expression) 用于表示进入方法之前表达式的值
(forall <decl>; <range-exp>; <body-exp>) 全称量词
(exists <decl>; <range-exp>; <body-exp>) 存在量词
a==>b a推出b
a<==b a隐含b
a<==>b a当且仅当b
以及，JML注释可以访问Java对象，方法和运算符。对象和方法对于JML有一定的可见性，同样可以通过关键字例如spec_public来规定。

各种工具支持

有很多应用工具能够提供给JML编译和检查的支持。比如lowa State JML工具提供了一个断言检查编译器jmlc，将JML注释转换为运行时的断言，一个文档生成器jmldoc，用于生成Javadoc文档，增加了来自JML注释的额外信息。以及一个单元测试生成器jmlunit，它可以从JML注释中生成JUnit测试代码。

部署JMLUnitNG/JMLUnit

针对Graph接口的实现自动生成测试用例， 并结合规格对生成的测试用例和数据进行简要分析。

OpenJML的检查

由于我的代码和标程给的JML有点不同，从命名到实现上。所以报错非常多。

JMLUnitNG的部署。

在Jar包的导入部分经常会出问题。可能是mac系统的缘故。运行JMLUniting，会生成很多个测试类，之后，在idea里可以运行带有main函数的Main_JML_Test类，利用JML对各个方法进行测试。

按照作业梳理自己的架构设计，并特别分析迭代中对架构的重构

架构设计

本次作业主要填充其中的几个核心的类，所以不需要考虑前后输入输出的问题，大大简化了细节的设计与思考。三次作业通过迭代，逐渐写成了一个初步的地铁线路查询无向图。主要分为几个类：

• 作业一的
  Path 单条路径
  PathContainer 一个路径的容器类，像一个玻璃瓶子，能看到里面所有的路径的情况，而不对路径进行进一步处理和计算，只负责增减和查询工作。
• 作业二的
  Graph 图类，这个类继承了PathContainer，并在此基础上增加无向图的一些概念，点、边、连通、最短路径。
  RailwaySystem 地铁系统，这个类继承了Graph，并在此基础上增加了最少票价、最少换乘、最低不满意度、连通块。这些需求实际上是对离散数学中的带权无向图的一个改进版，所以实际上是一个问题，可以用相同的思路解决。后续会详细说明。
  在上述的这些类中，分别定义了每一次迭代新增的需求。老师在上课的时候也有提到，在产品迭代更新的时候尽量不去修改原有的那些代码，即使他是不完善的，应该是再打一个补丁似的在外围添加。正如这单元的作业。
  因此实际上在迭代的过程中并没有对之前的架构进行重构，确保每一次迭代时，都用了性能较好的方法，那么在后续增加新需求的时候，只需要在外围进行扩展，不需要对之前的已经实现的代码进行改动。

关于数据结构

Hashmap中的Hashcode和equals的重写
本次作业用到了Java中的Hashmap，和C语言中的类似，只是调用起来更加方便。在研讨课上，有同学也分享了他对Hashmap和treemap的理解。关于Hashcode和equals的重写比较重要。在比较key的时候，Java会先比较Hashcode是否一致，若一致再比较equals。而对于一个对象，它的Hashcode是基于它在内存中的地址计算得到的，因此，如果hashmap的key是一个自定义类，想要自定义他们等同的条件，需要重写Hashcode和equals方法。对于Hashcode的重写，通常只将想要作为比较条件的部分写入，equals也是一样。比如：

for(int node: nodes)
    hash = 31 * hash + node;

采用31的原因是加快计算过程，31是1<<5-1，是计算机比较擅长的移位和减法运算。而且31是质数，不同对象的hashcode重合度比较低。

Hashmap与数组的选择
在PathContainer中用的Hashmap存放路径和id，访问时间复杂度是O(1)，是我能想到的最好的方式。之后在无向图的Floyd或者Dijkstra的计算中，用的是二维数组，虽然二者复杂度都是O(1)，但是对数组的访问要比Hashmap快很多，而且数组的书写简便，不需要考虑太多语法上的问题，可以使得思考重点放在算法上而非语法，思路更清晰。但是在部分实现上还是用Hashmap更好，尤其是那些不需要频繁访问，但每次访问如果不用hashmap就只能遍历查询的。比如node2Index和index2Node。两两为一组乱序存放，Hashmap很擅长做这种事情。

算法实现设计

总的来说用了Floyd和Dijkstra算法，来计算带权连通图的最短路径、最小票价、最少换乘次数和最小不满意度。

最短路径Floyd算法

首先都要准备一个邻接表。

• 先构造边的集合。
  为了简化图结构变更之后初始化邻接表的过程，我将邻接表用一个Hashmap存储，其中key是Pair类型的，是一条边的两个点，value是这条边出现的次数，记录次数是为了能够在增加边和删除边的时候能够直接对这条路径上的数目进行操作，而非从所有路径开始重新绘制一遍邻接表，当路径中节点数交多少时，可能这一步会消耗大量的时间。
  需要注意的是，为了节省Hashmap的开支，最好在边数变成0的时候把这个key删掉。简化的代码如下：

// pair表示这一对点
if (neighborTable.get(pair) == 0) {
	neighborTable.remove(pair);
}

• 在边集构造完毕之后，可以开始构造二维数组邻接表：

private void initMap() {
        for (int i = 0; i < distinct.size(); i++) {
            for (int j = 0; j <= i; j++) {
                if (i == j) {
                    map[i][j] = 0;
                } else {
                    int nodei = indexNode.get(i);	// index 2 node
                    int nodej = indexNode.get(j);	// 是一种从数组索引到实际节点编号的映射
                    if (containsEdge(nodei, nodej)) { // 邻接
                        map[i][j] = 1;
                        map[j][i] = 1;
                    } else {						// 不邻接，则为无穷大，这里选择250是因为不可能会有两个点的最短路径大于点数-1
                        map[i][j] = 250;	
                        map[j][i] = 250;
                    }
                }
            }
        }
    }

Floyd算法或者Dijkstra算法
本身理解起来比较简单，就是把两个点之间新增一个中转站之后能比原来的路径更长，如果有比已经存下的路径更短的就更新最短路径。
关键点在于几个可以优化的地方。首先，一个完整的Floyd本身的复杂度是O(n^3)，但是由于题目的简化，实际上我们可以把它的复杂度的常系数减小。见注释。

private void Floyd() {
        for (int mid = 0; mid < distinct.size(); mid++) {
            for (int i = 0; i < distinct.size(); i++) {
            // 第一处，j<i，可以借助无向图的矩阵对称性来将复杂度的常系数减小一半。
                for (int j = 0; j < i; j++) {
                // 第二处，如果两个点之间的距离已经是1，即他们通过一条边相连，那么就不存在有一个点，能够满足floyd优化条件。所以直接跳过 
                    if (map[i][j] == 1) {
                        continue;
                    }
                    // 第三处，如果这个中间点无法到达这两个待优化的点，那么这个中间点一定不能优化这一条路径。所以直接跳过
                    if (map[i][mid] < 250 && map[mid][j] < 250) {
                        if (map[i][j] > map[i][mid] + map[mid][j]) {
                        // 此处也是利用了矩阵的对称性，所以要同时改变对称的两个元素。
                            map[i][j] = map[i][mid] + map[mid][j];
                            map[j][i] = map[i][mid] + map[mid][j];
                        }
                    }
                }
            }
        }
    }

虽然缩小了常系数到原先的一半以内，但是他的复杂度还是O(n^3)，还是非常可观的。

最低票价、最少换乘、最小不满意度

这三个我用的是同样的方法cal()，只是改变了其中的变量所表示的带权图和换乘时候的代价。
在调用这个方法的时候，必须指定指令，type是一个枚举类型。

enum Type {
    TRANSFER, TICKET, UNPLEASANT
}

在计算这三条指令的时候我用的是Dijkstra算法。它的复杂度实际上和Floyd差不多。计算单点最优是O(n^2)。所以当查询数目少的时候，会比Floyd浪费的计算量更少一些。
只需要在计算之前询问，以该点为起始点的该指令的最优是否已经被计算过，并且没有图结构的更改。如果图结构没有更改，并且这个点为起始点的Dij已经计算过，那么就不必进行重复计算，可以直接输出相应二维矩阵的结果。截取相关代码片如下。

	// 检查图结构是否被更改。
	// 如果被更改，就初始化三个带权图，也初始化用于标记是否已经计算过最优的标记数组。
	checkMapModified(); 
	// 如果没有计算过以这个点为起点的Dij
	if (!counted[index1]) {
			// 那么就计算Dij
            askedMap = cal(Type.EXAMPLE, index1);
            // 并且把这个点标记为已计算
            counted[index1] = true;
    }
    // 如果已经计算过，那就输出询问的指令的对应结果
    return askedMap[index1][index2];

然后根据指令类型来选择合适的带权图map，以及换乘代价w。

private int[][] cal(Type type, int index1) {
        // 选择合适的二维矩阵 map 和换乘代价 w
        int w = 0;
        int[][] map = new int[1][1];
        if (type == Type.TRANSFER) {
            map = transferMap;
        } else if (type == Type.TICKET) {
            map = ticketMap;
            w = 2;
        } else if (type == Type.UNPLEASANT) {
            map = unpleasantMap;
            w = 32;
        }
        // Dijkstra 算法省略
        return map;
    }

复杂度优化

因为图结构变更的指令数被限制，而询问的指令数非常多，因此必须把复杂度都放在图结构变更的指令中，尽量减少询问的复杂度。所以在每一次add路径的时候，就计算他们各自的三个小矩阵——单条路径三种指令的结果。然后在询问的时候，现将所有小矩阵的值整合进大矩阵中，作为矩阵的初始化，然后计算大矩阵中的结果。这样可以省略大矩阵计算中，对于每条路径、每个点的从头的初始化，而是每条路径已经算好各自的最低票价等等，作为一个打包好的完整的小矩阵传递给大矩阵，只需要注意小矩阵的nodeid和index的映射关系与大矩阵中的不同即可。而在删除路径的时候也是同样，因为路径被删除，而小矩阵是封装在路径中的三个数据成员，也被同时删除。

按照作业分析代码实现的bug和修复情况

• 两个对象的比较
  Pair是Java自带的一个类。与Hashmap非常类似。它的key和value我虽然设置的是integer类型，这是int的一个包装类，但是不能直接用等号比较数值大小，因为他会比较hashcode而不是数值本身。所以应该重写比较，可以重写运算符但这比较麻烦，可以利用已有的方法比如compareTo()，或者自定义一个比较的方式，仅对数值本身进行比对。
• 更新矩阵的合适时机
  由于我的图结构变更指令和计算最短路径之类的不在一个类里进行，所以必须通过传信号值的方式进行交互。在查询指令进入的时候，先询问另一个类，是否有图结构的变更，如果有的话就初始化计算相关的mark，如果没有变更，就按现有的图进行计算。
  我原来的错误代码摘抄如下：

if (neighborTable.containsKey(pair)) {	
// 如果在邻接表中本来就有这个边
	neighborTable.put(pair, neighborTable.get(pair) + 1);  
	// 那么就让这个边出现的次数+1，其实次数与邻接表的元素是1还是0并没有太大的关系，只是方便在图结构变更的时候进行更新和统计
} else {
// 如果在邻接表中本来就没有这个边
    neighborTable.put(pair, 1);
    // 那么就把这个边放入邻接表中
    updatedThere = false;
    // 并且在另一个类里的计算都要重新来过
}  

但是实际上在每次图结构变更的时候都需要更新另一个类里的计算，因为关系到换乘，即路径本身的更换，而不仅仅是邻接边的问题。所以在每次路径的添加与删除的时候都需要重新计算三个指令相关的矩阵。
所以正确的代码应如下：

if (neighborTable.containsKey(pair)) {	
	neighborTable.put(pair, neighborTable.get(pair) + 1);  
} else {
    neighborTable.put(pair, 1);
}  
updatedThere = false;

• Floyd和Dij算法上出现的问题
  这个是我朋友碰到的问题，她自己并不能发现这个bug，因为整个程序是她写的，所以他会忽视一些她自己觉得很对绝对不可能出错的部分，但是往往这些被忽视的部分一旦出现错误就很难被发觉。而别人去看她的代码的时候我会从头开始捋一遍她的逻辑，就能很好的发现问题。
  就是在优化的时候，我们通常来说可以通过图的对称性来减小一半的复杂度，以及在确定已经是直接连通的边的时候就不需要继续计算。或者可以参考网上其他一些对Floyd、Dij的优化方案，比如利用堆排序、上三角等。
  每次都有bug但还是AC了所有强测点我觉得自己非常侥幸。其实还是对逻辑的不清晰。以后在设计各个数据成员、信号的时候，必须明确每一个信号的作用和值变化的时机，其实JML就在做这个事情。

关于JUnit测试

使用JUnit测试的时候，因为我们已经写了JML，所以在划分等价类的时候会更加容易一些。这样有利于我们构造尽量覆盖所有组合情况的测试集。

实际上，针对不同的实现思路，适合每个程序的测试类的划分也是不同的。就我个人的数据结构而言，划分等价类如下。

containsEdge

1. 两点都在图中
   • from == to
     • 边存在
     • 边不存在
   • from != to
     • 边存在
     • 边不存在
2. 有点不在图中

因为我的做法是把所有的边都放进一个Hashmap中，所以如果碰到from == to这种边，会给同一个key增加两次value，而实际上他们的边只出现了一次。会导致出错。

isConnected & getShortestPathLength
这个方法在实现的时候我先构造的邻接表，然后计算了最短路径，如果最短路径不是无穷大那就说明是连通的。
所以测试这个方法的划分与最短路径可以一起。

1. 两点都在图中
   • 存在边可以直接相连 - 测试邻接表的构造
   • 不存在直接相连的边但是可达 - 测试最短路径FLoyd的正确性
2. 有点不在图中。
3. from==to
   • 可达
   • 不可达

地铁系统的三个方法
这三个有异曲同工之妙，其实用的都是同一套方法。

1. 两点都在图中
   • 不换乘
   • 需要换乘
     • A 换乘 B 又换乘 C
     • A 换乘 B 又换乘 A
2. 有点不在图中

指令排列组合
实际上，测试单个方法很少出错，最容易出错的是指令组合之后，什么时候需要计算，什么时候需要更新的逻辑问题。

图结构变更指令
在这里我有出现过一个bug，究其原因，是没分清各个指令在什么时候应该重置初始化。
是否可达，以及最短路径，以及连通块数目，应该是在邻接表变更的时候重新算一遍。
而其他关系到换乘的指令，应该是有路径的增删的时候就应该重新算一遍。
所以测试集应该这样划分：

1. add + isConnected
   add + blockCount
   add + getShortestPathLength
2. add + price
   add + transfer
   add + unpleasant
   其中的add还应该更换成remove再检查一遍。

在利用JUnit进行测试的时候，利用断言来检查各个测试用例是否正确执行。

阐述对规格撰写和理解上的心得体会

规格很烦，但是很棒。我很喜欢这种契约式的思想，以及在编写代码之前就把这个方法或者这个类设计好，设计充分之后再着手思考应该用怎样的算法去实现，避免重构。

• 首先可以将每个方法的功能划分清楚，避免重复。
• 其次，在设计过程中，不去想如何实现的问题，不会受到具体算法过程的干扰，这样就能把关注点倾注在功能本身，在设计的时候思路更清晰。
• 副作用清晰明确。我的其中一个bug就是在add和remove路径的时候，除了往PathContainer里放路径或者删路径，还有一些其他的附加操作，比如更新一些信号量。这些信号量的选择性更新，对于代码逻辑也是一个challenge。如果我在写代码之前，把这个信号量在什么情况下会发生变更都搞清楚的话，就不太可能会发生这种逻辑上的错误。
• 设计与实现分离。在设计规格的时候和代码编写的时候会侧重不同的角度去思考问题，各有优劣。在设计的时候更考虑数据的输入和产出，但是在写代码的时候可能更考虑的是每一步的正确性。
• 自动化生成程序及测试。形式化的软件规格说明能使用特定的软件，自动生成程序和测试集，可以大大方便写程序这个过程。