面向对象设计与构造第三单元作业总结

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

JML的语言基础主要包括JML表达式、方法规格以及类规格

1、JML表达式

（1）原子表达式

　　 esult

　　old()

　　 ot_assigned()

　　 ot_modified()

　　 onnullelements()

　　 ype()

　　 ypeof()

（2）量化表达式

　　forall

　　exists

　　sum

　　product

　　max

　　min

　　 um_of

（3）操作符

　　子类型关系操作符  <:

　　等价关系操作符  <==>

　　推理操作符  ==>

　　变量应用  othing  everything

2、方法规格

（1）前置条件  reqquires

（2）后置条件  ensures

（3）副作用范围限定  assignable  modifiable

（4）signals子句

3、类规格

（1）状态变化约束  constraint

（2）不变式  invariant

4、应用工具链

我使用的是OpenJml工具，以最简单的加法为例

样例程序

public class Add {
     //@ requires a > 0;
     //@ requires b > 0;
     //@ ensures 
esult == a+b;
     public static int add(int a, int b){
         return a+b;
     }

    public static void main(String args[]){
         System.out.println(add(2,3));
     }
 }

（1）首先可以使用-check对规格的格式进行审查

比如我将规格改为

public class Add {
     //@ 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.out.println(add(2,3));
     }
 }

即将result前面的改为/，执行java -jar openjml.jar -check Add.java命令进行检查，会得到如下结果

图一  规格的格式检查

（2）第二可以使用 -esc 进行静态检查

对初始代码执行java -jar openjml.jar -esc Add.java命令结果如下

图二  静态检查结果

可以看到静态检查发现有加法溢出的问题，

更具体地使用java -jar openjml.jar -esc -subexpressions Add.java命令这可以查看详细结果如下

图三  静态检查详细结果

可以看到若a=2147483647,b=1的时候会出现算术溢出的异常

如果将代码修改如下就不会出现警告。

public class Add {
     //@ requires a > 0;
     //@ requires b > 0;
     //@ ensures 
esult == a+b;
     public static long add(int a, int b){
         return (long)a+(long)b;
     }

    public static void main(String args[]){
         System.out.println(add(2,3));
     }
 }

 （3）还可以通过-rac在运行时进行检查

现将样例代码修改如下

public class Add {
     //@ requires a > 0;
     //@ requires b > 0;
     //@ ensures 
esult == 3;
     public static int add(int a, int b){
         return a+b;
     }

    public static void main(String args[]){
         System.out.println(add(2,3));
     }
 }

可以看到我将后置条件进行修改，此时执行java -jar openjml.jar -rac Add.java和java -classpath ".;jmlruntime.jar" Add两条命令结果如下

图四  动态运行结果

可以看到动态检查发现运行结果与规格不相符

二、部署JMLUnitNG/JMLUnit，针对Graph接口的实现自动生成测试用例（简单方法即可，如果依然存在困难的话尽力而为即可，具体见更新通告帖）， 并结合规格对生成的测试用例和数据进行简要分析

由于Graph类编译过于复杂，所以这里使用一个比较简单测试样例，即两个数相比较，这也是很多人在Path中写错的一个地方，待测试程序如下

public class Compare {

     //@ ensures a > b ==> 
esult > 0;
     //@ ensures a < b ==> 
esult < 0;
     //@ ensures a == b ==> 
esult == 0;
     public static int compare(int a, int b){
         return a-b;
     }

    public static void main(String args[]){
         System.out.println(compare(2,3));
     }
 }

这是很多同学的错误写法，这样会导致算数溢出，这里使用JMLUnitNG自动生成测试用例执行以下命令

java -jar jmlunitng.jar calculateCompare.java

javac -cp jmlunitng.jar calculate*.java

java -jar openjml.jar -rac calculateCompare.java

java -cp jmlunitng.jar calculate.Compare_JML_Test

运行结果如下

图五  自动生成测试用例1

可以发现在边界值的测试中出现了问题，现将代码进行如下修改

public class Compare {

     //@ ensures a > b ==> 
esult > 0;
     //@ ensures a < b ==> 
esult < 0;
     //@ ensures a == b ==> 
esult == 0;
     public static int compare(int a, int b){
         if (a > b) {
             return 1;
         } else if (a < b) {
             return -1;
         } else {
             return 0;
         }
     }

    public static void main(String args[]){
         System.out.println(compare(2,3));
     }
 }

仍旧运行上述命令得到结果如下

图六  自动生成测试用例2

可以看到这样就可以成功通过边界测试。

三、按照作业梳理自己的架构设计，并特别分析迭代中对架构的重构

先用类图的方式分析三次作业中的代码架构设计

图七  第一次作业类图

本次作业十分简单，内容也是十分的清晰。构建了两个类一个是Path用来储存节点序列，另一个是一个用来储存Path的容器，对于每一个容器实现了对于Path的增删改查等一系列方法。为了能够降低时间复杂度，我在Pathcontainer中使用了Hashmap储存结构，使用hash查找的方式来减少查询时间。在统计不同节点的时候我也使用的是Hashmap结构，将每一个节点作为键值，当节点个数为零的时候将其从Hashmap中删去，键值对的个数即为不同节点的个数。

图八  第二次作业类图

相比第一次作业本次作业加入了对于图结构的一些判断，除了继承上一次Pathcontainer中的方法，还新增加了判断两个节点之间是否有边是否连接以及最短路径。由于此次节点的个数不超过200，所以我选择了指数稍大但常数很小的Floyd算法。每次图的结构改变的时候就要重新计算一下Floyd的距离矩阵，根据两个点指定位置的元素是否是“无穷”来判断是否连通，根据是否为1来判断是否有边。而本次作业仍然使用了两个类来实现，基本架构没有改变。

 

图九  第三次作业类图

本次作业在图的基础上加入了线路的概念，即在进行换乘的时候要考虑到损耗。本次的RailwaySystem继承了上一次的Graph类的同时，加入了最小换乘次数、最小票价、最小满意度。本次我使用的基础算法仍旧是Floyd算法，还加入了三角优化。在计算最小票价的时候首先计算一条Path之中任意两个点之间的最小值，之后将每一个Path两个点的值汇总到一个矩阵之中，若两个点在不同路径之间都是连通的则取最小值。之后将矩阵的每一个点都加上换乘的损耗，之后进行Floyd最短路径计算，之后将每个计算结果减去损耗。在架构上由于本次实现的功能比较复杂，所以我在一些功能上进行了单独的封装，比如将节点的值转化成矩阵的实际的索引的translate类。以及由于本次无论是路径内部还是对于汇总矩阵都要反复进行floyd计算，所以本次将floyd的计算单独封装成Goodfloyd类

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

1、第一次作业

第一次作业由于功能十分简单，所有没有发现正确性的问题，但最开始我使用的是Arraylist数据结构进行存储，这就导致了查询的时间复杂度非常高，在进行极限测试的时候会出现CPU时间超时的现象。之后改用了Hashmap进行存储，时间复杂度大幅度下降。

除此之外第一次作业还出现了一些我没有注意到但别人出现的BUG

（1）在compare路径的时候出现了整数越界的现象，由于本次的compare要求大于返回大于零的数，小于返回小于零的数等于返回零，所以有的人直接将两个数相减，但可能没有注意到整数越界的现象，当然这种现象如果使用JML_Unit单元测试的话可以很容易检查出来。

（2）将Arraylist的hashcode作为Pathd唯一标志，我们的Arraylist的hashcode的计算方式与String现象，只能说尽可能减少冲突，但并不能完全消除冲突，所以不能使用hashcode作为Path的识别符。

2、第二次作业

第二次作业中我在自己课下测试以及互测中发现的主要问题就是在相同节点的连通、最短路径和是否存在边的计算。首先对于前两者我们的JML规格明确说明了但fromid==toid的时候Isconnected = true,Shortestpath = 0，而对于是否存在边则不一定，所以我们在对前两个进行计算的时候可以对相等条件进行特判，是否存在边则利用floyd矩阵进行判断。这也是在互测中发现其他同学出现的BUG。

3、第三次作业

第三次作业要实现对于换乘的损耗。

（1）首先这就有了一个正确性的问题，我最开始使用的简单的迪杰特斯拉算法就存在很大的问题，因为使用迪杰特斯拉算法求最短路径的时候若有多条路径最短无法确定走的是哪一条。举一个例子，若有两条路径A-B-D, A-C-D-E我想求得A到E的最短票价，这就出现了一个问题，我之前确定的A-D的路径无论是走A-C-D还是A-B-D都是一样的，但到了E之后就有了区别，如果我走的是A-B-D-E那样的话就需要一次换乘，而走A-C-D-E就不需要换乘，相应的票价也会比较低。所以最开始的这个算法无法满足基本的正确性的问题。

（2）其次还有一个时间复杂度的问题，我使用的第二个方法就是将每一条边看做一个点，要注意的是顶点相同但是在不同路径中的边也看成是不一样的，这样的结果就是可以满足正确性问题，但是我们这次要求每条Path最多80个顶点，最多50个Path，平均算下来有近4000条边，如此大的n，即使是平方数量级也是承受不住的，在我自己的极限合法测试的时候基本运行时间接近30秒，肯定是要超时的了。

总的来说这次作业考察的十分综合，首先要能够看懂复杂的JML规格说明，此外还要对数据结构的知识有着比较深入的理解才可以实现既可以保证正确性又可以控制时间复杂度。

 五、阐述对规格撰写和理解上的心得体会

　　首先谈一下我对于JML规格语言的理解，其实描述一个类或者方法的功能并不会局限于某种形式，如果有能力说清楚用自然语言也未尝不可，比如jdk就是用的自然语言进行的描述，但是就我个人认为相比自然语言来说JML这种规格化语言可以大大减少歧义的出现，表述更加精准。举个例子，如果一个方法使用自然语言表述是传进一个int数组，返回最小值的索引，这就会出现一些问题，首先如果传进的数组引用是null怎么办，如果传进的数组为空怎么办，若果数组中最小值不止一个返回谁的索引？等等一系列问题。但是如果使用规格化语言的话就可以明确规定好前置条件，正常行为和异常行为以及后置条件等一系列方法需要满足的条件，来进一步规范方法的功能。

　　在撰写规格上，我们主要是在课上进行过相关训练。写规格的首先要考虑的就是要明确正常和异常行为的判断，也就是该方法需要满足的前置条件，最重要的是要规范的表述方法的功能，还有一个比较重要的一点就是在规格语言中可以使用类中的一些标记为pure的方法，但是一些会对类的成员变量进行修改的方法，换句话说副作用范围限定不是 othing的方法则不可以在规格中出现，此外还要注意old()的正确使用。