• 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 System
4 errors
后来我在同学的电脑（openJML配置成功，部署SMT Solver）上进行了openJML的测试（在这里感谢zjh大佬的帮助），结果如下：
1） 测试程序：
public class TestPath{
//@ public instance model non_null int[] nodes;
private int [] nodes;
public TestPath(int... nodeList) {
nodes = nodeList;
}
//@ ensures \result == nodes.length;
public /*@pure@*/int size() {
return nodes.length;
}
/*@ requires index >= 0 && index < size();
@ assignable \nothing;
@ ensures \result == nodes[index];
@*/
public /*@pure@*/int getNode(int index) {
return nodes[index];
}
public static void main(String[] args) {
MyPath demo=new MyPath(1,5,10);
System.out.println(demo.size());
System.out.println(demo.getNode(2));
System.out.println(demo.getNode(0));
}
}测试结果：
这是由于规格中要求node为public，而在实现过程中node为private，并且openJML找不到private的对象，所以报错如上图所示。
2） 测试程序：
public class TestPath{
//@ public instance model non_null int[] nodes;
public int [] nodes;
public TestPath(int... nodeList) {
nodes = nodeList;
}
//@ ensures \result == nodes.length;
public /*@pure@*/int size() {
return nodes.length;
}
/*@ requires index >= 0 && index < size();
@ assignable \nothing;
@ ensures \result == nodes[index];
@*/
public /*@pure@*/int getNode(int index) {
return nodes[index];
}
public static void main(String[] args) {
MyPath demo=new MyPath(1,5,10);
System.out.println(demo.size());
System.out.println(demo.getNode(2));
System.out.println(demo.getNode(0));
}
}测试结果：
这是由于在程序中使用node，没有使用this.node，前者对于IDEA来说可以接受，等价于后者，但是在openJML中，由于严格规格的要求，两者不等价，导致默认前者为一个方法内的局部对象，所以找不到，报错如上图所示。
3） 测试程序：
public class TestPath{
//@ public instance model int[] nodes;
public int [] node;
public TestPath(int... nodeList) {
this.node = nodeList;
}
//@ ensures \result == nodes.length;
public /*@pure@*/int size() {
return this.node.length;
}
/*@ requires index >= 0 && index < size();
@ assignable \nothing;
@ ensures \result == nodes[index];
@*/
public /*@pure@*/int getNode(int index) {
return this.node[index];
}
public static void main(String[] args) {
TestPath demo = new TestPath(1,5,10);
System.out.println(demo.size());
System.out.println(demo.getNode(2));
System.out.println(demo.getNode(0));
}
}测试结果：
这是由于创建node的时候没有实现 non_null 的要求，并且没有在规格或方法中写明，当node为空时的操作。
• 3、部署JMLUnitNG/JMLUnit
使用JunitNG可以实现简单的程序测试和验证，下载好对应的jar包后，运行相关指令即可完成测试。
（参考资料：https://course.buaaoo.top/assignment/71/discussion/199 ）
测试函数如下：
package test;
public class Test {
/*@ ensures \result == (a + b);
@ */
public static int add(int a, int b) {
return a + b;
}
public static void main(String[] args) {
add(1, 999);
}
}运行结果如下图所示：
[TestNG] Running:
Command line suite Failed: racEnabled()
Passed: constructor Test()
Passed: static add(-2147483648, -2147483648)
Passed: static add(0, -2147483648)
Passed: static add(2147483648, -2147483648)
Passed: static add(-2147483648, 0)
Passed: static add(0, 0)
Passed: static add(2147483648, 0)
Passed: static add(-2147483648, 2147483648)
Passed: static add(0, 2147483648)
Passed: static add(2147483648, 2147483648)
Passed: static main(null)
Passed: static main({}) ===============================================
Command line suite
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 .
但是他输出：
Ok, length is .
这个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
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判断结束等，导致不美观，易写错。
public boolean equals(Object obj) {
if (obj instanceof Path) {
Path path = (Path) obj;
if (path.size() == size()) {
int flag = 1;
for (int i = 0; i < size(); i++) {
if (path.getNode(i) != getNode(i)) {
flag = 0;
break;
}
}
return flag == 1;
}
}
return false;
}在层次化规格上，我做的不好，本单元三次作业其实有着严格的继承关系，而我没有发现，还在简单复制粘贴方法。如果使用继承关系，可以较好的分离出不同功能的对象，较好的解耦。
对于JML较为复杂的第三次作业中，我没有特别理解课程组设置几个选择性实现的方法的意义，当时为了省时间，直接按照自己的理解写程序，写完之后又发现和要求不匹配，改了挺久的程序。其实应该完成那几个方法，通过完成的过程，就能理解题意，还能较少错误，其实会更省时间。（这就说明了，先想明白架构、逻辑，远比先写代码重要的多）。
对于建模，我只是初步的将最短路径算法和一些有关图的计算封装成独立的类，但是并没有从点、边一层一层建立起图结构，也没有对四种不同的“最短路径“建立统一接口，用工厂方法实现统一模型下的不同图结构及其计算模型。
要学的东西还是很多，不过最起码知道要学什么，希望自己以后能深入学习有关规格设计和统一建模的资料。共勉~