面向对象第三单元总结 - JML(Java Modeling Language) - 简体版本

一、JML 理论基础 与 应用工具链

1.1 JML 理论基础

JML(Java Modeling Language)是用于对Java程序进行规格化设计的一种表示语言。JML是一种行为接口规格语言(Behavior Interface Specification Language, BISL)，基于Larch方法构建。BISL提供了对方法和类型的规格定义手段。所谓接口即一个方法或类型外部可见的内容。

以上文字摘自课程组下发的JML(Level 0)使用手册。

1.2 JML应用工具链

1.2.1 OpenJML

OpenJML is a program verification tool for Java programs that allows you to check the specifications of programs annotated in the Java Modeling Language.

OpenJML是可用于Java程序的程序验证工具，它可以检查使用JML(Java Modeling Language)语言进行注释的程序的正确性。它支持静态的检查，也支持运行时检查。此外它还集成了一些SMT Solvers，便于对程序进行更深层次的验证。

1.2.2 JMLUnitNG/JMLUnit

JMLUnitNG is an automated unit test generation tool for JML-annotated Java code, including code using Java 1.5+ features such as generics, enumerated types, and enhanced for loops. Like the original JMLUnit, it uses JML assertions as test oracles. It improves upon the original JMLUnit by allowing easy customization of data to be used for each method parameter of a class under test, as well as by using Java reflection to automatically generate test data of non-primitive types.

JMLUnitNG是JMLUnit的进阶版本，全称为JMLUnit Next Generation。JMLUnitNG是用于带有JML注释的Java代码的自动化单元测试生成工具，包括使用Java 1.5+特性(例如泛型，枚举类型和增强的for循环)的代码。 像原始的JMLUnit一样，它使用JML断言作为测试。 它通过允许对要测试的类的每个方法参数轻松地自定义数据，以及使用Java反射自动生成非原始类型的测试数据，对原始JMLUnit进行了改进。

JMLUnitNG最近更新于2014年，年代久远，用起来也不是很方便。

二、JMLUnitNG/JMLUnit部署

JMLUnitNG的部署恐怕是最难的地方了。说实话，看到大家在使用过程中各种报错，我甚至想像某学长“遂放弃”一样结束这一部分。但是后来我自己尝试了一下，发现还是可以正常使用的。正常使用之前需要先做如下几个工作：

使用jdk8。

将整个文件树复製到工作目录下test文件夹，并将所有的java文件开头加上package test;或在已有package前加上test.(如package test.com.oocourse .spec3.main;)。

将Group.java中所有的JML代码复制到MyGroup.java中相对应的地方，还需要将所有的@Override删掉。

将JML中的变量名与Java程序中的变量名修改，使其不会重名。我使用了VSCode对于Java代码的批量重命名功能，将Java代码中的变量名进行了修改。修改JML变量名有点麻烦。

在构造方法中，对HashMap的new操作显式指出HashMap的键值对类型。如this.peopleMap = new HashMap();。如果不这样做的话，在使用JMLUnitNG时会有如下报错(以及一大堆警告，此处略去)：

C:\Users\NBao\jml>java -jar jmlunitng.jar test\MyGroup.java

JMLUnitNG exited because of an irrecoverable error:

org.jmlspecs.jmlunitng.JMLUnitNGError: Encountered 2 compilation errors:

C:\Users\NBao\jml\test\MyGroup.java:23: error: illegal start of type

this.peopleMap = new HashMap<>();

^

warning: ...

最后我的MyGroup.java是这样的内容：

package test;

import test.com.oocourse.spec3.main.Group;

import test.com.oocourse.spec3.main.Person;

import java.math.BigInteger;

import java.util.HashMap;

public class MyGroup implements Group {

/*@ public instance model non_null int id;

@ public instance model non_null Person[] people;

@*/

private final int idNum;

private final HashMap peopleMap;

private int relationSum;

private int valueSum;

private BigInteger conflictSum;

private int ageSum;

private int ageSumSquare;

public MyGroup(int id) {

this.idNum = id;

this.peopleMap = new HashMap();

this.relationSum = 0;

this.valueSum = 0;

this.conflictSum = BigInteger.ZERO;

this.ageSum = 0;

this.ageSumSquare = 0;

}

//@ ensures \result == id;

public /*@pure@*/ int getId() {

return idNum;

}

/*@ also

@ public normal_behavior

@ requires obj != null && obj instanceof Group;

@ assignable \nothing;

@ ensures \result == (((Group) obj).getId() == id);

@ also

@ public normal_behavior

@ requires obj == null || !(obj instanceof Group);

@ assignable \nothing;

@ ensures \result == false;

@*/

public /*@pure@*/ boolean equals(Object obj) {

if (!(obj instanceof Group)) {

return false;

}

return ((Group) obj).getId() == idNum;

}

public void addPerson(Person person) {

for (Person p : peopleMap.values()) {

if (p.isLinked(person)) {

relationSum += 2;

valueSum += 2 * p.queryValue(person);

}

}

relationSum++;

conflictSum = conflictSum.xor(person.getCharacter());

ageSum += person.getAge();

ageSumSquare += person.getAge() * person.getAge();

peopleMap.put(person.getId(), person);

}

//@ ensures \result == (\exists int i; 0 <= i && i < people.length; people[i].equals(person));

public /*@pure@*/ boolean hasPerson(Person person) {

return peopleMap.containsKey(person.getId());

}

/*@ ensures \result == (\sum int i; 0 <= i && i < people.length;

@ (\sum int j; 0 <= j && j < people.length && people[i].isLinked(people[j]); 1));

@*/

public /*@pure@*/ int getRelationSum() {

return relationSum;

}

/*@ ensures \result == (\sum int i; 0 <= i && i < people.length;

@ (\sum int j; 0 <= j && j < people.length &&

@ people[i].isLinked(people[j]); people[i].queryValue(people[j])));

@*/

public /*@pure@*/ int getValueSum() {

return valueSum;

}

/*@ public normal_behavior

@ requires people.length > 0;

@ ensures (\exists BigInteger[] temp;

@ temp.length == people.length && temp[0] == people[0].getCharacter();

@ (\forall int i; 1 <= i && i < temp.length;

@ temp[i] == temp[i-1].xor(people[i].getCharacter())) &&

@ \result == temp[temp.length - 1]);

@ also

@ public normal_behavior

@ requires people.length == 0;

@ ensures \result == BigInteger.ZERO;

@*/

public /*@pure@*/ BigInteger getConflictSum() {

return conflictSum;

}

/*@ ensures \result == (people.length == 0? 0 :

@ ((\sum int i; 0 <= i && i < people.length; people[i].getAge()) / people.length));

@*/

public /*@pure@*/ int getAgeMean() {

return peopleMap.size() == 0 ? 0 : ageSum / peopleMap.size();

}

/*@ ensures \result == (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() {

if (peopleMap.size() == 0) {

return 0;

}

int mean = getAgeMean();

int n = peopleMap.size();

return (ageSumSquare + n * mean * mean - 2 * mean * ageSum) / n;

}

public void delPerson(Person person) {

peopleMap.remove(person.getId());

for (Person p : peopleMap.values()) {

if (p.isLinked(person)) {

relationSum -= 2;

valueSum -= 2 * p.queryValue(person);

}

}

relationSum--;

conflictSum = conflictSum.xor(person.getCharacter());

ageSum -= person.getAge();

ageSumSquare -= person.getAge() * person.getAge();

}

public int getSize() {

return peopleMap.size();

}

public void updateLink(int value) {

relationSum += 2;

valueSum += 2 * value;

}

}

此时的目录树是这样的：

C:\Users\NBao\jml>tree /f

Folder PATH listing

Volume serial number is 44BA-9DE9

C:.

│ jmlunitng.jar

│ openjml.jar

│

└─test

│ Dijkstra.java

│ Main.java

│ MyGroup.java

│ MyNetwork.java

│ MyPerson.java

│ Tarjan.java

│ UnionFindSet.java

│

└─com

└─oocourse

└─spec3

├─exceptions

│ EqualGroupIdException.java

│ EqualPersonIdException.java

│ EqualRelationException.java

│ GroupIdNotFoundException.java

│ PersonIdNotFoundException.java

│ RelationNotFoundException.java

│

└─main

Group.java

Network.java

Person.java

Runner.java

依次执行以下四条指令：

java -jar jmlunitng.jar test/MyGroup.java

javac -cp jmlunitng.jar test/*.java

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

java -cp jmlunitng.jar test.MyGroup_JML_Test

得到下面的结果：

Microsoft Windows [Version 10.0.18363.836]

(c) 2019 Microsoft Corporation. 著作權所有，並保留一切權利。

C:\Users\NBao>cd jml

C:\Users\NBao\jml>java -jar jmlunitng.jar test\MyGroup.java

C:\Users\NBao\jml>javac -cp jmlunitng.jar test\*.java

C:\Users\NBao\jml>java -jar openjml.jar -rac test\MyGroup.java

test\MyGroup.java:3: error: package test.com.oocourse.spec3.main does not exist

import test.com.oocourse.spec3.main.Group;

^

test\MyGroup.java:4: error: package test.com.oocourse.spec3.main does not exist

import test.com.oocourse.spec3.main.Person;

^

test\MyGroup.java:9: error: cannot find symbol

public class MyGroup implements Group {

^

symbol: class Group

test\MyGroup.java:11: error: cannot find symbol

@ public instance model non_null Person[] people;

^

symbol: class Person

location: class MyGroup

test\MyGroup.java:14: error: cannot find symbol

private final HashMap peopleMap;

^

symbol: class Person

location: class MyGroup

test\MyGroup.java:54: error: cannot find symbol

public void addPerson(Person person) {

^

symbol: class Person

location: class MyGroup

test\MyGroup.java:70: error: cannot find symbol

public /*@pure@*/ boolean hasPerson(Person person) {

^

symbol: class Person

location: class MyGroup

test\MyGroup.java:125: error: cannot find symbol

public void delPerson(Person person) {

^

symbol: class Person

location: class MyGroup

test\MyGroup.java:23: error: cannot find symbol

this.peopleMap = new HashMap();

^

symbol: class Person

location: class MyGroup

test\MyGroup.java:38: error: cannot find symbol

@ requires obj != null && obj instanceof Group;

^

symbol: class Group

location: class MyGroup

test\MyGroup.java:40: error: cannot find symbol

@ ensures \result == (((Group) obj).getId() == id);

^

symbol: class Group

location: class MyGroup

test\MyGroup.java:43: error: cannot find symbol

@ requires obj == null || !(obj instanceof Group);

^

symbol: class Group

location: class MyGroup

test\MyGroup.java:48: error: cannot find symbol

if (!(obj instanceof Group)) {

^

symbol: class Group

location: class MyGroup

test\MyGroup.java:51: error: cannot find symbol

return ((Group) obj).getId() == idNum;

^

symbol: class Group

location: class MyGroup

test\MyGroup.java:55: error: cannot find symbol

for (Person p : peopleMap.values()) {

^

symbol: class Person

location: class MyGroup

The operation symbol ++ for type java.lang.Object could not be resolved

org.jmlspecs.openjml.JmlInternalError: The operation symbol ++ for type java.lang.Object could not be resolved

at org.jmlspecs.openjml.JmlTreeUtils.findOpSymbol(JmlTreeUtils.java:291)

at org.jmlspecs.openjml.JmlTreeUtils.findOpSymbol(JmlTreeUtils.java:282)

at org.jmlspecs.openjml.JmlTreeUtils.makeUnary(JmlTreeUtils.java:739)

at com.sun.tools.javac.comp.JmlAttr.createRacExpr(JmlAttr.java:4465)

at org.jmlspecs.openjml.ext.QuantifiedExpressions$QuantifiedExpression.typecheck(QuantifiedExpressions.java:214)

at com.sun.tools.javac.comp.JmlAttr.visitJmlQuantifiedExpr(JmlAttr.java:4070)

at org.jmlspecs.openjml.JmlTree$JmlQuantifiedExpr.accept(JmlTree.java:2685)

at com.sun.tools.javac.comp.Attr.attribTree(Attr.java:577)

at com.sun.tools.javac.comp.Attr.visitParens(Attr.java:2995)

at com.sun.tools.javac.tree.JCTree$JCParens.accept(JCTree.java:1661)

at com.sun.tools.javac.comp.Attr.attribTree(Attr.java:577)

at com.sun.tools.javac.comp.Attr.attribExpr(Attr.java:619)

at com.sun.tools.javac.comp.JmlAttr.attribExpr(JmlAttr.java:6209)

at com.sun.tools.javac.comp.JmlAttr.visitJmlMethodClauseExpr(JmlAttr.java:3117)

at org.jmlspecs.openjml.JmlTree$JmlMethodClauseExpr.accept(JmlTree.java:2332)

at com.sun.tools.javac.comp.JmlAttr.visitJmlSpecificationCase(JmlAttr.java:3361)

at org.jmlspecs.openjml.JmlTree$JmlSpecificationCase.accept(JmlTree.java:2837)

at com.sun.tools.javac.comp.JmlAttr.visitJmlMethodSpecs(JmlAttr.java:3423)

at org.jmlspecs.openjml.JmlTree$JmlMethodSpecs.accept(JmlTree.java:2539)

at com.sun.tools.javac.comp.JmlAttr.visitBlock(JmlAttr.java:706)

at com.sun.tools.javac.comp.JmlAttr.visitJmlBlock(JmlAttr.java:3804)

at org.jmlspecs.openjml.JmlTree$JmlBlock.accept(JmlTree.java:1333)

at com.sun.tools.javac.comp.Attr.attribTree(Attr.java:577)

at com.sun.tools.javac.comp.Attr.attribStat(Attr.java:646)

at com.sun.tools.javac.comp.JmlAttr.attribStat(JmlAttr.java:558)

at com.sun.tools.javac.comp.Attr.visitMethodDef(Attr.java:1015)

at com.sun.tools.javac.comp.JmlAttr.visitMethodDef(JmlAttr.java:1112)

at com.sun.tools.javac.comp.JmlAttr.visitJmlMethodDecl(JmlAttr.java:6053)

at org.jmlspecs.openjml.JmlTree$JmlMethodDecl.accept(JmlTree.java:1261)

at com.sun.tools.javac.comp.Attr.attribTree(Attr.java:577)

at com.sun.tools.javac.comp.Attr.attribStat(Attr.java:646)

at com.sun.tools.javac.comp.JmlAttr.attribStat(JmlAttr.java:558)

at com.sun.tools.javac.comp.Attr.attribClassBody(Attr.java:4378)

at com.sun.tools.javac.comp.JmlAttr.attribClassBody(JmlAttr.java:536)

at com.sun.tools.javac.comp.Attr.attribClass(Attr.java:4286)

at com.sun.tools.javac.comp.JmlAttr.attribClass(JmlAttr.java:414)

at com.sun.tools.javac.comp.Attr.attribClass(Attr.java:4215)

at com.sun.tools.javac.comp.Attr.attrib(Attr.java:4190)

at com.sun.tools.javac.main.JavaCompiler.attribute(JavaCompiler.java:1258)

at com.sun.tools.javac.main.JmlCompiler.attribute(JmlCompiler.java:479)

at com.sun.tools.javac.main.JavaCompiler.compile2(JavaCompiler.java:898)

at com.sun.tools.javac.main.JmlCompiler.compile2(JmlCompiler.java:712)

at com.sun.tools.javac.main.JavaCompiler.compile(JavaCompiler.java:867)

at com.sun.tools.javac.main.Main.compile(Main.java:553)

at com.sun.tools.javac.main.Main.compile(Main.java:410)

at org.jmlspecs.openjml.Main.compile(Main.java:581)

at com.sun.tools.javac.main.Main.compile(Main.java:399)

at com.sun.tools.javac.main.Main.compile(Main.java:390)

at org.jmlspecs.openjml.Main.execute(Main.java:417)

at org.jmlspecs.openjml.Main.execute(Main.java:375)

at org.jmlspecs.openjml.Main.execute(Main.java:362)

at org.jmlspecs.openjml.Main.main(Main.java:334)

test\MyGroup.java:128: error: cannot find symbol

for (Person p : peopleMap.values()) {

^

symbol: class Person

location: class MyGroup

16 errors

C:\Users\NBao\jml>java -cp jmlunitng.jar test.MyGroup_JML_Test

[TestNG] Running:

Command line suite

Failed: racEnabled()

Passed: constructor MyGroup(-2147483648)

Passed: constructor MyGroup(0)

Passed: constructor MyGroup(2147483647)

Failed: <>.addPerson(null)

Failed: <>.addPerson(null)

Failed: <>.addPerson(null)

Failed: <>.delPerson(null)

Failed: <>.delPerson(null)

Failed: <>.delPerson(null)

Passed: <>.equals(null)

Passed: <>.equals(null)

Passed: <>.equals(null)

Passed: <>.equals(java.lang.Object@4fccd51b)

Passed: <>.equals(java.lang.Object@60215eee)

Passed: <>.equals(java.lang.Object@65e579dc)

Passed: <>.getAgeMean()

Passed: <>.getAgeMean()

Passed: <>.getAgeMean()

Passed: <>.getAgeVar()

Passed: <>.getAgeVar()

Passed: <>.getAgeVar()

Passed: <>.getConflictSum()

Passed: <>.getConflictSum()

Passed: <>.getConflictSum()

Passed: <>.getId()

Passed: <>.getId()

Passed: <>.getId()

Passed: <>.getRelationSum()

Passed: <>.getRelationSum()

Passed: <>.getRelationSum()

Passed: <>.getSize()

Passed: <>.getSize()

Passed: <>.getSize()

Passed: <>.getValueSum()

Passed: <>.getValueSum()

Passed: <>.getValueSum()

Failed: <>.hasPerson(null)

Failed: <>.hasPerson(null)

Failed: <>.hasPerson(null)

Passed: <>.updateLink(-2147483648)

Passed: <>.updateLink(-2147483648)

Passed: <>.updateLink(-2147483648)

Passed: <>.updateLink(0)

Passed: <>.updateLink(0)

Passed: <>.updateLink(0)

Passed: <>.updateLink(2147483647)

Passed: <>.updateLink(2147483647)

Passed: <>.updateLink(2147483647)

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

Command line suite

Total tests run: 49, Failures: 10, Skips: 0

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

此处运行了49个测试用例，39个通过，10个失败。这其中JMLUnitNG创建了三个MyGroup对象，其id分别为0、-2147483648、2147483647；之后JMLUnitNG分别调用了这三个MyGroup对象的所有方法进行测试。

可以看到，当方法所需参数为int类型时，JMLUnitNG会将0、最大整数和最小整数传入；当方法所需参数为Object子类时，JMLUnitNG会将null传入。这说明JMLUnitNG还是很注重边界条件的测试。不过由于JML规格中的这些方法是与其他方法相互配合的，所以诸如addPerson、delPerson、hasPerson这些方法其实是可以保证传入的对象不是null的，因此这些使用null进行的测试也没有特别大的意义。

总体来说，JMLUnitNG不是很好用，其自动生成的测试随机性不强，检测到代码中真正的遗漏与疏忽的可能性也不是很大。

三、架构设计

3.1 作业1

刚开始接触这一单元的作业时，我以为这一单元的作业就是要严格按照JML规格的要求来写代码，以至于我甚至尝试使用静态数组作为容器实现其功能。后来我意识到实际上规格就是用来表述一种抽象关系，在保证符合规格要求的前提下，使用什么容器都可以。为了最简单地和JML规格相对应，我採用了ArrayList来与规格中的数组相对应，这样在写代码的时候可以直接把规格类似地借鉴下来，最为便捷。现在来看，那个时候我对于JML规格的理解还是TOO YOUNG TOO SIMPLE、SOMETIMES NAIVE。

3.2 作业2

作业2的最高指令数达到了100000条，这很恐怖。对于Group中需要查询的字段，我採取了缓存的方式，避免每次都遍历。另外我发现，对于MyNetwork中要求实现的大部分函数中，在不存在Person ID的时候，就会直接抛出异常。这种情况下，如果采用ArrayList，就需要对整个列表遍歷一遍，时间复杂度很高。因此，我在作业2开展了一项“扫黑除恶”专项行动——将所有的ArrayList这样的黑恶势力替换成HashMap。替换成HashMap的好处在于，查找的复杂度由O(n)变成了O(1)。不过，这就需要我把查找相关的所有代码推倒重写。

如何判断重写的对不对呢？这就需要JUnit大显神通了。在重写之前，我构造了覆盖全面的JUnit测试用例。在重写之后，再次执行JUnit测试，如果原来的样例都可以通过，就说明重写大致没有问题(这取决于测试用例的水平)。说实话，重写之后的程序还真的有一个函数没有通过测试用例。后来发现，抛出异常的前提条件的boolean语句前面少写了一个非运算符!。JUnit真是一个好帮手。

3.3 作业3

作业3，虚假的JML——按照规格写代码；真实的JML——数据结构与算法。说实话这次作业需要考虑性能，新增加的这几个函数要想保证性能较佳，确实需要研究一下算法。这次作业中使用了堆优化的Dijkstra算法、Tarjan算法、并查集数据结构。这些具体的实现我都单独开了一个类，把复杂的代码分散，提高代码可读性。相对来说我还是比较满意这次的架构的。

四、BUG分析

三次作业中，作业3的代码中出现了一个小小的问题。我在周六晚上截止提交之后发现了这一BUG，但是已经无能为力，哭/(ㄒoㄒ)/~~ 。毫无疑问，在互测中，我被Hack了。

这个BUG是Tarjan算法实现上的一个小小的BUG，和dfs到割点之后、下一个即将遍历的节点顺序有关系。当这个割点与要判断是否StrongLinked的两个节点都强连通时，便可能出现判断失误的问题。

算法的具体问题有点过于细节，说实话也不应该作为JML单元的关注点……这次BUG的主要原因还是因为我对Tarjan算法对于无向图的处理理解得不透彻，下学期学算法的时候要好好学习一下。

五、感想

我认为本单元仅仅想要拿到作业分数并不算难，但本单元真正需要思考的却应当是设计与架构方面的问题。对于我的三次作业，前两次作业由于较为简单，因此我的代码中只有继承了三个接口的MyPerson、MyNetwork、MyGroup。第三次作业需要较为复杂的算法，因此我将那些重要的算法都单独分出了一个类，如Dijkstra、Tarjan、UnionFindSet这样三个类。这样将复杂的算法单独分离出来，便于相关算法的维护，也避免了将所有代码堆到MyNetwork中，对于这样的做法我还是比较满意的。不过，对于更深层次的构造问题我没有考虑更多，毕竟实现这些算法就够我花上两三天了。

这个单元我对于规格与代码的区别有了一个较为清晰的认识，也认识到方法的行为是可以从函数中抽象出来单独表示的。虽然之后写JML规格的机会很少，但是在之后写代码的时候至少会在脑海过一遍相关的行为抽象，也会有意识地控制自己写的方法，使其行为的抽象都能较为简单地描述出来。事实上，如果某个方法很难用规格描述，那么就说明这个方法的实现很有可能有较大问题。因此，这一单元的学习对于我之后写代码的影响还是比较大的。