OO_UNIT3_SUMMARY

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

1）JML理论基础：

1. 常用JML表达式：

   \result表达式：表示一个非void类型的方法执行所获得的结果，即方法执行后的返回值\old(expr)表达式：用来表示一个表达式expr在相应方法执行前的取值

   \not_assigned(x,y,...)表达式：用来表示括号中的变量是否在方法执行过程中被赋值。如果没有被赋值，返回为true，否则返回false。

   \typeof(expr)表达式：该表达式返回expr对应的准确类型。

   \forall表达式：全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。(\forall int i,j; 0 <= i && i < j && j < 10; a[i] < a[j])，意思是针对任意0<=i<j<10，a[i]<a[j]。这个表达式如果为真(true)，则表明数组a实际是升序排列的数组

   \exists表达式：存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束。(\exists int i; 0 <= i && i < 10; a[i] < 0)，表示针对0<=i<10，至少存在一个a[i]<0。

   \sum表达式：返回给定范围内的表达式的和。(\sum int i; 0 <= i && i < 5; i)，这个表达式的意思计算[0,5)范围内的整数i的和，即0+1+2+3+4==10。

2. 常见操作符

   (1) 子类型关系操作符：E1<:E2，如果类型E1是类型E2的子类型(sub type)，则该表达式的结果为真，否则为假。

   (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。对于表达式b_expr1==>b_expr2而言，当b_expr1==false，或者b_expr1==true且b_expr2==true时，整个表达式的值为true。

   (4) 变量引用操作符：。\nothing指示一个空集；\everything指示一个全集，即包括当前作用域下能够访问到的所有变量。变量引用操作符经常在assignable句子中使用，如assignable \nothing表示当前作用域下每个变量都不可以在方法执行过程中被赋值。

3. 方法规格：方法规格的核心内容包括三个方面，前置条件、后置条件和副作用约定。

   前置条件：前置条件通过requires子句来表示：requires P;

   后置条件：后置条件通过ensures子句来表示：ensures P;

   副作用条件：使用关键词assignable或者modifiable

4. 其他：

   不变式（invariant）：是要求在所有可见状态下都必须满足的特性，语法上定义invariant P，其中invariant为关键词，P为谓词

   状态变化约束（constraint）：用constraint来对前序可见状态和当前可见状态的关系进行约束。

2）应用工具链情况：

在网上找到的JML的资料比较少，可能也是因为jml发展还不够完备，了解到的JML的工具主要有三个：OpenJml（用于检查JML规格的语法）；SMT Solver（用于检查代码与JML是否一致）；JMLUnitNG（用于自动生成测试代码）。

二：部署JMLUnitNG/JMLUnit，针对Group接口的实现自动生成测试用例，并结合规格对生成的测试用例和数据进行简要分析

//采用以下命令生成
java -jar .\jmlunitng.jar .\jml\MyGroup.java

javac -cp .\jmlunitng.jar .\jml\*.java

java -jar .\openjml.jar -rac .\jml\Demo.java

java -cp .\jmlunitng.jar jml.Demo_JML_Test
// 结果如下
    
C:\Users\nishirong\Desktop\ll>java ~cp jmlunitng~l_4・jar test. MyGroup_JML_Test
[TestNG] Running:
  Command line suite


Failed: racEnabled()
Passed: constructor MyGroup(-2147483648)
Passed: construetor MyGroup(0)
Passed: construetor MyGroup(2147483647)
Passed: <<test. MyGroup@80000000>>. addGroupRelation(-2147483648)
Passed: <<test. MyGroup@0>>. addGroupRelation(-2147483648)
Passed: <<test. MyGroup@7fffffff>>. addGroupRelation(-2147483648)
Passed: <<test. MyGroup@80000000>>. addGroupRelation(0)
Passed: <<test. MyGroup@0>>. addGroupRelation(0)
Passed: <<test. MyGroup@7fffffff>>. addGroupRelation(0)
Passed: <<test. MyGroup@80000000>>. addGroupRelation(2147483647)
Passed: <<test. MyGroup@0>>. addGroupRelation(2147483647)
Passed: <<test. MyGroup@7fffffff>>. addGroupRelation(2147483647)
Failed: <<test. MyGroup@80000000>>. addPerson(null)
Failed: <<test. MyGroup@0>>. addPerson(null)
Failed: <<test. MyGroup@7fffffff>>. addPerson(null)
Passed: <<test. MyGroup@80000000>>. delPerson(null)
Passed: 〈〈test. MyGroup@0>>・ delPerson(null)
Passed: <<test. MyGroup@7fffffff>>. delPerson(null)
Passed: <<test. MyGroup@80000000>>. equals(null)
Passed: 〈〈test. MyGroup@0>>・ equals(null)
Passed: 〈〈test. MyGroup@7fffffff>>・ equals(null)
Passed: <<test. MyGroup@80000000>>. equals(java. lang. Object@4cee07)
Passed: <<test. MyGroup@0>>. equals(java. lang. Object@161e840)
Passed: <<test. MyGroup@7fffffff>>. equals(java. lang. Object@629d6e)
Passed: <<test. MyGroup@80000000>>. getAgeMeanO
Passed: <<test. MyGroup@0>>. getAgeMeanO
Passed: <<test. MyGroup@7fffffff>>. getAgeMeanO
Passed: <<test. MyGroup@80000000>>. getAgeVar ()
Passed: <<test. MyGroup@0>>. getAgeVar ()

Passed: <<test. MyGroup@80000000>>. getConf1ictSum()
Passed: <<test. MyGroup@0>>. getConf1ictSum()

可以看到，jmlunitng的测试照顾到了每个函数，总体的测试效果还是不错的，而且依照规格看，jmlunitng所生成的测试用例基本和相关的规格要求。

三：架构设计及模型构建策略

第一次：

第一次作业比较简单，只要按照规格实现函数就行。需要注意的只有isCircle函数，这里采用了bfs算法判断两个人是不是“相连接”。

---

第二次：第二次作业由于性能的限制，不能简单地实现单个函数，要根据jml提出的功能需求想办法尽可能减低函数实现的复杂度。具体主要体现在Group的getRelationSum() 和 getValueSum()两个函数上，如果仅仅按照规格描述的实现，那么每次调用这两个函数都要对group所有人进行一次双重遍历。而数据量可能是很大的，所以很可能会超时。

为此，深层次分析如何优化这两个函数。拿valueSum为例，整个group的valueSum增加只有两种情况，一种是在addRelation的时候如果两个人同属于一个group这时候要增加；二是在往group里面加人的时候如果某两个人有联系那么这个group的valueSum也要增加。所以只需要在group的addPerson中增加valueSum，以及在addRelation时增加valueSum即可

addPerson中增加valueSum

 @Override
    public void addPerson(Person person) {
        this.people.add(person);

        for (int i = 0; i < people.size(); i++) {
            if (person.isLinked(people.get(i))) {
                if (i != people.size() - 1) {
                    relationSum += 2;
                    valueSum += 2 * people.get(i).queryValue(person);

                }

            }
        }
    }

addRelation时增加valueSum

   @Override
    public void addRelation(int id1, int id2, int value) throws
            PersonIdNotFoundException, EqualRelationException {

        //....其他代码
        List<Group> groups1 = ((MyPerson)p1).getGroup();
        List<Group> groups2 = ((MyPerson)p2).getGroup();

        for (Group tmp1 : groups1) {
            if (groups2.contains(tmp1)) {
                ((MyGroup)tmp1).setRelationSum();
                ((MyGroup)tmp1).setValueSum(p1.queryValue(p2)); 
            } 
        }
       //...其他代码
    }

---

第三次:第三次作业我觉得要特别注意对实现规格时算法的选择。此外从迭代的角度考虑，由于第二次作业对Group的getRelationSum() 和 getValueSum()两个函数做了如上优化，所以在实现第三次作业Group新加入的delPerson的时候，也要考虑到这两个函数的返回值情况。这样虽然耦合度有一定的增加，但是从性能优化的角度来看，还是很可观的。

函数的算法设计：

1. public int queryMinPath(int id1, int id2)

   这个函数抽象出来就是求图中两个点之间的最短路径，可选择的算法有：dijkstra算法、Floyd算法。考虑时间复杂度，选择较低的dijkstra算法。要注意的是初始化id1到其他点的距离的时候，如果queryValue(id1, idx)返回值是0的话，有两种情况，一种是这两个点的value就是0，还有一种是这两个点不直接相连，不直接相连的点初始化距离的时候要设置成无穷大。所以在初始化id1到其他点距离的数组的时候，可以直接根据getPerson(id1).isLinked(people.get(i))来判断是否赋值成无穷大。

2. public boolean queryStrongLinked(int id1, int id2)

   这个函数是求图中两个点是否双连通，点双连通的算法可以用tarjan。我这里采用的是先bfs出一条路径，记录这条路径，然后遍历删除这条路径上的每个点再次bfs看有没有其他路径的方法，本质就是：先找出一条路径，然后查看这条路径上是否有割点，没有返回true，有的话返回false。特殊情况是如果第一次找到的路径是id1和id2直接相连，此时还要查看此路径之外还有没有其他路径。

3. public int queryBlockSum()

   这个函数是求图中连通块的个数，最好的算法就是并查集，具体实现并查集算法只需要在addRelation的时候将两个人放到一个连通块里面就可以。另外多开一个blockSize[]数组记录每个连通块的大小。这样在调用该函数的时候，只要返回blockSize中不为零的数组元素的个数就可了。

   并查集核心算法：

    private void join(int a, int b) {//合并连通块
           int x = unionFind(a);
           int y = unionFind(b);
   
           if (blockSize[x] == 0) {
               blockSize[x] = 1; 
           }
           if (blockSize[y] == 0) {
               blockSize[y] = 1; 
           }
           if (x != y) {
               pre[y] = x;
               blockSize[x] += blockSize[y]; 
               blockSize[y] = 0;
           } 
    }
   
       private int unionFind(int son) { //找根and压缩路径
           int root = son;
           while (root != pre[root]) {
               root = pre[root]; 
           }
           int sonx = son;
           while (sonx != root) {
               int tmp = pre[sonx];
               pre[sonx] = root;
               sonx = tmp; 
           }
           return root;
       }
   

四：代码实现的bug和修复情况

第一次是因为isCircle的dfs有问题，我也一直没测出来有什么问题，数据量很大的话就会导致dfs一直出不来，我觉得可能是由于递归太多层导致的，反正最后还是改成了没有递归的bfs。

第二次的主要问题就是超时，问题却出现在第一次实现的queryNameRank上，因为这里我完全照着规格写的，调用network里面的compare来比较两个人的name，这样做会导致每次比较name都要遍历一次所有人，而第二次的数据又很大，所以就出现了严重超时的现象。改也很简单，就是直接比较name，用字符串比较就完了。

还有一个地方就是 group里面计算relationSum和valueSum的时候，没考虑优化，照搬规格，导致每次查询这两个都要用两重循环遍历整个group；我修改的方法是，拿valueSum为例，整个group的valueSum增加只有两种情况，一种是在addRelation的时候如果两个人同属于一个group这时候要增加；二是在往group里面加人的时候如果某两个人有联系那么这个group的valueSum也要增加。

还是太单纯，也没动脑子，就照着规格半个小时写完了，一看中测过了，改改风格也没管了，结果bug一大堆。

第三次吸取前两次的教训，实现规格之前还是仔细想了一下算法的复杂度的情况，写完了之后也用Junit自己测试了，但还是出现了一些问题，第一就是求最短路径的dijkstra算法初始化的时候，把所有的quaryValue为0的distance都初始化成了无穷大，应该我没有仔细看两个人之间value的范围，我以为都是大于0的，后来才看到有等于0的情况。

还有就是isStrongLinked我是采用bfs出一条路径，然后遍历删除每个点，然后再bfs看有没有其他路径的方法来实现的。出问题的地方是如果我第一次bfs的路径中恰好就是id1和id2两个点，那么我就直接返回false了，这种情况下我没有判断有没有其他通路；bug修改就是将原来的bfs改造了一下，让它第一次遍历id1的acquaintance的时候排除掉id2，这样就能保证判断出有没有id1和id2之外的其他路径。

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

只有实验课做了一些规格填空，作业都是根据规格实现代码，我觉得用规格表达设计实现首先是制定了怎么表达设计思想的标准，目的当然是为了建立便于设计师和程序员高效、规范的沟通机制。但是我个人觉得JML语言有些地方过于啰嗦而且也不太容易阅读，比如往一个List里面增加一个元素，JML里面还要表达“保持其他元素都不变”的这个意思。而且照我这几次作业的经验，JML我前两次都是傻傻地按照规范写，后面发现不行，还是要自己思考怎么实现。那么JML对我来说也就是提出了一个需求，而这个需求还是我根据JML费劲想出来，我觉得还是不如自然语言直接讲需求来的高效。但也不能一棒子打死，JML既然发展起来，说明它也有自己的优势，“规范”的标准是任何自然语言不能代替的。所以我认为，可以采用自然语言和JML相结合的方式提出需求，自然语言作为JML的补充。本单元作业只给出了JML，然后就让直接实现了，体验不是太好，有些抓不住实现重点的感觉，所以还是希望能考虑将自然语言和JML结合，以高效沟通为目的，而不是单纯考察阅读JML。