第三次博客作业
(一)梳理JML语言的理论基础、应用工具链情况
JML(Java Modeling Language)是用于对Java程序进行规格化设计的一种表示语言，主要用于开展规格化设计和针对已有的代码实现，书写其对应的规格，从而提高代码的可维护性。
- JML语言的理论基础
（1）前置条件：requires子句定义该方法的前置条件，对参数进行限制。
（2）副作用范围限定：assignable列出这个方法能够修改的类成员属性。
（3）后置条件：ensures子句定义了后置条件，对方法的执行结果进行限制。
（4）其他重要语法：
\result表达式：表示一个非 void 类型的方法执行所获得的结果，即方法执行后的返回值。
\old( expr )表达式：用来表示一个表达式 expr 在相应方法执行前的取值。
\forall表达式：全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。
\exists表达式：存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束。
\max表达式：返回给定范围内的表达式的最大值。
\min表达式：返回给定范围内的表达式的最小值。
- 应用工具链情况
a. 使用 OpenJML对含有JML标记的代码进行不同检查：
（1）-check 选项可以对java文件进行JML规范检查，检查是否有语法错误，比如： openjml -check Demo.java
（2）-rac 选项可以对代码进行运行时的检查，比如：openjml -rac Demo.java
（3）-esc 选项能对程序代码进行静态检查，看是否有潜藏的问题
b.使用 JMLUnitNG根据JML语言自动生成TestNG测试，或是JMLUnit检查程序代码的正确性。
我个人感觉，它的好处是可以帮助你保证程序的正确性，但是JMLUnitNG和JMLUnit也有局限性，具体讨论见下板块。
(二)部署JMLUnitNG/JMLUnit，针对Graph接口的实现自动生成测试用例， 并结合规格对生成的测试用例和数据进行简要分析
我按讨论区说的方法，安装好了openjml和JMLUnitNG，其中遇到的不少阻力就不赘述了，这是我用demo.java的例子：
先编译，共分为两步：
- 用 javac 编译 JMLUnitNG 的生成文件
- 用 jmlc 编译自己的文件，生成带有运行时检查的 class 文件
javac -cp ../../../../openjml/jmlunitng.jar *.java
java -jar ../../../../openjml/openjml.jar -rac Demo.java
java -cp jmlunitng.jar Demo_JML_Test
之后生成了测试样例，如图：
public class Demo { /*@ public normal_behaviour @ ensures \result == lhs - rhs; */ public static int compare(int lhs, int rhs) { return lhs + rhs; } public static void main(String[] args) { compare(115514,1919810); }} [TestNG] Running:
Command line suitePassed: racEnabled()
Passed: constructor Demo() Failed: static compare(-2147483648, -2147483648) Failed: static compare(0, -2147483648) Failed: static compare(2147483647, -2147483648) Passed: static compare(-2147483648, 0) Passed: static compare(0, 0) Passed: static compare(2147483647, 0) Failed: static compare(-2147483648, 2147483647) Failed: static compare(0, 2147483647) Failed: static compare(2147483647, 2147483647) Failed: static main(null) Failed: static main({})===============================================
Command line suiteTotal tests run: 13, Failures: 8, Skips: 0
这个方法错误性很明显，而且看的出来，它的边界检查很有效啊，而修改后，程序通过了测试：
/*@ public normal_behaviour @ ensures \result == lhs - rhs;*/public static long compare(int lhs, int rhs) { long a = lhs; a = a - rhs; return a;} $ java -cp jmlunitng.jar Demo_JML_Test
[TestNG] Running: Command line suitePassed: racEnabled()
Passed: constructor Demo() Passed: static compare(-2147483648, -2147483648) Passed: static compare(0, -2147483648) Passed: static compare(2147483647, -2147483648) Passed: static compare(-2147483648, 0) Passed: static compare(0, 0) Passed: static compare(2147483647, 0) Passed: static compare(-2147483648, 2147483647) Passed: static compare(0, 2147483647) Passed: static compare(2147483647, 2147483647) 2147483648 Passed: static main(null) 2147483648 Passed: static main({})===============================================
Command line suiteTotal tests run: 13, Failures: 0, Skips: 0
由于我们的作业比较复杂，其中重要的方法并不适合自动生成测试样例，所以可见JMLUnitNG还是有所局限，对于较为复杂的程序，有些hold不住了，那我们再来看看 JMLUnit：
以下是我对graph接口的相关方法进行简单的测试：
ublic class MyGraphTest { private static MyPath p1 = new MyPath(1, -1, 2, 2, 3); private static MyPath p2 = new MyPath(1, 2, 5, 2, 5, 6); private static MyPath p3 = new MyPath(3, 4, 5, 6, 7, 8); @Test public void containsEdge() { MyGraph myGraph = new MyGraph(); try { myGraph.addPath(p1); } catch (Exception e) { e.printStackTrace(); } assertFalse(myGraph.containsEdge(1, 2)); assertTrue(myGraph.containsEdge(2, 2)); } @Test public void isConnected() { MyGraph myGraph = new MyGraph(); try { myGraph.addPath(p1); myGraph.addPath(p2); } catch (Exception e) { e.printStackTrace(); } try { assertTrue(myGraph.isConnected(-1, 6)); } catch (Exception e) { e.printStackTrace(); } } @Test public void getShortestPathLength() { MyGraph myGraph = new MyGraph(); try { myGraph.addPath(p1); myGraph.addPath(p2); myGraph.addPath(p3); } catch (Exception e) { e.printStackTrace(); } try { assertEquals(0, myGraph.getShortestPathLength(2, 2)); assertEquals(5, myGraph.getShortestPathLength(1, 8)); assertEquals(3, myGraph.getShortestPathLength(3, 6)); assertEquals(4, myGraph.getShortestPathLength(7, -1)); assertEquals(1, myGraph.getShortestPathLength(2, 3)); } catch (Exception e) { e.printStackTrace(); } try { myGraph.removePath(p1); } catch (Exception e) { e.printStackTrace(); } try { assertEquals(3, myGraph.getShortestPathLength(2, 3)); } catch (Exception e) { e.printStackTrace(); } }} 测试结果如图，自己简单的测试是没有问题的：
但是如果，仅仅是简单的测试，可能会有没有考虑到的情况，比如如果没有我在测最短路径时，对remove后的情况进行测试，可能又有隐藏的bug。
因此，对于比较复杂的程序，如果使用 Junit 进行测试，则需要充分考虑各种可能情况，来构造测试样例，比如if导致的不同结果分支等。
(三)按照作业梳理自己的架构设计，并特别分析迭代中对架构的重构
这个单元的作业让我们了解了JML语言，并学会了熟练使用相关设计思路和工具。而在使用过程中，所以设计策略，首先应该保证程序的正确性，其次再去保证性能的优化。首先，从需求来分析，给你请求，要求实现乘客的准确到达，这就需要电梯的正确调度和运行。
而第一次作业，我在结构设计上采用的是多容器来解决时间性能问题，即：
public class MyPath implements Path { private ArrayList nodesList; private HashMap nodeMap; //map与list存的东西一样，但是map便于查找 } public class MyPathContainer implements PathContainer { private HashMap pathMap; private HashMap pidMap; private int count; private HashMap countMap; //左边key 右边为出现次数} 第二次作业，path类，无需改变，而MyPathContainer，由于加带了图结构，所以，我在第一次作业的基础上进行了改进，将图结构存起来，而图的数据结构，我选择的是hashmap嵌套hashmap，而由于图没有权值，所以直接使用bfs来解决最短路径问题，具体如下：
public class MyGraph implements Graph { private HashMap pathMap; private HashMap pidMap; private int count; private HashMap countMap; //标记不同的点的次数 private HashMap > graph; //邻接矩阵 private HashMap > disTable; //距离矩阵 private boolean ifcalcu; //全局变量} public void bfs(int from) { Queue que = new LinkedList<>(); HashMap map = new HashMap<>(); map.put(from, 0); que.offer(from); while (!que.isEmpty()) { int top = que.poll(); int distance = map.get(top); for (int key : graph.get(top).keySet()) { if (!map.containsKey(key)) { //if !visited map.put(key, distance + 1); que.offer(key); } } } disTable.put(from, map);} 第三次作业，保留了不少上一次作业的设计思路，正如，数据结构，hashmap嵌套hashmap，仍然与第二次相同。但由于图结构有不同权值，而且存在换乘，这导致上一次的bfs肯定要放弃了，改用dij来计算最短路径，但是我的算法仍然有些冗杂。因为我的设计是，每次加入的path，都构造成完全图，每次换一条边，相当于增加一次换乘。
public class MyRailwaySystem implements RailwaySystem { private HashMap pathMap; private HashMap pidMap; private int count; private int blockCount = 0; private HashMap > graph; //邻接矩阵 private HashMap > disTable; //距离矩阵 private HashMap > valueMap; //以下各种权值矩阵 private HashMap > unpleavalMap; private HashMap > changeMap; private HashMap > priceMap; private HashMap > unpleaMap; private GraphHelper helper; //新的类 private boolean valCalcu; private boolean chanCalcu; private boolean priCalcu; private boolean unpleaCalcu; private boolean disCalcu; private boolean bloCalcu; //这些也是全局变量，决定是否更新某个图} 可见，总体设计变得比较复杂了，每次add，remove要更新图结构，所以虽然增加了另一个类为graphHelper，不同于第二次的暴力融合在一个类里，但是方法仍然比较冗杂，这容易导致错误的产生。而具体的错误分析，则请移步下一板块啦。
(四)按照作业分析代码实现的bug和修复情况
前两次作业，从设计思路上来说，没有任何问题，强测和互测都是满分，原因是自己先用 JUnit 测试了程序的一定正确性，并用随机数据生成器，与他人进行对拍，充分的进行了测试，保证了正确性。而且前两次优化了容器的使用，使得设计本身不会导致超时等问题。
但是，最后一次作业却因为一行代码翻车，如下：
public void removeEdge(int from, int to) { if (!graph.containsKey(from)) { return; } HashMap edges = graph.get(from); int num = edges.get(to); if (num == 1) { edges.remove(to); disCalcu = true; bloCalcu = true; } else { edges.put(to, num - 1); } if (edges!=null) { //应该改为edges.size()!=0 graph.put(from, edges); } else { graph.remove(from); }} 这一错误是当一个hashmap的key全部remove了时，它并不是null的，而是应该用size为0来判断。
而这个错误导致我的强测和互测基本奔溃，为什么会出现bug呢？原因是第三次我的设计思路比较迟缓，留给自己测试时间太短了，没有进行充分的测试，这个方法第二次作业也有，但是在其他方法使用时，对容器进行了一定改变，我没有充分测试另一个方法的各种情况，导致没有发现调用时的问题。
另外，测试手段真的很关键，随机数据生成器也不能依赖，应该仔细分析程序的各种可能结果，自己精心构造好测试样例，而构造好测试样例，不仅是在动手前，也是在动手后的仔细检查中。
(五)阐述对规格撰写和理解上的心得体会
规格的撰写，是有利于设计者、开发者，有利于团队合作的，代码规格能够帮助我们对代码的逻辑思路、代码风格进行规范和引导，在浏览规格时，能给开发者予以启迪，也能给合作者快速理解代码的可能。我想，在大型的工程或团队里，共同维护良好的规格设计和代码风格等工作，也是比不课少的。
而我自己在使用中也体会到了JML语言的好处，JML帮助我理清楚设计思路，帮我检查程序正确性，openJML，Junit，JunitNG等工具的使用也让我看到了写规格化设计的优势，之后，我会多使用这些工具，增加对JML及其工具链的熟练使用。