一、JML语言理论基础及应用工具链
理论基础
官网定义：
Java建模语言（JML）是一种行为接口规范语言，可用于指定Java模块的行为 。它结合了Eiffel的契约方法设计 和Larch系列接口规范语言的基于模型的规范方法 ，以及细化演算一些元素 。
用法：
（1）开展规格化设计。这样交给代码实现人员的将不是可能带有内在模糊性的自然语言描述，而是逻辑严格的规格。
（2）针对已有的代码实现，书写其对应的规格，从而提高代码的可维护性。
具体的语法在JML手册中都有，就不在这里阐述了。
应用工具链
OpenJML：
可以根据配置的solver文件检查JML描述语言的语法正确性、程序代码的实现是否满足JML语言所描述的设计的规格。
JMLUnitNG：
可以基于JML生成测试文件。
二、部署JMLUnitNG，自动生成测试用例
下载JMLUnitNG的jar包并安装后，我针对简单的Text样例自动生成测试样例。
代码如下：
public class MyText2 {
/*@ public normal_behaviour
@ ensures \result == a + b;
*/
public static int add(int a, int b) {
return a + b;
}
/*@ public normal_behaviour
@ ensures \result == a - b;
*/
public static int min(int a, int b) {
return a - b;
}
/*@ public normal_behaviour
@ ensures \result == a * b;
*/
public static int mult(int a, int b) {
return a * b;
}
/*@ public normal_behaviour
@ ensures \result == a / b;
*/
public static int div(int a, int b) {
return a / b;
}
public static void main(String[] args) {
add(99965, 35687);
min(6698, 535489);
mult(2265, 985);
div(55478, 2);
}
}
生成的测试数据如下：
MyText2
针对MyText2的测试数据中出现了除0的Failed和运算结果超出int范围的Failed,和预想一致，生成的样例比较全面，同时可以看到生成的数据大多针对int大小的边界值和0值。可见JMLUnitNG自动生成测试样例的思路大概是边界爆破。
三、架构设计
第一次作业
结构比较简单，实现了官方要求的两个类：MyPath和MyPathContainer。
MyPath中利用一个HashSet来管理结点（不重复），利用一个ArrayList来管理结点序列。
MyPathContainer中有三个HashMap结构，分别用来管理路径->ID、ID->路径、结点->个数的映射关系，在添加路径和删除路径的时候就分别对这三个Map进行处理，获取信息也可以直接从这三个Map中获取。也即map1，map2用来双向存储路径和其ID，方便两种不同的remove。map3用来存储结点和他在图中出现的次数，添加结点时进行判断 ，如果是新的（map3不含结点key）,就把（node,1）加入，如果是旧的，就将次数（value）加一重新加入map3。
第二次作业
在第一次作业的基础上添加了距离矩阵和映射关系数组：
discourt是距离矩阵，直接存储各个结点之间的距离，不连通的点之间为apart(9999)。
每加入一条新路径，先将该路径中所有相邻的点之间的距离置为1，然后floyd算法更新距离矩阵。
每删除一条路径，首先将该路径中所有相邻的点之间的边删除一次，然后通过edgenum矩阵进行判断是不是删为0了，一旦删为0，就重新初始化所有的矩阵，把所有之前添加过的路径拿出来重新添加，如果没删为0就不用管。
至于如何将取值范围为int的结点映射到一定范围之内，我采用的是ying[]数组和valid[]数组，valid[]数组表示当前ying[]数组中的映射关系是不是有效，ying[]数组中存储的就是映射关系，例如ying[1]=6666表示当前我所有矩阵的第二个点都代表的是6666这个node，getIndex是返回某个结点在当前映射下对应的位置，例如在之前那个例子中就有getIndex（6666）=1，getFree是返回当前第一个没有映射关系的位置（valid[]为0）。因为根据指导书，任何时候不同的结点个数都不超过250，所以我的ying[]数组和valid[]数组的大小都为nodemax=251。
第三次作业
一开始利用暴力拆点的方法，构造了一个2000*2000的矩阵，发现超时是不可避免的，正在纠结之际，看到了讨论区的精品帖子，它利用一些数学上的和逻辑上的技巧，得到了了一个极为简单的处理方法：首先，对于不考虑换乘的情况，显然可以直接用floyd或者Dijkstra算法来处理，所以关键就在于怎么处理换乘，答案是对于每一条边，都先加上换乘所需的花费，这样大家都多加了一部分，所以floyd处理完之后得到的最小值仍然是不加额外花费情况下的最小值，最后再减掉这个额外增加的花费即可，距离、车费、不满意度均可如法炮制同样处理。
四、Bug分析
本系列作业没有在公测或互测中出现bug，故在这里分析一下自己在完成作业的过程中发现并修改掉的一些bug。
1.对于containsEdge()函数，1和1之间有没有边要分情况讨论。如果有类似“1 1 2 3”这样的路径则containsEdge(1,1)为true；而如果只有“1 2 3”这样的路径则containsEdge(1,1)为false。
2.对于removePath系列函数，如果发现某removePath行为导致本存在的一条边不存在了该如何处理呢？一开始我只是将这条边对应的邻接矩阵位置置为apart，然后进行floyd更新，但这样是错误的，因为floyd算法永远只会使距离减小，不会使距离增加，更不可能按照你要求的方式增加。所以我最后采取的是将数据矩阵重新初始化，遍历容器中剩下的路径重新进行计算的方法，因为容器中路径数量不会很多，所以效率还算可以。
五、心得体会
1.计算机学院开设的课程前后是有着非常紧密的联系的，或者说其实整个计算机领域，不同的分支其实都有着非常强的联系。
·本单元学习的JML规格，很大程度上是用大一离散数学学习的逻辑来进行说明的。
·图的结构，优化，最短路径的求解等一系列问题是大一数据结构学习过的。
2.关于JML规格。
JML的出现，是为了方便地对Java程序进行规格化设计。主要用途有二：一种是由用户完成并交给程序员，从而是程序员明确自己的需求，同时不同于自然语言的描述，JML还没有二义性，实在是妙不可言。第二种是由程序员针对已完成的代码进行书写，目的是为了提高程序的可维护性，其实也就是以一种最规范的形式对于程序作注释。 在本单元完成作业的过程中，我自然对于JML的第一种用途有了比较深刻的体会，在课上实验中也体会到了它的第二种用途。