BUAA_OO_Summary_StageThree

一、JML语言理论基础

JML简述

JML(Java Modeling Language)是用于对Java程序进行规格化设计、行为接口规格语言（Behavior Interface Specification Language，BISL）。通过JML及其支持工具，不仅可以基于规格自动构造测试用例，并整合了SMT Solver等工具以静态方式来检查代码实现对规格的满足情况。

JML关键语法

方法规格

normal_behavior：正常行为,说明方法的正常行为
exceptional_behavior：异常行为，说明方法的异常行为
requires：前置条件，调用者保证满足的方法运行条件
assignable：约束条件，约束方法可以修改的数据域
ensures：后置条件，方法在前置条件满足的情况下保证的输出
signals：异常抛出，说明抛出某个异常要满足的条件

类型规格

invariant：不变式，数据域在所有可见状态下都必须满足的特性
constraint：状态变化约束，数据域状态变化所满足的约束

原子表达式

old(expr)：执行前状态，表示expr在方法执行前的取值
esult：结果代词，指代一个非void型方法执行的结果
onnullelements(container)表达式：表示 container 对象中存储的对象不会有 null
ype(type)表达式：返回类型type对应的类型(Class)
ypeof(expr)表达式：该表达式返回expr对应的准确类型。

应用工具链情况

OpenJML：用于检查JML文档规格语法
JMLUnitNG：基于JML的单元测试工具，能够自动生成测试用例，注重边界条件的测试
Junit：单元测试，可用于编写和可重复运行的自动化测试。

二、OpenJML验证

SMT Solver是openjml的基础组件，在进行openjml在进行验证时调用SMT Solver。

通过这条指令调用openjml进行验证：java -jar $OPENJML /openjml.jar <options> <files>

//静态验证结果
C:Users24501Desktop2020SpringObject-OrientedHOMEWORKstage3oo2020_unit3_spec3srccomoocoursespec3main>java -jar C:Users24501Desktop2020SpringObject-OrientedHOMEWORKstage3openjmlopenjml.jar -exec C:Users24501Desktop2020SpringObject-OrientedHOMEWORKstage3openjmlSolvers-windowsz3-4.7.1.exe -esc @java.txt
C:Users24501Desktop2020SpringObject-OrientedHOMEWORKstage3oo2020_unit3_spec3srccomoocoursespec3mainGroup.java:57: 错误: 不可比较的类型: int和INT#1
    /*@ ensures 
esult == (people.length == 0? 0 :
                        ^
  其中, INT#1是交叉类型:
    INT#1扩展Number,Comparable
C:Users24501Desktop2020SpringObject-OrientedHOMEWORKstage3oo2020_unit3_spec3srccomoocoursespec3mainGroup.java:62: 错误: 不可比较的类型: int和INT#1
    /*@ ensures 
esult == (people.length == 0? 0 : ((sum int i; 0 <= i && i < people.length;
                        ^
  其中, INT#1是交叉类型:
    INT#1扩展Number,Comparable
2 个错误

动态验证只是把最后的一个参数-exc改为-rac，反馈信息太长我就不在这放了

但是据大佬说是因为forall和exist均不能被openjml识别，所以对我们这次的JML验证非常不便

为了不用每次调用openjml都输入超长的参数，可以进行如下配置：

::openjml.bat
@echo off
set java=java -jar "%~dp0openjml.jar" -noPurityCheck
set prove=-prover cvc4 -exec "%~dp0Solvers-windowscvc4-1.6.exe"
set runtime=-cp %~dp0jmlruntime.jar;
set allparam=
set rac=
:param
set str=%1
if "%str%"=="" (
    goto end
)
if "%str%"=="-rac" (
	set rac=rac
)
if "%str%"=="-prove" (
	set str=%prove%
)
set allparam=%allparam% %str%
shift /0
goto param
:end
if "%allparam%"=="" (
    goto eof
)
rem remove left right blank
:intercept_left
if "%allparam:~0,1%"==" " set "allparam=%allparam:~1%"&goto intercept_left
:intercept_right
if "%allparam:~-1%"==" " set "allparam=%allparam:~0,-1%"&goto intercept_right
:eof
%java% %allparam%
set filename=
if "%rac%"=="rac" (
	:input
	set /p filename=Input file name:
	if "%filename%"=="" (
		goto input
	)
	java %runtime% %filename%
)
pause

三、部署JMLUnitNG

这个MyGroup类的测试怎么改都是从第一步运行JMLUnitNG.jar就开始疯狂报错，我是真的懵了

最后觉得还是从简单的入手，自己随手写了一个类，目录树如下，test中放有测试类Adder.java

第一步是运行JMLUnitNG.jar：java -jar jmlunitng-1_4.jar test/Adder.java

第二步是编译里头生成的所有Java文件，并用openjml验证：

javac -cp jmlunitng-1_4.jar ./test/*.java

java -jar openjml.jar -rac test/Adder.java

第三步是运行生成的测试代码：java -cp jmlunitng-1_4.jar test/Adder_JML_Test

结果如下：

[TestNG] Running:
  Command line suite

Passed: racEnabled()
Passed: constructor Adder()
Failed: static add(-2147483648, -2147483648)
Passed: static add(0, -2147483648)
Passed: static add(2147483647, -2147483648)
Passed: static add(-2147483648, 0)
Passed: static add(0, 0)
Passed: static add(2147483647, 0)
Passed: static add(-2147483648, 2147483647)
Passed: static add(0, 2147483647)
Failed: static add(2147483647, 2147483647)

===============================================
Command line suite
Total tests run: 11, Failures: 2, Skips: 0
===============================================

不难看出，基本上测试数据都集中在边界条件上，而且很明显测试出了溢出导致的错误
但是尽管如此，它也只方便进行一些简单代码的测试。并没有起到很好的辅助/减轻工作量的效果。感觉工具链工具链还不够完善，期待后续能看到他们有较好的使用效果。

四、梳理作业架构设计

第一次作业

第一次作业基本上主需要直接按照给定的JML实现，其中isCircle方法为了降低时间复杂度采用并查集实现，并查集对于在作业三增加的queryBlockSum方法也是极为高效的。

第一次作业UML图

第二次作业

增加了Group接口，对应实现MyGroup类。

本次作业需要针对JML给出的方法自行设计，MyGroup类中的一切求和方法需要设计相应属性存储，在关系改变和addPeople时进行属性的改变。

对于直接照着JML实现会超时，本人亲身经历=_=

除此之外，为了减少时间，每个类中的容器采取用HashMap<Ineteger,Person>的形式存储，减少索引的时间，考虑到测试时Person上限为5000的问题，初始时设置HashMap容量为8192，防止size达到总容量的0.75而扩容重新建立Map所浪费的时间。

第二次作业UML图

第三次作业

第三次作业增加从Group中删除Person的方法，需要注意的是第二次作业中所设置的属性值在delPerson时注意修改，

第三次作业增加了几个方法稍微有些复杂，分别是queryBlockSum,queryMinPath和queryStrongLink。

query_block_sum方法乍一看让人有些摸不着头脑，直接照着规格实现是万万不行的其JML规格如下：
```
  /*@ ensures 
esult == 
    @         (sum int i; 0 <= i && i < people.length && 
    @         (forall int j; 0 <= j && j < i; !isCircle(people[i].getId(), people[j].getId()));
    @         1);
    @*/
  public /*@pure@*/ int queryBlockSum();
```
但是仔细揣摩一下这个JML所给出的这个要求，再结合这个方法的名字，我们可以察觉到这个方法实际实在求图中连通块的个数，用并查集真的是太香了。
queryMinPath方法只是最典型的最短路径，课下实测用弗洛伊德会被卡死，我个人采用迪杰斯特拉外加优先队列来进行优化。

queryStrongLink方法是我花费了大量时间去想怎么实现的算法

最开始考虑的是先用BFS找一条路删掉再找有没有第二条路，美滋滋写完睡觉第二天突然发现你可能第一次找的路可能会把本来能找到的两条路都破坏掉而导致错误结果。
最后再想到的是暴力DFS将所有两点间的路都找出来，然后一一比对看有没有完全不同路径的。但个人感觉过于暴力，没有去实现。

最终在翻阅讨论区之后，决定学习一手Tarjan算法，手头没有算法书的我翻了一下午的博客，最终凭着顽强的毅力终于把它写完了。~~（泪目们，把公屏打在兄弟上o(╥﹏╥)o）~~

具体原理则是：由于两点间有两条不同的路，所以两点必定处于同一个双连通分量上，采取Tarjan在求割点的过程中即可求出图中所有的双连通分量。附一个我自己的实现：

public boolean tarjan(int id1) {
        visited.add(id1);
        low.put(id1, counter);
        dfn.put(id1, counter);
        counter++;
        Person person1 = peopleHashMap.get(id1);
        for (Map.Entry<Integer, Person> entry : ((MyPerson) person1).getAcquaintance().entrySet()) {
            int num = entry.getKey();
            if (visited.contains(num)) {
                if (father.containsKey(id1) && father.get(id1) != num) {
                    low.put(id1, Math.min(low.get(id1), dfn.get(num)));
                }
            } else {
                father.put(num, id1);
                push(id1, num);
                tarjan(num);
                if (low.get(num) >= dfn.get(id1)) {
                    HashSet<Integer> set = new HashSet<>();
                    int f = 0;
                    int r = 0;
                    do {
                        int[] edge = pop();
                        f = edge[0];
                        r = edge[1];
                        set.add(f);
                        set.add(r);
                    } while (f != id1 || r != num);
                   	dbMap.add(set);
                }
                low.put(id1, Math.min(low.get(id1), low.get(num)));
            }
        }
    }

第三次作业UML图

五、Test and Bug

Test

在课下测试时，主要是针对每个方法进行Junit测试，以及用python写了一份与其他同学进行对拍测试，但是没有多留意性能部分，导致第二次作业出了bug。

互测时，主要是针对JML规格，进行一些测试，以及针对某些方法进行大量测试测试是否超时。

Bug

第二次作业query_group_age_mean，query_group_age_var一开始没有采用属性的方式存储，导致超时。
其实有被同学提醒这个问题，不知道为什么上头了觉得就是不会超时=_=

六、规格撰写与理解上的心得体会

规格，侧重于功能而非实现，也就是先给出了一个具体地功能框架，方法是我们要实现的一个黑箱，而规格告诉我们他的输入输出的特点也就是我们要满足什么。

我认为，JML规格在软件开发和团队合作中是必不可少的。规格使得架构工程师、代码工程师和测试工程师之间更有效的协同工作，用代码进行交流。规格相比自然语言能够更全面更细致的描述方法和属性。

但在真正地实现上，我们还需要对代码进行合理的设计，绝不能一味的依赖于JML去实现，那会使得方法很笨重，我们在实现中要去考虑他的性能等因素。