OO第三次博客作业

JML是用于对Java程序进行规格化设计的一种表示语言，有两种主要的用法，一是开展规格化设计，二是针对已有的代码实现，书写其对应的规格，从而提高代码的可维护性，本单元的三次作业和两次实验就针对这些内容展开。

JML理论基础

JML的设计考虑到了未来扩展需要，把语言分成了几个层次，其中level 0是最核心的语言特征，要求所有的JML工具都要支持。在本单元开始前，课程组就下发了JML level 0手册，经过一个月的学习，现将主要的用法总结如下：

方法规格

1、前置条件通过requires子句来表示，在代码中通过if-else实现。一个方法规格中可以有多个requires子句，是并集的关系，调用者必须满足所有前置条件中的一个，对于不满足所有前置条件的输入，方法的实现不保证方法调用结果的正确性。

2、后置条件通过ensures子句来表示，同样的，一个方法规格中也可以有多个ensures子句，是交集的关系，对于满足前置条件的调用，方法实现者必须同时满足所有ensures子句的要求。

3、JML提供了区分正常行为和异常行为的机制，public normal_behavior对方法的正常功能行为给出规格，public exceptional_behavior对方法的异常行为给出规格。异常规格中要使用signals或signals_only子句，前者在满足某个条件时会抛出符合相应类型的异常，而后者则在满足前置条件时就抛出相应的异常。一个方法规格中可以使用多个public normal_behavior和public exceptional_behavior。

3、副作用约束使用关键词assignable来表示可以进行修改的对象，包括两种形态，一种是指明具体的变量列表，另一种是使用othing和everything这两个关键词，表示当前作用域内可见的所有类成员变量和方法输入对象。

4、对于设计中出现的纯访问性的方法，可以使用pure关键词进行表示，方法规格中的前置条件可以引用pure方法返回的结果。

5、forall是全称量词，表示对于给定范围内的元素都应该满足相应的约束。exists是存在量词，表示对于给定范围内的元素，存在某个元素满足相应的约束。

数据规格

本单元作业主要接触了两类数据规格，不变式限制invariant和约束限制constraints。invariant只针对可见状态的取值进行约束，constraint对前序可见状态和当前可见状态的关系进行约束。这里需要注意的是，凡是会修改成员变量的方法执行期间，对象的状态都不是可见状态，换句话说，在方法执行期间，对象的不变式限制和约束限制有可能不满足。

JML工具链

openjml

将所有要检查的java文件路径放在一个txt文件中：

使用check选项检查JML语法：

使用esc选项进行代码静态检查：

报错的是Group.java中以下两个方法：

    /*@ ensures 
esult == (people.length == 0? 0 : 
      @          ((sum int i; 0 <= i && i < people.length; people[i].getAge()) / 
      @			 people.length));
      @*/
    public /*@pure@*/ int getAgeMean();
    
    /*@ ensures 
esult == 
      @			(people.length == 0? 0 : ((sum int i; 0 <= i && i < people.length;
      @			(people[i].getAge() - getAgeMean()) * (people[i].getAge()
      @ 		- getAgeMean())) / people.length));
      @*/
    public /*@pure@*/ int getAgeVar();

做如下修改后通过了检查：

    /*@ public normal_behavior
      @ requires people.length > 0;
      @ ensures 
esult ==
      @          ((sum int i; 0 <= i && i < people.length; people[i].getAge()) / 
      @			 people.length);
      @ also
      @ public normal_behavior
      @ requires people.length == 0;
      @ ensures 
esult == 0;
      @*/
    public /*@pure@*/ int getAgeMean();

    /*@ public normal_behavior
      @ requires people.length > 0;
      @ ensures 
esult == ((sum int i; 0 <= i && i < people.length;
      @          (people[i].getAge() - getAgeMean()) * (people[i].getAge() - 
      @		     getAgeMean())) / people.length);
      @ also
      @ public normal_behavior
      @ requires people.length == 0;
      @ ensures 
esult == 0;
      @*/
    public /*@pure@*/ int getAgeVar();

JMLUnitNG

使用自己写的Calculate类进行测试：

public class Calculate {

    /*@ ensures 
esult == a+b;
      @*/
    public static int add(int a, int b) {
        return a + b;
    }

    /*@ ensures 
esult == a-b;
      @*/
    public static int sub(int a, int b) {
        return a - b;
    }

    /*@ ensures 
esult == a*b;
      @*/
    public static int mul(int a, int b) {
        return a * b;
    }

    /*@ requires b > 0;
      @ ensures 
esult == a/b;
      @*/
    public static int dev(int a, int b) {
        return a / b;
    }

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

依次使用如下命令进行自动化测试：

java -jar jmlunitng.jar D:openjmlCalculate.java
javac -cp jmlunitng.jar *.java
java -jar openjml.jar -rac Calculate.java
java -cp jmlunitng.jar Calculate_JML_Test

第一步生成.java文件：

第二步生成.class文件：

第三步得到相应的JML_TEST程序文件，然后第四步运行即可看到自动生成的样例以及给出的结果，根据测试样例可以看出，JMLUnitNG只对边界数据进行了测试：

第一次作业

第一次作业只实现了person类和简单社交关系的模拟和查询，主要目标在于对JML入门级的理解和实现，代码量较少，实现也比较简单，唯一的坑点就在iscircle函数要注意自己和自己是认识的，并且熟悉程度是0。这次作业强测和互测都没有被发现bug，也没有hack到同屋其他同学。

第二次作业

第二次作业增加了Group类，对人进行了分组，并增加了很多操作。为避免超时我使用了缓存的机制，在MyGroup类中增加了以下成员变量：

private int relationSum = 0;
private int valueSum = 0;
private BigInteger conflictSum = BigInteger.ZERO;
private int ageSum = 0;
private int ageMean = 0;
private int ageVar = 0;

在每次向组内加人时，将relationSum,valueSum,conflictSum,ageSum 四个变量进行更新，并将ageMean和ageVar两个变量赋值为0，代表在查询时要重新进行计算。

@Override
public int getAgeMean() {
    if (ageMean == 0 && people.size() != 0) {
        ageMean = ageSum / people.size();
    }
    return ageMean;
}

@Override
public int getAgeVar() {
    if (ageVar == 0 && people.size() != 0) {
        ageMean = ageSum / people.size();
        for (int i : people.keySet()) {
            ageVar += Math.pow(people.get(i).getAge() - ageMean, 2);
        }
        ageVar /= people.size();
    }
    return ageVar;
}

当向社交网络中增加关系时，如果两人在同一组中，需要将组内relationSum,valueSum两个变量进行更新。

HashSet<Group> groupHashSet = ((MyPerson) people.get(id1)).getGroups();
for (Group group : ((MyPerson) people.get(id2)).getGroups()) {
	if (groupHashSet.contains(group)) {
		((MyGroup) group).updateRelationAndValue(value);
    }
}

本次作业强测和互测都没有被发现bug，使用可能会超时的数据也没有hack到同屋其他同学。

第三次作业

这一次作业新增了很多的查询操作，难度增加了不少，主要是在考验图论相关的算法。时间复杂度较高的算法主要有：queryMinPath查询两点间的最短路径，queryStrongLinked查询两点是否是点双联通的，queryBlockSum查询社交网络中连通子图的个数。在课下，我最短路径使用的是经典的Dijkstra算法，queryStrongLinked使用朴素的dfs查找是否有包含id1和id2两点的环，连通子图的个数是在加人和加关系时使用了并查集的算法，然后在强测中成功CTLE。

经过与同学的交流，我对Dijkstra算法进行了堆优化，新增了Distance类，用优先队列进行存储，每次可以直接从队首取出最小值，省去了O(n)遍历求最小值的过程。queryStrongLinked方法使用遍历割点的方式，先用dfs深度优先遍历找到两点间的一条路径，然后依次将路径上的点删去，如果两点依然连通，说明两点是点双连通的。

心得体会

本单元的作业看似难度不大，但相比于看指导书自己设计架构并进行代码的实现，通过JML来进行程序设计很容易局限思维，只注重实现的正确性而忽略性能和架构。其实在作业中不能一味的对照JML写代码，而是要自己思考应该用什么样的数据结构进行存储，用什么样的算法来进行查询才能很好的完成本单元的作业。

在作业中，我们主要训练的是阅读规格写代码的能力，其实根据设计书写规格以及依据规格开展单元化测试的能力同样重要，同样能体现出规格的重要意义。如此一来，方法的调用者不需要考虑方法内部的具体代码实现，只需要通过规格将功能描述清楚，而方法的实现者只需要考虑如何依据规格进行实现，在保证正确性的同时提升性能。这种契约化编程的思想可以将程序的设计与实现分离，提供了更加严谨的程序设计方式。