前言
第三单元，我们以JML为基础，先后完成了
这是一个递进的过程，代码实现基于课程组给出的JML语言，JML是一个只关心前提与结果的建模语言，可以描述清楚对于该方法的需求，但具体实现由个人完成，实现方法不限，只需要满足需求。一定意义上，算是工程方面客户的需求，而我们依据其完成代码。
JML理论基础及应用
注释结构
一般使用块注释，即/*@ annotation @*/，注释放在被注释成分的上方，一般类似于下方例子的构架。
/*@ public normal_behavior
@ requires 定义该方法的前置条件
@ assingable 列出该方法可能修改的成员属性
@ ensures
esult = 定义后置条件
@ also
@ exceptional_behavior
@ signals (Exception e) 抛出异常的类型以及何种情况下
@*/
同时也可以使用行注释，如下
//@ ensures
esult =
规格中的每一个句子都必须以分号结尾，否则会导致JML工具无法解析，且规格中描述的model int[] elements只是规格层次的描述，并不一定要实现该声明，变量类型也无需相同。
JML表达式
1. 原子表达式
esult：表示一个非 void 类型的方法执行所获得的结果，即方法执行后的返回值。
old( expr )：用来表示一个表达式 expr 在相应方法执行前的取值。
ot_assigned(x,y,...)：用来表示括号中的变量是否在方法执行过程中被赋值。
ot_modified(x,y,...)：该表达式限制括号中的变量在方法执行期间的取值未发生变化。
onnullelements( container )：表示 container 对象中存储的对象不会有 null。
2. 量化表达式
forall表达式：全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。
exists表达式：存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束。
sum表达式：返回给定范围内的表达式的和。
product表达式：返回给定范围内的表达式的连乘结果。
max表达式：返回给定范围内的表达式的最大值。
min表达式：返回给定范围内的表达式的最小值。
um_of表达式：返回指定变量中满足相应条件的取值个数。
3. 操作符
(1) 子类型关系操作符：E1<:E2 ，如果类型E1是类型E2的子类型(sub type)，则该表达式的结果为真，否则为假。如果E1和E2是相同的类型，该表达式的结果也为真。
(2) 等价关系操作符：b_expr1<==>b_expr2或者b_expr1<=!=>b_expr2，其中b_expr1和b_expr2都是布尔表达式，这两个表达式的意思是b_expr1==b_expr2或者b_expr1!=b_expr2。
(3) 推理操作符：b_expr1==>b_expr2或者b_expr2<==b_expr1。
(4) 变量引用操作符：除了可以直接引用Java代码或者JML规格中定义的变量外，JML还提供了几个概括性的关键词来引用相关的变量。 othing指示一个空集；everything指示一个全集，即包括当前作用域下能够访问到的所有变量。
部署JMLUnitNG/JMLUnit
测试代码
package demo;
public class Demo {
private int[] Nodes = new int[100000];
public Demo(int[] list) {
for (int i = 0; i < list.length; i++) {
Nodes[i] = list[i];
}
}
//@ public instance model non_null int[] nodes;
//@ ensures
esult == nodes.length;
public /*@pure@*/int size() {
return Nodes.length;
}
/*@ requires index >= 0 && index < size();
@ assignable
othing;
@ ensures
esult == nodes[index];
@*/
public /*@pure@*/ int getNode(int index) {
return Nodes[index];
}
/*@
@ public normal_behaviour
@ ensures
esult == a + b;
*/
public /*@pure@*/ int add(int a, int b) {
return a + b;
}
//@ ensures
esult == (nodes.length >= 2);
public /*@pure@*/ boolean isValid() {
return Nodes.length >= 2;
}
public static void main(String[] args) {
int[] list1 = {1, 2, 3, 4, 5};
int[] list2 = {5,12354, 2345342, 12312345, 425};
Demo demo1 = new Demo(list1);
Demo demo2 = new Demo(list2);
System.out.println(demo1.size());
System.out.println(demo1.size() + demo2.size());
}
}
测试结果
显然有多个地方failed，例如add方法，没有考虑溢出，导致多次被爆破，且当构造函数接收到Null时也会出错。我试图修改代码，我考虑了传入数组为null的情况，抛出了异常，同时也考虑了add溢出的可能性，但依然skip或是fail。。。就很绝望，个人感觉JML体系还不是很完善，或是OpenJml以及TestNG不够完善，还有很大上升的空间。
作业情况分析
第一次作业（Path+PathContainer）
架构设计
第一次作业较为简单，只需实现一个路径管理系统，实现通过输入指令来进行数据增减查改。在MyPath中，我是用ArrayList存储路径节点，Path中的方法都较为容易实现，而在MyPathContainer中，我使用了两个HashMap来存储<Id, Path>，<Path, Id>，使用HashSet来存所有Path中的不同节点，同时还将PathId和Path在ArrayList中也存储一次，当使用contains功能时，我选择使用ArrayList.contains方法，速度较HashMap更快，但在get方法中，我使用HashMap效率更高，当路径发生更改，入add或remove时，会对于以上存储进行维护。强侧并没有出现问题。
类图
方法复杂度
可以看出CompareTo方法，复杂度最高，因为根据要求使用字典序，我使用了较为笨拙的方法，即循环判大小，复杂度较高。
类复杂度
第二次作业（Path+Graph）
架构设计
第二次作业新增了实现无向图系统功能，Graph除了继承PathContainer中的功能以外，还多出了节点是否连通，是否包含边，以及求两点之间的最短路径。我选择使用邻接矩阵，鉴于该无向图边的权重都为1，使用二维数组来维护点之间的最短路径，同时维护了一个change变量，当执行add或remove命令时，change++，在查询之前，判断change是否大于0，若是则使用update方法，更新二维数组，这样可以减少更新数组的次数。距离矩阵初始化为INF，即无限大，同时根据指导书描述，节点不可超过250个，于是建立映射数组，将节点与0-250建立起联系，以便使用数组。矩阵的建立采用Floyd算法，一次更新将所有最短距离都算出，查询时直接返回int即可。强侧并没有出现问题。
类图
方法复杂度
可以看出延续第一次作业中的CompareTo方法较高复杂度，而getShortestPathLength方法复杂度较高，是因为要分别判断抛出三个异常，if语句使用较多，问题不大。
类复杂度
第三次作业（Path+RailwaySystem）
架构设计
第三次作业较为复杂，不再是不加权无向图，更新为计算权值型无向图，需要我们维护价格，满意度，最少换乘次数，最短距离四个权重图。首先延续第二次作业中的映射，维护了映射HashMap，每当进行增加或删除路径操作时，都重新根据不同节点数组，更新映射。由于本次作业新增要求，只在RAilwaySystem类中维护矩阵，远远不足以满足需求，于是我在每一个Path类中维护了一个该路径下的最短距离举证，但现在想来，当时应该重新写一个类，如PathHelper类，来完成这些工作，而不是自己篡改接口，接口也就失去了意义。每新建一条path时，该path内部会自信跑一边floyd，算出最短路径矩阵，同时提供返回值。在RailwaySystem中，即总图需要更新时，首先根据每一条path的最短距离矩阵配合权重计算方法，初始化总图，此时的总图的权重代表了一个path内部的最小值，以最少换成次数为例，初始化时会更新每一个path内部，相连的点之间的权重，而不仅仅时相邻点的权重，同时给权值加1，代表一次换乘，初始化完成后，用总图跑一边Floyd，此时计算出的最小矩阵的权值，是多加一次换乘的权值，因此在计算最后返回值时，需要考虑到这一点。并没有使用拆点做法，下面时更新的过程，同时，连通块采取染色算法，可以轻易算出。
private void update() {
updateMap();
init();
int num = idList.size();
for (Path path : paList) {
for (int i = 0; i < path.size(); i++) {
for (int j = 0; j <= i; j++) {
if (i != j) {
// 计算新的权值，同时加上一次换乘
} else {
int a = path.getNode(i);
a = map.get(a);
priceMap[a][a] = 0;
transMap[a][a] = 0;
pleaseMap[a][a] = 0;
}
}
}
}
floyd(priceMap, num);
floyd(transMap, num);
floyd(disMap, num);
floyd(pleaseMap, num);
int[] color = new int[num];
int count = 0;
numOfConn = 0;
while (count < num) {
int t = 0;
numOfConn++;
while (color[t] != 0) { t++; }
for (int n = 0; n < num; n++) {
if (0 <= disMap[t][n] && disMap[t][n] < INF) {
color[n] = numOfConn;
count++;
}
}
}
}
类图
方法复杂度
类复杂度
Bug修复
总体并没有遇到太多的bug，前两次作业都是满封，但第三次作业，强测通过，但在互测阶段，被找到了一个bug，同时我自己写的评测机本来用来hack别人的，结果报的都是我的错，是一个极其粗心的错误，在同一点的距离矩阵中，我直接初始化为0，后续在containsEgde中，我根据距离矩阵的值大于0，判断存在边，于是忽视了自环的情况，导致了这个极其弱智的bug。（其实我运气也比较好，强测数据点竟然没有测自环，毕竟我的评测机几乎10个点就有1个是我的bug，可能是我造的数据太弱了。
心得体会