北航OO（2020）第三单元博客作业

北航OO（2020）第三单元博客作业

JML语言总结

理论基础

JML是用于对Java程序进行规格化设计的一种表示语言，它使用JavaDoc注释的方式来表示规格。JML以Java语法为基础并进行了一定的扩充。JML的语法分为几个层次，下面对JML Level 0的核心特性进行简要的总结。

规格变量的声明

规格变量分为静态规格变量和实例规格变量两种。以整型数组为例，它们分别可以声明为//@public static model non_null int []elements和//@public instance model non_null int []elements。

常用表达式

表达式	含义
esult	非void类型的方法的返回值
old(`expr`)	一个表达式`expr`在相应方法执行前的取值（遵从引用规则）
ot_assigned(x, y, ...)	括号中的变量是否在方法执行过程中未被赋值
ot_modified(x, y, ...)	限制括号中的变量在方法执行期间的取值未发生变化
(forall T x; R(x); P(x))	全称量词，表示满足R(x)的x都满足P(x)
(exists T x; R(x); P(x))	存在量词，表示存在满足R(x)的x满足P(x)
(sum T x; R(x); `expr`)	对于满足R(x)的x，求`expr`的和
(max T x; R(x); `expr`)	对于满足R(x)的x，求`expr`的最大值
(min T x; R(x); `expr`)	对于满足R(x)的x，求`expr`的最小值
<==>	等价操作符
==>	蕴含操作符
othing	空集

方法规格

方法规格分为正常行为规格和异常行为规格两种，分别对应normal_behavior和exceptional_behavior。多个规格之间使用also连接。每种规格又可分为前置条件、副作用范围限定和后置条件，分别对应requires、assignable和ensures。多个子句之间为合取关系。

对于纯粹访问性的方法，即不会对对象的状态进行任何改变，也不需要提供输入参数，这样的方法无需描述前置条件，也不会有任何副作用，且执行一定会正常结束。对于这类方法，可以使用简单的（轻量级）方式来描述其规格，即使用pure关键词。在方法规格中，前置条件可以引用pure方法返回的结果。

对于异常行为规格，我们通常会使用signals或signals_only子句来抛出异常。signals子句的结构为signals (***Exception e) expr;意思是当expr 为true 时，方法会抛出括号中给出的相应异常e；signals_only子句的结构为signals_only ***Exception;，意思是一旦进入此子句，就会抛出相应的异常。

类型规格

类型规格指针对Java程序中定义的数据类型所设计的限制规则，一般而言，就是指针对类或接口所设计的约束规则。课程中的重点是不变式invariant和状态变化约束constraint。不变式invariant是要求在所有可见状态下都必须满足的特性，而状态变化约束constraint对对象状态的变化进行约束。

应用工具链情况

JML的工具链较不完善，且大都已很长时间没有维护。常用的JML工具主要有OpenJML（对JML进行语法检查、配合Solver进行简单的静态验证、以及运行时验证）、JMLUnitNG（自动化单元测试生成工具）和JMLUnit（类似前者）等。OpenJML有Eclipse插件版，使用体验较好。但是没有可用的IDEA插件是一个遗憾。

在http://www.eecs.ucf.edu/~leavens/JML//download.shtml这个页面上，有更多JML相关工具的介绍。

OpenJML验证情况

由于后两次作业无法通过OpenJML的语法检查，下面以第一次作业为例，演示OpenJML的验证。

Parsing and Type-checking

本功能主要检查JML规格的语法。

在IDEA的External Tools中，运行如下命令：java -jar openjml.jar -check "$FilePath$" -cp "$Classpath$" -sourcepath "$Sourcepath$" -encoding utf-8，即可进行JML的静态语法检查。-check参数指定检查类型为Parsing and Type-checking，-cp和-sourcepath命令用于指定Classpath和源文件目录，-encoding参数用于指定文件编码。

第一次作业的JML规格成功通过了该检查，返回值为0。

Extended Static Checking

本功能主要利用Solver对按照JML编写的程序进行简单的静态检查。

在IDEA的External Tools中，运行如下命令：java -jar openjml.jar -prover z3_4_7 -exec ".Solvers-windowsz3-4.7.1.exe" -esc "$FilePath$" -cp "$Classpath$" -sourcepath "$Sourcepath$" -encoding utf-8，即可进行JML的静态语法检查。-prover参数用于指定Solver类型，-exec参数用于指定Solver可执行程序，-esc参数指定检查类型为Extended Static Checking。

在对MyPerson检查的过程中，触发了36个警告，其中主要是The prover cannot establish an assertion，但这些警告似乎并不是由于程序的错误，而是Solver无法对程序进行充分的解析导致的；在对MyNetwork检查的过程中，触发了100个警告，其中主要仍是The prover cannot establish an assertion，且提示静态检查不支持对 ot_assigned表达式进行检查。由此可见，该功能对一些较为复杂的程序的支持还十分欠缺。

下面展示部分MyPerson类的检查结果：

.Unit3Homework1srccomoocourseimplements1MyPerson.java:82: 警告: The prover cannot establish an assertion (Postcondition: .Unit3Homework1srccomoocoursespec1mainPerson.java:67: 注: ) in method compareTo
return name.compareTo(p2.getName());
^
.Unit3Homework1srccomoocoursespec1mainPerson.java:67: 警告: Associated declaration: .Unit3Homework1srccomoocourseimplements1MyPerson.java:82: 注:
@ ensures esult == name.compareTo(p2.getName());
^
.Unit3Homework1srccomoocourseimplements1MyPerson.java:82: 警告: The prover cannot establish an assertion (ExceptionalPostcondition: .Unit3Homework1srccomoocoursespec1mainPerson.java:66: 注: ) in method compareTo
return name.compareTo(p2.getName());
^
.Unit3Homework1srccomoocoursespec1mainPerson.java:66: 警告: Associated declaration: .Unit3Homework1srccomoocourseimplements1MyPerson.java:82: 注:
@ public normal_behavior
^
.Unit3Homework1srccomoocourseimplements1MyPerson.java:53: 警告: The prover cannot establish an assertion (ExceptionalPostcondition: .Unit3Homework1srccomoocoursespec1mainPerson.java:29: 注: ) in method equals
return id == person.getId();
^
.Unit3Homework1srccomoocoursespec1mainPerson.java:29: 警告: Associated declaration: .Unit3Homework1srccomoocourseimplements1MyPerson.java:53: 注:
@ public normal_behavior
^
.Unit3Homework1srccomoocourseimplements1MyPerson.java:53: 警告: The prover cannot establish an assertion (Postcondition: .Unit3Homework1srccomoocoursespec1mainPerson.java:32: 注: ) in method equals
return id == person.getId();
^
.Unit3Homework1srccomoocoursespec1mainPerson.java:32: 警告: Associated declaration: .Unit3Homework1srccomoocourseimplements1MyPerson.java:53: 注:
@ ensures esult == (((Person) obj).getId() == id);
^
.Unit3Homework1srccomoocourseimplements1MyPerson.java:77: 警告: The prover cannot establish an assertion (Postcondition: .Unit3Homework1srccomoocoursespec1mainPerson.java:62: 注: ) in method getAcquaintanceSum
return acquaintance.size();
^
.Unit3Homework1srccomoocoursespec1mainPerson.java:62: 警告: Associated declaration: .Unit3Homework1srccomoocourseimplements1MyPerson.java:77: 注:
//@ ensures esult == acquaintance.length;
^
.Unit3Homework1srccomoocourseimplements1MyPerson.java:41: 警告: The prover cannot establish an assertion (Postcondition: .Unit3Homework1srccomoocoursespec1mainPerson.java:25: 注: ) in method getAge
return age;
^
.Unit3Homework1srccomoocoursespec1mainPerson.java:25: 警告: Associated declaration: .Unit3Homework1srccomoocourseimplements1MyPerson.java:41: 注:
//@ ensures esult == age;
^
.Unit3Homework1srccomoocourseimplements1MyPerson.java:36: 警告: The prover cannot establish an assertion (Postcondition: .Unit3Homework1srccomoocoursespec1mainPerson.java:22: 注: ) in method getCharacter
return character;
^
.Unit3Homework1srccomoocoursespec1mainPerson.java:22: 警告: Associated declaration: .Unit3Homework1srccomoocourseimplements1MyPerson.java:36: 注:
//@ ensures esult.equals(character);
^
.Unit3Homework1srccomoocourseimplements1MyPerson.java:26: 警告: The prover cannot establish an assertion (Postcondition: .Unit3Homework1srccomoocoursespec1mainPerson.java:16: 注: ) in method getId
return id;
^
.Unit3Homework1srccomoocoursespec1mainPerson.java:16: 警告: Associated declaration: .Unit3Homework1srccomoocourseimplements1MyPerson.java:26: 注:
//@ ensures esult == id;
^
.Unit3Homework1srccomoocourseimplements1MyPerson.java:31: 警告: The prover cannot establish an assertion (Postcondition: .Unit3Homework1srccomoocoursespec1mainPerson.java:19: 注: ) in method getName
return name;
^
.Unit3Homework1srccomoocoursespec1mainPerson.java:19: 警告: Associated declaration: .Unit3Homework1srccomoocourseimplements1MyPerson.java:31: 注:
//@ ensures esult.equals(name);
^
.Unit3Homework1srccomoocourseimplements1MyPerson.java:67: 警告: The prover cannot establish an assertion (Postcondition: .Unit3Homework1srccomoocoursespec1mainPerson.java:43: 注: ) in method isLinked
return id == person.getId() || acquaintance.containsKey(person);
^
.Unit3Homework1srccomoocoursespec1mainPerson.java:43: 警告: Associated declaration: .Unit3Homework1srccomoocourseimplements1MyPerson.java:67: 注:
@ ensures esult == (exists int i; 0 <= i && i < acquaintance.length;
^
.Unit3Homework1srccomoocourseimplements1MyPerson.java:67: 警告: The prover cannot establish an assertion (ExceptionalPostcondition: .Unit3Homework1srccomoocoursespec1mainPerson.java:41: 注: ) in method isLinked
return id == person.getId() || acquaintance.containsKey(person);
^
.Unit3Homework1srccomoocoursespec1mainPerson.java:41: 警告: Associated declaration: .Unit3Homework1srccomoocourseimplements1MyPerson.java:67: 注:
/@ public normal_behavior
^
.Unit3Homework1srccomoocourseimplements1MyPerson.java:72: 警告: The prover cannot establish an assertion (ExceptionalPostcondition: .Unit3Homework1srccomoocoursespec1mainPerson.java:55: 注: ) in method queryValue
return acquaintance.getOrDefault(person, 0);
^
.Unit3Homework1srccomoocoursespec1mainPerson.java:55: 警告: Associated declaration: .Unit3Homework1srccomoocourseimplements1MyPerson.java:72: 注:
@ public normal_behavior
^
.Unit3Homework1srccomoocourseimplements1MyPerson.java:72: 警告: The prover cannot establish an assertion (ExceptionalPostcondition: .Unit3Homework1srccomoocoursespec1mainPerson.java:48: 注: ) in method queryValue
return acquaintance.getOrDefault(person, 0);
^
.Unit3Homework1srccomoocoursespec1mainPerson.java:48: 警告: Associated declaration: .Unit3Homework1srccomoocourseimplements1MyPerson.java:72: 注:
/@ public normal_behavior
^
.Unit3Homework1srccomoocourseimplements1MyPerson.java:72: 警告: The prover cannot establish an assertion (Postcondition: .Unit3Homework1srccomoocoursespec1mainPerson.java:58: 注: ) in method queryValue
return acquaintance.getOrDefault(person, 0);
^
.Unit3Homework1srccomoocoursespec1mainPerson.java:58: 警告: Associated declaration: .Unit3Homework1srccomoocourseimplements1MyPerson.java:72: 注:
@ ensures esult == 0;
^
.Unit3Homework1srccomoocourseimplements1MyPerson.java:72: 警告: The prover cannot establish an assertion (Postcondition: .Unit3Homework1srccomoocoursespec1mainPerson.java:52: 注: ) in method queryValue
return acquaintance.getOrDefault(person, 0);
^
.Unit3Homework1srccomoocoursespec1mainPerson.java:52: 警告: Associated declaration: .Unit3Homework1srccomoocourseimplements1MyPerson.java:72: 注:
@ ensures (exists int i; 0 <= i && i < acquaintance.length;
^

Runtime Assertion Checking

本功能主要对按照JML编写的程序进行简单的运行时检查。

在IDEA的External Tools中，运行如下命令：java -jar openjml.jar -rac "$FilePath$" -cp "$Classpath$" -sourcepath "$Sourcepath$" -encoding utf-8，即可进行JML程序的运行时检查。-rac参数指定检查类型为Runtime Assertion Checking。

OpenJML在对MyPerson检查的过程中触发了Internal JML bug，并抛出了NullPointerException；在对MyNetwork检查的过程中报错：An internal JML error occurred。由此可见，该功能还不甚完善。

JMLUnitNG测试（针对MyGroup类）

首先将OpenJML中的jmlruntime.jar复制到环境变量CLASSPATH所在的目录下，然后，在项目目录下，运行如下命令：java -jar jmlunitng-1_4.jar -d . est .src即可生成测试类。

对于MyGroup类的测试，可以直接运行MyGroup_JML_Test类中的main方法，得到结果如下：

[TestNG] Running:
Command line suite

Failed: racEnabled()
Passed: constructor MyGroup(-2147483648)
Passed: constructor MyGroup(0)
Passed: constructor MyGroup(2147483647)
Failed: <com.oocourse.implements3.MyGroup@8000001f>.addPerson(null)
Failed: <com.oocourse.implements3.MyGroup@1f>.addPerson(null)
Failed: <com.oocourse.implements3.MyGroup@8000001e>.addPerson(null)
Passed: <com.oocourse.implements3.MyGroup@8000001f>.addRelation(-2147483648)
Passed: <com.oocourse.implements3.MyGroup@1f>.addRelation(-2147483648)
Passed: <com.oocourse.implements3.MyGroup@8000001e>.addRelation(-2147483648)
Passed: <com.oocourse.implements3.MyGroup@8000001f>.addRelation(0)
Passed: <com.oocourse.implements3.MyGroup@1f>.addRelation(0)
Passed: <com.oocourse.implements3.MyGroup@8000001e>.addRelation(0)
Passed: <com.oocourse.implements3.MyGroup@8000001f>.addRelation(2147483647)
Passed: <com.oocourse.implements3.MyGroup@1f>.addRelation(2147483647)
Passed: <com.oocourse.implements3.MyGroup@8000001e>.addRelation(2147483647)
Failed: <com.oocourse.implements3.MyGroup@8000001f>.delPerson(null)
Failed: <com.oocourse.implements3.MyGroup@1f>.delPerson(null)
Failed: <com.oocourse.implements3.MyGroup@8000001e>.delPerson(null)
Passed: <com.oocourse.implements3.MyGroup@8000001f>.equals(null)
Passed: <com.oocourse.implements3.MyGroup@1f>.equals(null)
Passed: <com.oocourse.implements3.MyGroup@8000001e>.equals(null)
Passed: <com.oocourse.implements3.MyGroup@8000001f>.equals(java.lang.Object@61baa894)
Passed: <com.oocourse.implements3.MyGroup@1f>.equals(java.lang.Object@b065c63)
Passed: <com.oocourse.implements3.MyGroup@8000001e>.equals(java.lang.Object@768debd)
Passed: <com.oocourse.implements3.MyGroup@8000001f>.getAgeMean()
Passed: <com.oocourse.implements3.MyGroup@1f>.getAgeMean()
Passed: <com.oocourse.implements3.MyGroup@8000001e>.getAgeMean()
Passed: <com.oocourse.implements3.MyGroup@8000001f>.getAgeVar()
Passed: <com.oocourse.implements3.MyGroup@1f>.getAgeVar()
Passed: <com.oocourse.implements3.MyGroup@8000001e>.getAgeVar()
Passed: <com.oocourse.implements3.MyGroup@8000001f>.getConflictSum()
Passed: <com.oocourse.implements3.MyGroup@1f>.getConflictSum()
Passed: <com.oocourse.implements3.MyGroup@8000001e>.getConflictSum()
Passed: <com.oocourse.implements3.MyGroup@8000001f>.getId()
Passed: <com.oocourse.implements3.MyGroup@1f>.getId()
Passed: <com.oocourse.implements3.MyGroup@8000001e>.getId()
Passed: <com.oocourse.implements3.MyGroup@8000001f>.getPeopleSum()
Passed: <com.oocourse.implements3.MyGroup@1f>.getPeopleSum()
Passed: <com.oocourse.implements3.MyGroup@8000001e>.getPeopleSum()
Passed: <com.oocourse.implements3.MyGroup@8000001f>.getRelationSum()
Passed: <com.oocourse.implements3.MyGroup@1f>.getRelationSum()
Passed: <com.oocourse.implements3.MyGroup@8000001e>.getRelationSum()
Passed: <com.oocourse.implements3.MyGroup@8000001f>.getValueSum()
Passed: <com.oocourse.implements3.MyGroup@1f>.getValueSum()
Passed: <com.oocourse.implements3.MyGroup@8000001e>.getValueSum()
Passed: <com.oocourse.implements3.MyGroup@8000001f>.hasPerson(null)
Passed: <com.oocourse.implements3.MyGroup@1f>.hasPerson(null)
Passed: <com.oocourse.implements3.MyGroup@8000001e>.hasPerson(null)
Passed: <com.oocourse.implements3.MyGroup@8000001f>.hashCode()
Passed: <com.oocourse.implements3.MyGroup@1f>.hashCode()
Passed: <com.oocourse.implements3.MyGroup@8000001e>.hashCode()

===============================================
Command line suite
Total tests run: 52, Failures: 7, Skips: 0

===============================================

Process finished with exit code 0

可以看出，JMLUnitNG主要针对边界数据和空引用进行了测试。在上面的测试中，主要由于方法传入null而失败。而由于本单元作业中，方法不会传入null，因此在代码中未进行处理。

作业架构分析

在本单元的作业中，我主要依据JML进行构建，同时采取一些实现上的优化，如应用容器和算法等。在本单元，我没有进行过多的抽象，仅仅是编写了Pair和SegmentTree工具类，并在MyNetwork类中编写了Dijkstra和PointBiconnectedComponent内部类进行算法的封装。我认为若能将Graph类和Node类抽象出来，并使MyNetwork类和MyPerson类对其分别进行继承或组合，或许可以收到更好的效果。

下面是本单元第三次作业的UML类图（略去了官方包）：

作业Bug情况

本单元作业未在公测和互测中出现任何bug。

在第二次作业中，我在本地测试时发现Group中的getAgeVar方法在使用方差公式简化计算时，若将括号中的项提取出来，可能会导致误差，如下：

public int getAgeVar() {
    if (people.isEmpty()) {
        return 0;
    }
    return (ageSquaredSum - 2 * getAgeMean() * ageSum) / people.size()
            + getAgeMean() * getAgeMean();
}

需要改成如下写法：

public int getAgeVar() {
    if (people.isEmpty()) {
        return 0;
    }
    return (ageSquaredSum - 2 * getAgeMean() * ageSum
            + getAgeMean() * getAgeMean() * people.size()) / people.size();
}

经验证，原因是Java整数除法在取整时，采取向0取整的方式，而前面写法的括号中可能会出现负数，导致舍入错误，而与正确结果差1。

心得体会：规格撰写与理解

在本单元，我接触了一种全新的程序设计模式：规格化设计。规格化设计能够使得设计与实现分离，同时，形式化的规格也便于进行严格的形式化验证。

在撰写规格时，我们会更多地从需求而非实现的角度去思考程序的设计。此外，规格的前置条件会促使我们考虑各种边界条件与极端数据，一定程度上缓解了由于前置条件考虑不周而导致程序出现Bug的现象。

在理解规格时，重点是对规格行为的理解。通常情况下，规格描述并不适合直接作为代码实现。因此，我们需要对规格所描述的行为进行理解，并由此选择合适的实现。我们甚至还可以在规格的基础上进一步抽象，设计出更加清晰合理的程序架构。

虽然如此严格而繁琐的形式化规格表述在日常软件的开发领域并不常见，但我相信，由于其可以进行严格的形式化验证，形式化的规格在高可靠性领域一定大有用武之地。