OO第三次博客

OO第三单元总结

JML语言的理论基础、应用工具链

JML(Java Modeling Language)是用于对Java程序进行规格化设计的一种表示语言。它把语言分为几个层次，我们主要用到了level 0层次.

JML的主要作用如下所示：

（1）开展规格化设计。这样交给代码实现人员的将不是可能带有内在模糊性的自然语言描述，而是逻辑严格的规格。

（2）针对已有的代码实现，书写其对应的规格，从而提高代码的可维护性。这在遗留代码的维护方面具有特别重要的意义。

JML 注释结构

每行以@开头 

行注释为 

//@annotation

块注释为

/* @annotation@ */

JML注释一般放在被注释成分的近邻上部。

JML表达式

主要分为原子表达式、量化表达式、集合表达式、操作符等

原子表达式主要有‘ esult’，'old(expr)'，' ot_asigned(x,y,...)'，' ypeof(expr)'等

esult      //表示一个非 void 类型的方法执行所获得的结果，即方法执行后的返回值

old(expr)     //用来表示一个表达式 expr 在相应方法执行前的取值。

量化表达式主要有‘forall’，‘exists’，‘sum’，‘product’，‘max’，‘min’等

forall    //全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。 

exists    //存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束。 

集合表达式可以在JML规格中构造一个局部的集合（容器），明确集合中可以包含的元素。集合构造表达式的一般形式为：new ST {T x|R(x)&&P(x)}，其中的R(x)对应集合中x的范围，通常是来自于某个既有集合中的元素，如s.has(x)，P(x)对应x取值的约束。

操作符主要分为子类型关系操作符、等价关系操作符、推理操作符、变量引用操作符。

E1<:E2    //如果类型E1是类型E2的子类型(包括相同类型)，则该表达式的结果为真，否则为假。

b_expr1 <==> b_expr2    //意义为b_expr1 == b_expr2
b_expr1 <=！=> b_expr2    //意义为b_expr1 ！= b_expr2

//数理逻辑中的蕴含运算符
b_expr1==>b_expr2
b_expr1<==b_expr2

othing    // 指空集
everything    // 指全集

JML方法规格

方法规格核心内容包括前置条件、后置条件和副作用约定，有着正常行为规格和异常行为规格之分，异常行为规格还可以使用signals子句。

前置条件

requires P；    //前置条件通过requires语句表示

后置条件

ensures P    //后置条件通过ensures语句表示

副作用约定

//副作用约定可由assignable或modifiable语句来表示，二者几乎无差别
assignable x
modifiable x

signals子句

signals (***Exception e) b_expr    //当 b_expr 为 true 时，方法会抛出括号中给出的相应异常e

signals_only e　　//满足前置条件就会抛出异常e

JML类型规格

类型规格主要有不变式以及状态变化约束两种

不变式（invariant）是要求在所有可见状态下都必须满足的特性，以下六个状态均为可见状态

• 对象的有状态构造方法（用来初始化对象成员变量初值）的执行结束时刻
• 在调用一个对象回收方法(finalize方法)来释放相关资源开始的时刻
• 在调用对象o的非静态、有状态方法(non-helper)的开始和结束时刻
• 在调用对象o对应的类或父类的静态、有状态方法的开始和结束时刻
• 在未处于对象o的构造方法、回收方法、非静态方法被调用过程中的任意时刻
• 在未处于对象o对应类或者父类的静态方法被调用过程中的任意时刻

语法上定义 invariant P ，其中 invariant 为关键词， P 为谓词。

状态变化约束规定对象在变化时满足一定的约束条件

constraint counter == old(counter)+1;    //约束每次修改counter只能加1。

语法上定义 constraint P ，其中 constraint 为关键词， P 为谓词。

JML主要工具链

我们目前主要用到了openjml以及JMLUnitNG来做我们的作业。

openJML可以用于对带有JML注释的Java代码执行静态检查，运行时断言检查和其他任务。

JMLUnitNG可以根据JML注释自动生成testNG测试样例来测试自己的程序

部署JMLUnitNG/JMLUnit，实现自动生成测试用例

由于JMLUnitNG对Windows操作系统不够友好，我始终没有能够按照评论区中的方法成功，因此我使用了自己编写的java测试程序

package test;

public class Test {
    /*@ public normal_behaviour
      @ ensures 
esult == lhs + rhs;
    */
    public static int add(int lhs, int rhs) {
        return lhs - rhs;
    }

    public static void main(String[] args) {
        add(1514,1);
    }
}

可以发现我的实现并不符合JML的规格。

我将上述代码保存在Test.java文件中，存放在test文件夹下，依次输入下图的指令

最终得到了如下结果

可以看到测试程序成功找到了错误数据。

第九次作业

作业设计结构

本次作业结构比较简单，只需要使用两个类，按照指导书的说明去做就好了，我没有什么可以分析自己的架构的。

                                                                                            第九次作业的类图

作业度量分析

本次作业中我的MyPath类中的comparesTo和equals方法使用了较多逻辑语句比较大小和判断是否相同，所以ev复杂度有些高了。

                                                                                                  第九次作业的度量图

作业BUG分析

本次作业我的程序没有被找到BUG。

发现他人BUG策略

由于本次作业代码量小，大家按照指导书所给JML编写比较好，因此我主要通过阅读他人代码来分析BUG，最终没有发现BUG

第十次作业

作业设计结构

本次作业结构比上一次稍复杂一点，但是我们所需要做的只是在原来架构的基础上增加一些图论上的算法，我主要通过Floyd算法来计算是否连通以及计算最短路径。

但是我出现了问题，我无法让MyGraph继承MyPath，所有我使用了将MyPath完全复制到MyGraph的方法，这使得我的架构变得既复杂又丧失了递进的结构层次。

                                                                                                                                 第十次作业的类图

作业度量分析

本次作业中我继承了上次作业中MyPath类出现的问题，还出现了由于将Graph和PathContainer整合在一起而出现的addPath方法逻辑复杂的问题，而getShortestPathLength方法由于判断是否抛出异常使用了一些相对较多的分支语句被判定是比较复杂，同时由于Floyd算法本身需要三重循环所以这一方法也出现了方法逻辑复杂的问题。

                                                                                                         第十次作业的度量图

作业BUG分析

我的程序并没有被发现BUG

发现他人BUG策略

由于本次作业代码量明显增大，同时大家的程序也编写的相当好，因此我没能找到BUG。

第十一次作业

作业设计结构

本次作业结构相当复杂，比上次的数据结构增加了线路的概念，使得程序的编写相当繁琐。

我采取了评论区中王嘉仪大佬的算法结构，抛弃了本来使用的拆点策略，大大降低了算法的复杂度，在这里对他表示由衷的感谢与敬佩。

我这次将上一次作业中的MyGraph类保留了下来，新建了MyRailwaySystem类作为本次的主要调用的类，新建了NewRailwayGraph类作为实现线路的类，新建了Edge类来表示数据结构中边的概念。

我个人认为本次的实现架构还算比较合理，但是存在两点问题

• 之前的MyGraph类虽然被保留下来但是还是有一些不能完全吻合这次作业的要求的，这是我的MyGraph类的可延展性出现了问题，并且我由于这一问题出现了因为没有完全改正的BUG。
• 我没有对点建立数据结构，这导致我在图中使用了大量的HashMap来存储一些对应关系。

 

                                                                                                                                                                         第十一次作业的类图

作业度量分析

本次作业中我首先有着从MyPath类和MyGraph类中继承来的一些复杂度方面的问题，在其他类中，我的三个获取票价、不满意度、换乘的方法都因为判断是否抛出异常时使用了相对较多的分支语句被判定是复杂度较高，而Floyd方法和getDistance方法均使用了Floyd算法，较高的循环层数使其复杂度较高，而我的removePath方法也因为在判断上使用了较多的分支和循环语句而复杂度略高。

                                                                                                         第十一次作业的度量图

作业BUG分析

本次作业我的程序ArrayList的add方法的使用方法BUG，即add方法若第一个参数为int类型，第二个参数为ArrayList所存储的类型，则方法会将第二个参数插入到List的第一个参数为下标的位置，并且将所有之后的数据向后挪一位。如果我插入后存在数据向后移动，那么我就会出现问题，因此我将ArrayList换为HashMap

private HashMap<Integer, LinkedList<Edge>> link = new HashMap<>(); // change ArrayList to HashMap
...
link.put(i, new LinkedList<>()); // change add to put
...
link.put(dest, tmpList); // change add to put

还有一个BUG在于将MyGraph移植过来后没有完整修改，由于我改变了两点之间的边的计数方法，但是我没有改变是否存在相联边的判断方法而出现BUG

return graph[x][y] >= 1; // change == to >=

发现他人BUG策略

由于本次作业代码量相当大，因此我采用了随机数据自动化测试并对拍的方式寻找别人BUG，最终成功hack他人6次。

对规格撰写和理解上的心得体会

JML对于大型项目中不同人相互之间的协作有着很大的帮助，可以使程序员准确得知各个方法的具体需要实现的功能。