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

　　JML（Java Modeling Language）—— java建模语言，是一种行为接口规范语言( behavioral interface specification language, BISL)。同时，JML也是一种进行详细设计的符号语言，它鼓励你用一种全新的方式来看待Java的类和方法，既规定了方法或抽象数据类型的接口，也规定了它们的行为。

　　面向对象的分析和设计（OOAD）的一个重要原则就是过程性的思考应该尽可能地推迟，先以一定的规范建立框架，这类的规范通常被称作面向模型。

注释结构

 //@ annotation   行注释 

 /*@ annotation*/ 块注释

原子表达式

\result 　　　　　　　　　　　　表示返回值

\old（x） 　　　　　　　　 　　表示x在该方法运行前的取值

\not_assigned(x,y,...) 　　  表示括号内对象不被赋值

\not_modified(x,y,...) 　　　表示括号内对象不被修改

nonnullelements(container)  表示container的存储对象没有null

type(x) 　　　　　　　　　　　　表示x的类型

typeof（x） 　　　　　　　　　　表示x的准确类型

量化表达式

\forall 全称量词

\exists 存在量词

\sum    一组对象的和

操作符

 expr1<==>expr2 　　等价关系操作符

 expr1==>expr2 　　 推理操作符

 \nothing　　　　　　空操作符

\everything 　　　　全部对象操作符

方法规格

requires X 　 pre-condition

ensures X 　　post-condition

assignable　　赋值

pure  　　　　 关键字

singals   　　子句

 

　　下图是JML官网上的应用工具链详情，具体包括JML-launcher、jmlc-gui、jmle、Jtest、JML-Junit等相关工具 。

　　一般而言，JML有两种主要的用法：

　　1)  开展规格化设计。

　　2)  书写已有的代码实现的规格，从而提高代码的可维护性。

 

• 2、部署SMT Solver

　　 由于本地安装出现了很多问题（主要集中在多版本JDK共存上），所以我一开始采用openJML官网的线上测试，来体验SMT Solver的功能。

　　　　测试代码：

public class MaybeAdd {    // requires a > 0;    //@ requires b > 0    //@ ensures \result = a+b;    public static int add(int a, int b){        return a-b;    }    public static void main(String args[]){        System.ou.println(add(2,3));    }}

　　　　测试结果：

/tmp/tmp9iwx_W/MaybeAdd.java:3: error: The expression is invalid or not terminated by a semicolon    //@ requires b > 0                      ^/tmp/tmp9iwx_W/MaybeAdd.java:4: error: unexpected type    //@ ensures \result = a+b;                ^  required: variable  found:    value/tmp/tmp9iwx_W/MaybeAdd.java:4: error: Assignments are not allowed where pure expressions are expected    //@ ensures \result = a+b;                        ^/tmp/tmp9iwx_W/MaybeAdd.java:10: error: cannot find symbol        System.ou.println(add(2,3));              ^  symbol:   variable ou  location: class System4 errors　

　　后来我在同学的电脑（openJML配置成功，部署SMT Solver）上进行了openJML的测试（在这里感谢zjh大佬的帮助），结果如下：

　　1） 测试程序：

1 public class TestPath{ 2     //@ public instance model non_null int[] nodes; 3     private int [] nodes; 4  5     public TestPath(int... nodeList) { 6         nodes = nodeList; 7     } 8  9     //@ ensures \result == nodes.length;10     public /*@pure@*/int size() {11         return nodes.length;12     }13 14     /*@ requires index >= 0 && index < size();15       @ assignable \nothing;16       @ ensures \result == nodes[index];17       @*/18     public /*@pure@*/int getNode(int index) {19         return nodes[index];20     }21 22     public static void main(String[] args) {23         MyPath demo=new MyPath(1,5,10);24         System.out.println(demo.size());25         System.out.println(demo.getNode(2));26         System.out.println(demo.getNode(0));27     }28 }

　　　　测试结果：

　　　这是由于规格中要求node为public，而在实现过程中node为private，并且openJML找不到private的对象，所以报错如上图所示。

　　2） 测试程序：

1 public class TestPath{ 2     //@ public instance model non_null int[] nodes; 3     public int [] nodes; 4  5     public TestPath(int... nodeList) { 6         nodes = nodeList; 7     } 8  9     //@ ensures \result == nodes.length;10     public /*@pure@*/int size() {11         return nodes.length;12     }13 14     /*@ requires index >= 0 && index < size();15       @ assignable \nothing;16       @ ensures \result == nodes[index];17       @*/18     public /*@pure@*/int getNode(int index) {19         return nodes[index];20     }21 22     public static void main(String[] args) {23         MyPath demo=new MyPath(1,5,10);24         System.out.println(demo.size());25         System.out.println(demo.getNode(2));26         System.out.println(demo.getNode(0));27     }28 }

　　　　测试结果：

　　这是由于在程序中使用node，没有使用this.node，前者对于IDEA来说可以接受，等价于后者，但是在openJML中，由于严格规格的要求，两者不等价，导致默认前者为一个方法内的局部对象，所以找不到，报错如上图所示。

　　3） 测试程序：

1 public class TestPath{ 2     //@ public instance model int[] nodes; 3     public int [] node; 4  5     public TestPath(int... nodeList) { 6         this.node = nodeList; 7     } 8  9     //@ ensures \result == nodes.length;10     public /*@pure@*/int size() {11         return this.node.length;12     }13 14     /*@ requires index >= 0 && index < size();15       @ assignable \nothing;16       @ ensures \result == nodes[index];17       @*/18     public /*@pure@*/int getNode(int index) {19         return this.node[index];20     }21 22     public static void main(String[] args) {23         TestPath demo = new TestPath(1,5,10);24         System.out.println(demo.size());25         System.out.println(demo.getNode(2));26         System.out.println(demo.getNode(0));27     }28 }

　　　　测试结果：

　　　　这是由于创建node的时候没有实现 non_null 的要求，并且没有在规格或方法中写明，当node为空时的操作。

 

• 3、部署JMLUnitNG/JMLUnit

　　使用JunitNG可以实现简单的程序测试和验证，下载好对应的jar包后，运行相关指令即可完成测试。

（参考资料： ）

　　测试函数如下：

1 package test; 2  3 public class Test { 4     /*@ ensures \result == (a + b); 5       @ */ 6     public static int add(int a, int b) { 7         return a + b; 8        } 9 10     public static void main(String[] args) {11         add(1, 999);12     }13 }

　　运行结果如下图所示：

1 [TestNG] Running: 2   Command line suite 3   4 Failed: racEnabled() 5 Passed: constructor Test() 6 Passed: static add(-2147483648, -2147483648) 7 Passed: static add(0, -2147483648) 8 Passed: static add(2147483648, -2147483648) 9 Passed: static add(-2147483648, 0)10 Passed: static add(0, 0)11 Passed: static add(2147483648, 0)12 Passed: static add(-2147483648, 2147483648)13 Passed: static add(0, 2147483648)14 Passed: static add(2147483648, 2147483648)15 Passed: static main(null)16 Passed: static main({})17 18 ===============================================19 Command line suite20 Total tests run: 13, Failures: 1, Skips: 0

　　可以发现，自动生成的样例主要是在各种边界情况，比如int的范围（最大值、最小值、正负数、零），传参的类型（int、object、NULL）。对程序的鲁棒性进行了较好的测试。

 

• 4、梳理架构设计

作业一、MyPathContainer规格设计

1. 统计信息图

2. 复杂度分析

基本复杂度（Essential Complexity (ev(G))、模块设计复杂度（Module Design Complexity (iv(G))）、Cyclomatic Complexity (v(G))圈复杂度

 

OCavg为平均循环复杂度;WMC为总循环复杂度

 

3. 结构信息图

可见，由于逻辑简单，本次作业的复杂度和耦合度都不高。 

4. 分析架构设计

　　为了减少时间复杂度，采用的是三个hashmap的策略（起先我用的是单hashmap，但是由于hashmap的getValue方法的时间复杂度是O（n），所以对于一些极端数据存在超时的风险），效果明显，时间收益很好。也为以后减少时间开销打下了基础。

 

作业二、MyGraph规格设计

1. 统计信息图

2. 复杂度分析

基本复杂度（Essential Complexity (ev(G))、模块设计复杂度（Module Design Complexity (iv(G))）、Cyclomatic Complexity (v(G))圈复杂度

 

OCavg为平均循环复杂度;WMC为总循环复杂度

 

3. 结构信息图

 

可见，由于逻辑简单，只比上次作业多了迪杰斯特拉算法，所以本次作业的复杂度和耦合度都不高。 

4. 分析架构设计

　　在上一次作业的基础上，采用使用优先队列的迪杰斯特拉算法实现最小路径，并将中间结果储存，减少重复计算，以最大化减少运行时间。

　　架构设计不好，虽然没有重构，但是直接将上一次作业的内容复制粘贴，而没有采用继承等方式实现。层次性不明显，框架比较冗杂。　　

　　对下一次作业也不友好，没有对迪杰斯特拉算法建模或单独建类，复用起来较为困难。

　　完成作业时，还不是特别明白规格设计的意图，和建模建类的重要性。所以对结构方面的考虑较少，导致第三次作业有了比较大的重构，花费了很多时间，还不利于扩展和DEBUG。

 

作业三、MyRailwaySystem规格设计

1. 统计信息图

2. 复杂度分析

基本复杂度（Essential Complexity (ev(G))、模块设计复杂度（Module Design Complexity (iv(G))）、Cyclomatic Complexity (v(G))圈复杂度

 

OCavg为平均循环复杂度;WMC为总循环复杂度

 

3. 结构信息图

 

　　可见，本次作业功能增加，复杂度和耦合度上升，尤其是addPathGraph和removePathGraph两个函数。

　　因为图结构发生变化，要对多个不同功能的初始邻接表（initXXX）和一些结果邻接表（connect，edge等）进行计算，所以复杂度和耦合度较高。  

4. 分析架构设计

　　在上次作业的基础上，进行了一定的重构。

　　首先是将迪杰斯特拉和弗洛伊德等最短路径算法分离出去，单独建类，并将对于图的有关操作单独建类。

　　其次，模型采用评论区大佬的“完全图方法”，主要算法是弗洛伊德算法，保存所有中间矩阵和初始建图矩阵。

　　整体速度还不错，但是极端情况CPU时间会贴近35s的限制。

 　　

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

　1） 第一次作业中未出现BUG，互测中也未发现BUG。

　2） 第二次作业中未出现BUG，互测中发现了同学的一个BUG，当查询在图中的某一点到这一点的距离时，应该输出：

Ok, length is 0.

　　但是他输出：

Ok, length is 2.

　　这个BUG我在第二次作业没有发现，但在第三次作业自测中发现过，原因是没有进行特判两个点为相同时的距离。因为按照最短路径算法，点A与点A之间没有边的话，那么A-A之间的最短路径为A-B（某一个和A相连的点）-A，距离为2，导致出错。

　　犯这个错误的原因之一可能是没有好好看JML规格说明。

　3） 第三次作业中出现一个BUG，出错点是判断连通块个数出错。

　　我判断连通块是通过遍历paths中所有的path，如含有path_new中的点，则将两者判为连通块。

　　出错原因：当pathA和pathB连通时，pathC加入，若pathA中含有pathC中点，pathB中不含有pathC中的点，那么我会判断pathA和pathC连通，但是判断pathB和pathC不连通，与实际不符。

e.g. pathA : 1-2-3-4-5-6-7 pathB : 1-3-5-7-9-11 pathC : 2-4-6-8-10-12　

　　解决措施：在判断时，将所有与path_new连通的path的标志号记下，最后再遍历一遍paths，将所有标志号在其中的path，判断与path_new连通。

 　   反思: 这个错误的出现更深层次的原因是自己太懒，在写连通块个数的算法时，本应该建树查找，更加稳妥，但是我采用了自己的想出来的“简单”方法，贪图一时休息，却导致了BUG的发生。

 　　在互测中，我一共发现了同组同学的4类不同BUG：

　　 1.　对于输入：

PATH_ADD 2 2

CONTAINS_PATH 2 2

错误输出 NO. ，应该是 YES. 

原因：2-2进入图中变为一个点，而没有记下自环边（2-2）。

　　 2. 对于输入：

CONNECTED_BLOCK_COUNT

错误输出

Ok, connected block count is xxx.　　（xxx是全部点的个数）

应该输出

Ok, connected block count is 0.

错误原因猜测：建图时，对每个点建立一棵树，但是在查询时没有及时更新数据，导致输出的是“原始”结果。

　　 3. 对于输入：

LEAST_UNPLEASANT_VALUE 15 143

错误输出

Ok, least unpleasant value is 99968.

应该输出

Ok, least unpleasant value is 1060.

错误原因猜测：计算不满意度方法中存在一个“上限”或者计算方法通过减法等，但这组数据的不满意度超过限制范围，导致计算结果出错。

 　　4. 对于复杂输入， CPU_TIME_LIMIT_EXCEED ，原因为程序复杂度过高，没有很好的完成时间限制的要求。

 

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

　　对于规格这个东西，第一感觉是“什么？我为什么要写这奇奇怪怪没用的东西？”。但当我真正实践过后，发现我之所以怎么想，是因为有指导书的存在，其实指导书就是类似于一种规格。只是JML规格更加精准，减少语言上的二义性或者模糊性。

　　在本单元的作业中，我对于规格的理解和灵活运用方面比较欠缺，有时候会被规格束缚了手脚，比如在完成某个方法时，不会跳出规格的思路，采用一些简便的方法实现：

　　以下在实现MyPath的equals方法时，直接按照JML规格一步步写完，用原始的flag判断结束等，导致不美观，易写错。

1     public boolean equals(Object obj) { 2         if (obj instanceof Path) { 3             Path path = (Path) obj; 4             if (path.size() == size()) { 5                 int flag = 1; 6                 for (int i = 0; i < size(); i++) { 7                     if (path.getNode(i) != getNode(i)) { 8                         flag = 0; 9                         break;10                     }11                 }12                 return flag == 1;13             }14         }15         return false;16     }

　　在层次化规格上，我做的不好，本单元三次作业其实有着严格的继承关系，而我没有发现，还在简单复制粘贴方法。如果使用继承关系，可以较好的分离出不同功能的对象，较好的解耦。

　　对于JML较为复杂的第三次作业中，我没有特别理解课程组设置几个选择性实现的方法的意义，当时为了省时间，直接按照自己的理解写程序，写完之后又发现和要求不匹配，改了挺久的程序。其实应该完成那几个方法，通过完成的过程，就能理解题意，还能较少错误，其实会更省时间。（这就说明了，先想明白架构、逻辑，远比先写代码重要的多）。

　　对于建模，我只是初步的将最短路径算法和一些有关图的计算封装成独立的类，但是并没有从点、边一层一层建立起图结构，也没有对四种不同的“最短路径“建立统一接口，用工厂方法实现统一模型下的不同图结构及其计算模型。

　　要学的东西还是很多，不过最起码知道要学什么，希望自己以后能深入学习有关规格设计和统一建模的资料。共勉~