OO 第三单元总结
目录
JML 语言概述
理论基础
JML 的理论基础是按契约设计（Design by Contract）。[1]
Design By Contract (DbC) is a software correctness methodology. It uses preconditions and postconditions to document (or programmatically assert) the change in state caused by a piece of a program. Design by Contract is a trademarked term of Bertrand Meyer and implemented in his Eiffel language as assertions.
按契约设计实际上不是 JML 首创，但是 OO 用到的是 Java，所以 JML 应该是一种比较容易引入的规约语言。首创按契约设计的是 Eiffel 语言，这种语言也普及化了契约式设计的思想。[2]
JML 官方文档给了 JML 的三大组成部分。[3]
The Java Modeling Language (JML) is a behavioral interface specification language that can be used to specify the behavior of Java modules. It combines the design by contract approach of Eiffel and the model-based specification approach of the Larch family of interface specification languages, with some elements of the refinement calculus.
实际上，Larch 语言家族一开始是基于 Hoare 的工作。Hoare 率先提出了前置条件和后置条件的思想，以及 ADT 的思想。但是 Hoare 的工作过于理论，需要程序编写者掌握一定的数学知识。JML 吸收的另一部分，是从 VDM 一类语言中吸收的用基本的数学工具建构规约的思想，但是这也需要数学知识。因此 JML 结合了 Eiffel 内置的规约特性，使得规格更加方便编写。[3:1]
总之，JML 是结合 Hoare 的前置条件、后置条件、ADT 的思想，以及 VDM 语言用预定义的数据类型构造抽象数据类型的思想，同时还有 Eiffel 语言内置规约特性的思想。这三大思想结合在一起，使得 JML 具有理论优美性，也具有实用性。
应用工具链情况
部署 SMT Solver
环境
通过 OpenJML + z3 进行测试。z3 是微软开发的 SMT Solver，开发历史较早、有大公司支持，而且是 OpenJML 自带的 SMT Solver。[4]
OpenJML 在最新版的 JDK 1.8.0_241 下无法运行，需要把 JDK 降级到 1.8.0_102 版本。
z3 使用 OpenJML 自带的版本也可以，也可以去它的 Github 主页下载。[4:1]
运行
通过 /path/to/jdk/bin/java -jar /path/to/openjml.jar -prover z3 -exec /path/to/z3/binary/z3-version -esc /path/to/Source.java 运行。其中对应的路径需要填空。
运行的时候会出现一堆如下提示，似乎可以忽略。
警告: An internal JML error occurred, possibly recoverable. Please report the bug with as much information as you can.
Reason: Last resort loading of extensions
如果需要调试，也可以在运行的命令行参数里加上 -trace -subexpressions。
如果长时间没有响应，可以试试更换 z3 版本。
实际上 -esc 是程序代码静态检查。还有 -check 和 -rac，分别是 JML 语法和运行时检查。
结果
如果失败，会出现如下提示。
警告: The prover cannot establish an assertion (ArithmeticOperationRange) in method ...
如果成功，会没有这种提示。
在主要方法上用 OpenJML 和 SMT Prover 验证
MyPerson 各方法
选择 MyPerson.java 进行验证，在运行时不仅要加上 MyPerson.java，还要加上 Person.java。
MyPerson.java:65: 警告: The prover cannot establish an assertion (ExceptionalPostcondition: Person.java:65: 注: ) in method compareTo
return this.name.compareTo(Objects.requireNonNull(p2).getName());
^
Person.java:65: 警告: Associated declaration: MyPerson.java:65: 注:
@ public normal_behavior
^
TRACE of com.oocourse.spec1.main.MyPerson.compareTo(com.oocourse.spec1.main.Person)
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(java.math.BigInteger.ZERO != null && java.math.BigInteger.ZERO != null) || java.math.BigInteger.ZERO != null
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(java.math.BigInteger.ONE != null && java.math.BigInteger.ONE != null) || java.math.BigInteger.ONE != null
MyPerson.java:68: 注: requires p2 != null;
VALUE: p2 === REF!val!59
VALUE: null === NULL
VALUE: p2 != null === true
MyPerson.java:68: 注: requires o != null;
VALUE: o === REF!val!59
VALUE: null === NULL
VALUE: o != null === true
MyPerson.java:65: 注: return this.name.compareTo(Objects.requireNonNull(p2).getName());
VALUE: this.name === REF!val!41
VALUE: p2 === REF!val!59
VALUE: Objects.requireNonNull(p2) === REF!val!59
VALUE: Objects.requireNonNull(p2).getName() === NULL
VALUE: this.name.compareTo(Objects.requireNonNull(p2).getName()) === ( - 2147483649 )
MyPerson.java:6: 注: PossiblyNullDeReference assertion: THIS != null
MyPerson.java:65: 注: UndefinedCalledMethodPrecondition assertion: _JML_METHODEF__java_util_Objects_requireNonNull_1803(_JML__tmp1078)
MyPerson.java:68: 注: Precondition assertion: _$CPRE__15
MyPerson.java:65: 注: PossiblyNullDeReference assertion: _JML__tmp1101 != null
MyPerson.java:65: 注: Exception thrown by getName()
VALUE: _JML___exceptionCall === REF!val!74
MyPerson.java:68: 注: Terminated with exception
VALUE: _JML___exception === REF!val!74
MyPerson.java:1: 注: signals () false;
MyPerson.java:68: 注: ExceptionalPostcondition assertion: !Pre_16 || false
MyPerson.java:65: 注: Invalid assertion (ExceptionalPostcondition)
: Person.java:65: 注: Associated location
MyPerson.java:65: 警告: The prover cannot establish an assertion (Postcondition: Person.java:66: 注: ) in method compareTo
return this.name.compareTo(Objects.requireNonNull(p2).getName());
^
Person.java:66: 警告: Associated declaration: MyPerson.java:65: 注:
@ ensures
esult == name.compareTo(p2.getName());
^
TRACE of com.oocourse.spec1.main.MyPerson.compareTo(com.oocourse.spec1.main.Person)
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(java.math.BigInteger.ZERO != null && java.math.BigInteger.ZERO != null) || java.math.BigInteger.ZERO != null
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(java.math.BigInteger.ONE != null && java.math.BigInteger.ONE != null) || java.math.BigInteger.ONE != null
MyPerson.java:68: 注: requires p2 != null;
VALUE: p2 === REF!val!54
VALUE: null === NULL
VALUE: p2 != null === true
MyPerson.java:68: 注: requires o != null;
VALUE: o === REF!val!54
VALUE: null === NULL
VALUE: o != null === true
MyPerson.java:65: 注: return this.name.compareTo(Objects.requireNonNull(p2).getName());
VALUE: this.name === REF!val!40
VALUE: p2 === REF!val!54
VALUE: Objects.requireNonNull(p2) === REF!val!54
VALUE: Objects.requireNonNull(p2).getName() === REF!val!58
VALUE: this.name.compareTo(Objects.requireNonNull(p2).getName()) === 1
MyPerson.java:6: 注: PossiblyNullDeReference assertion: THIS != null
MyPerson.java:65: 注: UndefinedCalledMethodPrecondition assertion: _JML_METHODEF__java_util_Objects_requireNonNull_1803(_JML__tmp1078)
MyPerson.java:68: 注: Precondition assertion: _$CPRE__15
MyPerson.java:65: 注: PossiblyNullDeReference assertion: _JML__tmp1101 != null
MyPerson.java:25: 注: UndefinedNullDeReference assertion: !(_JML__tmp1105 && _JML__tmp1101.name != null) || _JML__tmp1111 != null
MyPerson.java:68: 注: UndefinedCalledMethodPrecondition assertion: _$CPRE__17
MyPerson.java:6: 注: PossiblyNullDeReference assertion: _JML__tmp1156 != null
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(_JML__tmp1156.charArray != null && _JML__tmp1102 != null) || _JML__tmp1102 != null
MyPerson.java:68: 注: UndefinedCalledMethodPrecondition assertion: _$CPRE__19
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(_JML__tmp1183 && _JML__tmp1170 != null && _JML__tmp1171 != null && _JML__tmp1170 != null) || _JML__tmp1170 != null
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(_JML__tmp1183 && _JML__tmp1170 != null && _JML__tmp1171 != null && _JML__tmp1170 != null && _JML__tmp1171 != null) || _JML__tmp1171 != null
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(_JML__tmp1183 && _JML__tmp1170 != null && _JML__tmp1171 != null && _JML__tmp1170 != null && _JML__tmp1171 != null && _JML__tmp1170 != null) || _JML__tmp1170 != null
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(_JML__tmp1183 && _JML__tmp1170 != null && _JML__tmp1171 != null && _JML__tmp1170 != null) || _JML__tmp1170 != null
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(_JML__tmp1183 && _JML__tmp1170 != null && _JML__tmp1171 != null && _JML__tmp1171 != null) || _JML__tmp1171 != null
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(_JML__tmp1183 && _JML__tmp1170 != null && _JML__tmp1171 != null && (_$CPRE__20_1_1 && _$CPRE__20_1_2) && (_$CPRE__20_1_3 && _$CPRE__20_1_4 && _$CPRE__20_1_5 && _$CPRE__20_1_6 && _$CPRE__20_1_7) && _JML__tmp1170 != null) || _JML__tmp1170 != null
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(_JML__tmp1183 && _JML__tmp1170 != null && _JML__tmp1171 != null && (_$CPRE__20_1_1 && _$CPRE__20_1_2) && (_$CPRE__20_1_3 && _$CPRE__20_1_4 && _$CPRE__20_1_5 && _$CPRE__20_1_6 && _$CPRE__20_1_7 && _$CPRE__20_1_8) && _JML__tmp1171 != null) || _JML__tmp1171 != null
MyPerson.java:68: 注: UndefinedCalledMethodPrecondition assertion: _$CPRE__20
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(true && (_$CPRE__18_2_1 && _$CPRE__18_2_2) && _JML__tmp1156.charArray != null && _JML__tmp1102 != null) || _JML__tmp1102 != null
MyPerson.java:68: 注: UndefinedCalledMethodPrecondition assertion: _$CPRE__21
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(_JML__tmp1287 && _JML__tmp1274 != null && _JML__tmp1275 != null && _JML__tmp1274 != null) || _JML__tmp1274 != null
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(_JML__tmp1287 && _JML__tmp1274 != null && _JML__tmp1275 != null && _JML__tmp1274 != null && _JML__tmp1275 != null) || _JML__tmp1275 != null
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(_JML__tmp1287 && _JML__tmp1274 != null && _JML__tmp1275 != null && _JML__tmp1274 != null && _JML__tmp1275 != null && _JML__tmp1274 != null) || _JML__tmp1274 != null
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(_JML__tmp1287 && _JML__tmp1274 != null && _JML__tmp1275 != null && _JML__tmp1274 != null) || _JML__tmp1274 != null
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(_JML__tmp1287 && _JML__tmp1274 != null && _JML__tmp1275 != null && _JML__tmp1275 != null) || _JML__tmp1275 != null
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(_JML__tmp1287 && _JML__tmp1274 != null && _JML__tmp1275 != null && (_$CPRE__22_1_1 && _$CPRE__22_1_2) && (_$CPRE__22_1_3 && _$CPRE__22_1_4 && _$CPRE__22_1_5 && _$CPRE__22_1_6 && _$CPRE__22_1_7) && _JML__tmp1274 != null) || _JML__tmp1274 != null
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(_JML__tmp1287 && _JML__tmp1274 != null && _JML__tmp1275 != null && (_$CPRE__22_1_1 && _$CPRE__22_1_2) && (_$CPRE__22_1_3 && _$CPRE__22_1_4 && _$CPRE__22_1_5 && _$CPRE__22_1_6 && _$CPRE__22_1_7 && _$CPRE__22_1_8) && _JML__tmp1275 != null) || _JML__tmp1275 != null
MyPerson.java:68: 注: UndefinedCalledMethodPrecondition assertion: _$CPRE__22
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(_JML__tmp1156.charArray != null && _JML__tmp1102 != null) || _JML__tmp1102 != null
MyPerson.java:68: 注: UndefinedCalledMethodPrecondition assertion: _$CPRE__23
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(true && (_$CPRE__18_3_1 && _$CPRE__18_3_2) && _JML__tmp1156.charArray != null && _JML__tmp1102 != null) || _JML__tmp1102 != null
MyPerson.java:68: 注: UndefinedCalledMethodPrecondition assertion: _$CPRE__24
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(_JML__tmp1156.charArray != null && _JML__tmp1102 != null) || _JML__tmp1102 != null
MyPerson.java:68: 注: UndefinedCalledMethodPrecondition assertion: _$CPRE__25
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(_JML__tmp1156.charArray != null && _JML__tmp1102 != null) || _JML__tmp1102 != null
MyPerson.java:68: 注: UndefinedCalledMethodPrecondition assertion: _$CPRE__26
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(_JML__tmp1455 && _JML__tmp1442 != null && _JML__tmp1443 != null && _JML__tmp1442 != null) || _JML__tmp1442 != null
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(_JML__tmp1455 && _JML__tmp1442 != null && _JML__tmp1443 != null && _JML__tmp1442 != null && _JML__tmp1443 != null) || _JML__tmp1443 != null
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(_JML__tmp1455 && _JML__tmp1442 != null && _JML__tmp1443 != null && _JML__tmp1442 != null && _JML__tmp1443 != null && _JML__tmp1442 != null) || _JML__tmp1442 != null
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(_JML__tmp1455 && _JML__tmp1442 != null && _JML__tmp1443 != null && _JML__tmp1442 != null) || _JML__tmp1442 != null
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(_JML__tmp1455 && _JML__tmp1442 != null && _JML__tmp1443 != null && _JML__tmp1443 != null) || _JML__tmp1443 != null
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(_JML__tmp1455 && _JML__tmp1442 != null && _JML__tmp1443 != null && (_$CPRE__27_1_1 && _$CPRE__27_1_2) && (_$CPRE__27_1_3 && _$CPRE__27_1_4 && _$CPRE__27_1_5 && _$CPRE__27_1_6 && _$CPRE__27_1_7) && _JML__tmp1442 != null) || _JML__tmp1442 != null
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(_JML__tmp1455 && _JML__tmp1442 != null && _JML__tmp1443 != null && (_$CPRE__27_1_1 && _$CPRE__27_1_2) && (_$CPRE__27_1_3 && _$CPRE__27_1_4 && _$CPRE__27_1_5 && _$CPRE__27_1_6 && _$CPRE__27_1_7 && _$CPRE__27_1_8) && _JML__tmp1443 != null) || _JML__tmp1443 != null
MyPerson.java:68: 注: UndefinedCalledMethodPrecondition assertion: _$CPRE__27
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(true && (_$CPRE__18_4_1 && _$CPRE__18_4_2) && _JML__tmp1156.charArray != null && _JML__tmp1102 != null) || _JML__tmp1102 != null
MyPerson.java:68: 注: UndefinedCalledMethodPrecondition assertion: _$CPRE__28
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(true && (_$CPRE__18_4_1 && _$CPRE__18_4_2 && _$CPRE__18_4_3) && _JML__tmp1156.charArray != null && _JML__tmp1102 != null) || _JML__tmp1102 != null
MyPerson.java:68: 注: UndefinedCalledMethodPrecondition assertion: _$CPRE__29
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(_JML__tmp1576 && _JML__tmp1563 != null && _JML__tmp1564 != null && _JML__tmp1563 != null) || _JML__tmp1563 != null
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(_JML__tmp1576 && _JML__tmp1563 != null && _JML__tmp1564 != null && _JML__tmp1563 != null && _JML__tmp1564 != null) || _JML__tmp1564 != null
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(_JML__tmp1576 && _JML__tmp1563 != null && _JML__tmp1564 != null && _JML__tmp1563 != null && _JML__tmp1564 != null && _JML__tmp1563 != null) || _JML__tmp1563 != null
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(_JML__tmp1576 && _JML__tmp1563 != null && _JML__tmp1564 != null && _JML__tmp1563 != null) || _JML__tmp1563 != null
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(_JML__tmp1576 && _JML__tmp1563 != null && _JML__tmp1564 != null && _JML__tmp1564 != null) || _JML__tmp1564 != null
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(_JML__tmp1576 && _JML__tmp1563 != null && _JML__tmp1564 != null && (_$CPRE__30_1_1 && _$CPRE__30_1_2) && (_$CPRE__30_1_3 && _$CPRE__30_1_4 && _$CPRE__30_1_5 && _$CPRE__30_1_6 && _$CPRE__30_1_7) && _JML__tmp1563 != null) || _JML__tmp1563 != null
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(_JML__tmp1576 && _JML__tmp1563 != null && _JML__tmp1564 != null && (_$CPRE__30_1_1 && _$CPRE__30_1_2) && (_$CPRE__30_1_3 && _$CPRE__30_1_4 && _$CPRE__30_1_5 && _$CPRE__30_1_6 && _$CPRE__30_1_7 && _$CPRE__30_1_8) && _JML__tmp1564 != null) || _JML__tmp1564 != null
MyPerson.java:68: 注: UndefinedCalledMethodPrecondition assertion: _$CPRE__30
MyPerson.java:68: 注: Precondition assertion: _$CPRE__18
MyPerson.java:8: 注: NullField assertion: _JML__tmp1677
MyPerson.java:9: 注: NullField assertion: _JML__tmp1681
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(Pre_16 && THIS.name != null && p2 != null) || _JML__tmp1684 != null
MyPerson.java:25: 注: UndefinedNullDeReference assertion: !(_JML__tmp1688 && _JML__tmp1684.name != null) || _JML__tmp1693 != null
MyPerson.java:68: 注: UndefinedCalledMethodPrecondition assertion: _$CPRE__32
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(Pre_16 && THIS.name != null) || _JML__tmp1738 != null
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(Pre_16 && _JML__tmp1738.charArray != null && _JML__tmp1685 != null) || _JML__tmp1685 != null
MyPerson.java:68: 注: UndefinedCalledMethodPrecondition assertion: _$CPRE__34
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(Pre_16 && (_$CPRE__33_2_1 && _$CPRE__33_2_2) && _JML__tmp1738.charArray != null && _JML__tmp1685 != null) || _JML__tmp1685 != null
MyPerson.java:68: 注: UndefinedCalledMethodPrecondition assertion: _$CPRE__36
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(Pre_16 && _JML__tmp1738.charArray != null && _JML__tmp1685 != null) || _JML__tmp1685 != null
MyPerson.java:68: 注: UndefinedCalledMethodPrecondition assertion: _$CPRE__38
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(Pre_16 && (_$CPRE__33_3_1 && _$CPRE__33_3_2) && _JML__tmp1738.charArray != null && _JML__tmp1685 != null) || _JML__tmp1685 != null
MyPerson.java:68: 注: UndefinedCalledMethodPrecondition assertion: _$CPRE__39
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(Pre_16 && _JML__tmp1738.charArray != null && _JML__tmp1685 != null) || _JML__tmp1685 != null
MyPerson.java:68: 注: UndefinedCalledMethodPrecondition assertion: _$CPRE__40
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(Pre_16 && _JML__tmp1738.charArray != null && _JML__tmp1685 != null) || _JML__tmp1685 != null
MyPerson.java:68: 注: UndefinedCalledMethodPrecondition assertion: _$CPRE__41
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(Pre_16 && (_$CPRE__33_4_1 && _$CPRE__33_4_2) && _JML__tmp1738.charArray != null && _JML__tmp1685 != null) || _JML__tmp1685 != null
MyPerson.java:68: 注: UndefinedCalledMethodPrecondition assertion: _$CPRE__43
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(Pre_16 && (_$CPRE__33_4_1 && _$CPRE__33_4_2 && _$CPRE__33_4_3) && _JML__tmp1738.charArray != null && _JML__tmp1685 != null) || _JML__tmp1685 != null
MyPerson.java:68: 注: UndefinedCalledMethodPrecondition assertion: _$CPRE__44
MyPerson.java:68: 注: UndefinedCalledMethodPrecondition assertion: _$CPRE__33
MyPerson.java:68: 注: ensures
esult == name.compareTo(p2.getName());
VALUE:
esult === 1
VALUE: name === REF!val!58
VALUE: p2 === REF!val!54
VALUE: p2.getName() === REF!val!58
VALUE: name.compareTo(p2.getName()) === 0
VALUE:
esult == name.compareTo(p2.getName()) === false
MyPerson.java:65: 注: Invalid assertion (Postcondition)
: Person.java:66: 注: Associated location
警告: An internal JML error occurred, possibly recoverable. Please report the bug with as much information as you can.
Reason: Last resort loading of extensions
MyPerson.java:44: 警告: The prover cannot establish an assertion (ExceptionalPostcondition: openjml.jar(specs/java/lang/Object.jml):72: 注: ) in method equals
return (((Person) obj).getId() == getId());
^
openjml.jar(specs/java/lang/Object.jml):72: 警告: Associated declaration: MyPerson.java:44: 注:
/*@ public normal_behavior
^
TRACE of com.oocourse.spec1.main.MyPerson.equals(java.lang.Object)
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(java.math.BigInteger.ZERO != null && java.math.BigInteger.ZERO != null) || java.math.BigInteger.ZERO != null
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(java.math.BigInteger.ONE != null && java.math.BigInteger.ONE != null) || java.math.BigInteger.ONE != null
MyPerson.java:68: 注: requires obj != null;
MyPerson.java:68: 注: requires this == obj;
MyPerson.java:68: 注: requires obj != null && ypeof(this) == ype(Object);
MyPerson.java:68: 注: requires obj == null;
MyPerson.java:55: 注: requires obj != null;
VALUE: obj === REF!val!19
VALUE: null === NULL
VALUE: obj != null === true
MyPerson.java:41: 注: requires obj != null && obj instanceof Person;
VALUE: obj === REF!val!19
VALUE: null === NULL
VALUE: obj != null === true
VALUE: obj === REF!val!19
VALUE: obj instanceof Person === true
VALUE: obj != null && obj instanceof Person === true
MyPerson.java:55: 注: requires obj != null;
VALUE: obj === REF!val!19
VALUE: null === NULL
VALUE: obj != null === true
MyPerson.java:50: 注: requires obj == null || !(obj instanceof Person);
VALUE: obj === REF!val!19
VALUE: null === NULL
VALUE: obj == null === false
VALUE: obj === REF!val!19
VALUE: obj instanceof Person === true
VALUE: (obj instanceof Person) === true
VALUE: !(obj instanceof Person) === false
VALUE: obj == null || !(obj instanceof Person) === false
MyPerson.java:41: 注: if (!(obj instanceof Person)) ...
VALUE: obj === REF!val!19
VALUE: obj instanceof Person === true
VALUE: (obj instanceof Person) === true
VALUE: !(obj instanceof Person) === false
VALUE: (!(obj instanceof Person)) === false
Condition = false
MyPerson.java:44: 注: return (((Person)obj).getId() == getId());
VALUE: obj === REF!val!19
VALUE: (Person)obj === REF!val!19
VALUE: ((Person)obj) === REF!val!19
VALUE: ((Person)obj).getId() === 0
VALUE: getId() === 0
VALUE: ((Person)obj).getId() == getId() === true
VALUE: (((Person)obj).getId() == getId()) === true
MyPerson.java:44: 注: PossiblyBadCast assertion: obj == null || obj instanceof com.oocourse.spec1.main.Person
MyPerson.java:44: 注: PossiblyNullDeReference assertion: _JML__tmp612 != null
MyPerson.java:44: 注: Exception thrown by getId()
VALUE: _JML___exceptionCall === REF!val!79
MyPerson.java:68: 注: Terminated with exception
VALUE: _JML___exception === REF!val!79
MyPerson.java:1: 注: signals () false;
MyPerson.java:68: 注: ExceptionalPostcondition assertion: !Pre_6 || false
MyPerson.java:44: 注: Invalid assertion (ExceptionalPostcondition)
: openjml.jar(specs/java/lang/Object.jml):72: 注: Associated location
警告: An internal JML error occurred, possibly recoverable. Please report the bug with as much information as you can.
Reason: Last resort loading of extensions
警告: An internal JML error occurred, possibly recoverable. Please report the bug with as much information as you can.
Reason: Last resort loading of extensions
MyPerson.java:36: 警告: The prover cannot establish an assertion (Postcondition: Person.java:24: 注: ) in method getAge
return age;
^
Person.java:24: 警告: Associated declaration: MyPerson.java:36: 注:
//@ ensures
esult == age;
^
TRACE of com.oocourse.spec1.main.MyPerson.getAge()
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(java.math.BigInteger.ZERO != null && java.math.BigInteger.ZERO != null) || java.math.BigInteger.ZERO != null
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(java.math.BigInteger.ONE != null && java.math.BigInteger.ONE != null) || java.math.BigInteger.ONE != null
MyPerson.java:36: 注: return age;
VALUE: age === ( - 2147483039 )
MyPerson.java:8: 注: NullField assertion: _JML__tmp511
MyPerson.java:9: 注: NullField assertion: _JML__tmp515
MyPerson.java:36: 注: ensures
esult == age;
VALUE:
esult === ( - 2147483039 )
VALUE: age === ( - 2147483038 )
VALUE:
esult == age === false
MyPerson.java:36: 注: Invalid assertion (Postcondition)
: Person.java:24: 注: Associated location
警告: An internal JML error occurred, possibly recoverable. Please report the bug with as much information as you can.
Reason: Last resort loading of extensions
MyPerson.java:31: 警告: The prover cannot establish an assertion (Postcondition: Person.java:21: 注: ) in method getCharacter
return character;
^
Person.java:21: 警告: Associated declaration: MyPerson.java:31: 注:
//@ ensures
esult.equals(character);
^
TRACE of com.oocourse.spec1.main.MyPerson.getCharacter()
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(java.math.BigInteger.ZERO != null && java.math.BigInteger.ZERO != null) || java.math.BigInteger.ZERO != null
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(java.math.BigInteger.ONE != null && java.math.BigInteger.ONE != null) || java.math.BigInteger.ONE != null
MyPerson.java:31: 注: return character;
VALUE: character === REF!val!34
MyPerson.java:8: 注: NullField assertion: _JML__tmp353
MyPerson.java:9: 注: NullField assertion: _JML__tmp357
MyPerson.java:34: 注: ensures
esult != null;
VALUE:
esult === REF!val!34
VALUE: null === NULL
VALUE:
esult != null === true
MyPerson.java:30: 注: UndefinedNullDeReference assertion: !(Pre_4 && THIS.character != null) || _JML__tmp362 != null
MyPerson.java:68: 注: UndefinedCalledMethodPrecondition assertion: _$CPRE__3
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(_JML__tmp398 && _JML__tmp361 != null) || _JML__tmp410 != null
MyPerson.java:68: 注: UndefinedCalledMethodPrecondition assertion: _$CPRE__4
MyPerson.java:30: 注: ensures
esult.equals(character);
VALUE:
esult === REF!val!34
VALUE: character === REF!val!31
MyPerson.java:31: 注: Invalid assertion (Postcondition)
: Person.java:21: 注: Associated location
警告: An internal JML error occurred, possibly recoverable. Please report the bug with as much information as you can.
Reason: Last resort loading of extensions
MyPerson.java:21: 警告: The prover cannot establish an assertion (Postcondition: Person.java:15: 注: ) in method getId
return id;
^
Person.java:15: 警告: Associated declaration: MyPerson.java:21: 注:
//@ ensures
esult == id;
^
TRACE of com.oocourse.spec1.main.MyPerson.getId()
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(java.math.BigInteger.ZERO != null && java.math.BigInteger.ZERO != null) || java.math.BigInteger.ZERO != null
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(java.math.BigInteger.ONE != null && java.math.BigInteger.ONE != null) || java.math.BigInteger.ONE != null
MyPerson.java:21: 注: return id;
VALUE: id === ( - 2147482506 )
MyPerson.java:8: 注: NullField assertion: _JML__tmp158
MyPerson.java:9: 注: NullField assertion: _JML__tmp162
MyPerson.java:20: 注: ensures
esult == id;
VALUE:
esult === ( - 2147482506 )
VALUE: id === ( - 2147482505 )
VALUE:
esult == id === false
MyPerson.java:21: 注: Invalid assertion (Postcondition)
: Person.java:15: 注: Associated location
警告: An internal JML error occurred, possibly recoverable. Please report the bug with as much information as you can.
Reason: Last resort loading of extensions
MyPerson.java:26: 警告: The prover cannot establish an assertion (Postcondition: Person.java:18: 注: ) in method getName
return name;
^
Person.java:18: 警告: Associated declaration: MyPerson.java:26: 注:
//@ ensures
esult.equals(name);
^
TRACE of com.oocourse.spec1.main.MyPerson.getName()
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(java.math.BigInteger.ZERO != null && java.math.BigInteger.ZERO != null) || java.math.BigInteger.ZERO != null
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(java.math.BigInteger.ONE != null && java.math.BigInteger.ONE != null) || java.math.BigInteger.ONE != null
MyPerson.java:26: 注: return name;
VALUE: name === REF!val!36
MyPerson.java:8: 注: NullField assertion: _JML__tmp232
MyPerson.java:9: 注: NullField assertion: _JML__tmp236
MyPerson.java:29: 注: ensures
esult != null;
VALUE:
esult === REF!val!36
VALUE: null === NULL
VALUE:
esult != null === true
MyPerson.java:25: 注: UndefinedNullDeReference assertion: !(Pre_3 && THIS.name != null) || _JML__tmp241 != null
MyPerson.java:68: 注: UndefinedCalledMethodPrecondition assertion: _$CPRE__2
MyPerson.java:25: 注: ensures
esult.equals(name);
VALUE:
esult === REF!val!36
VALUE: name === REF!val!33
MyPerson.java:26: 注: Invalid assertion (Postcondition)
: Person.java:18: 注: Associated location
警告: An internal JML error occurred, possibly recoverable. Please report the bug with as much information as you can.
Reason: Last resort loading of extensions
MyPerson.java:50: 警告: The prover cannot establish an assertion (ExceptionalPostcondition: Person.java:40: 注: ) in method isLinked
throw new UnsupportedOperationException();
^
Person.java:40: 警告: Associated declaration: MyPerson.java:50: 注:
/*@ public normal_behavior
^
TRACE of com.oocourse.spec1.main.MyPerson.isLinked(com.oocourse.spec1.main.Person)
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(java.math.BigInteger.ZERO != null && java.math.BigInteger.ZERO != null) || java.math.BigInteger.ZERO != null
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(java.math.BigInteger.ONE != null && java.math.BigInteger.ONE != null) || java.math.BigInteger.ONE != null
MyPerson.java:68: 注: requires person != null;
VALUE: person === REF!val!25
VALUE: null === NULL
VALUE: person != null === true
MyPerson.java:50: 注: throw new UnsupportedOperationException();
VALUE: new UnsupportedOperationException() === REF!val!103
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(_JML__tmp732 && _JML__tmp728._throwables != null) || _JML__tmp728._throwables != null
MyPerson.java:50: 注: PossiblyNullValue assertion: _JML___NEWOBJECT_1019_723 != null
MyPerson.java:59: 注: Terminated with exception
VALUE: _JML___exception === REF!val!103
MyPerson.java:1: 注: signals () false;
MyPerson.java:59: 注: ExceptionalPostcondition assertion: !Pre_12 || false
MyPerson.java:50: 注: Invalid assertion (ExceptionalPostcondition)
: Person.java:40: 注: Associated location
警告: An internal JML error occurred, possibly recoverable. Please report the bug with as much information as you can.
Reason: Last resort loading of extensions
MyPerson.java:55: 警告: The prover cannot establish an assertion (ExceptionalPostcondition: Person.java:47: 注: ) in method queryValue
throw new UnsupportedOperationException();
^
Person.java:47: 警告: Associated declaration: MyPerson.java:55: 注:
/*@ public normal_behavior
^
TRACE of com.oocourse.spec1.main.MyPerson.queryValue(com.oocourse.spec1.main.Person)
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(java.math.BigInteger.ZERO != null && java.math.BigInteger.ZERO != null) || java.math.BigInteger.ZERO != null
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(java.math.BigInteger.ONE != null && java.math.BigInteger.ONE != null) || java.math.BigInteger.ONE != null
MyPerson.java:68: 注: requires person != null;
VALUE: person === REF!val!25
VALUE: null === NULL
VALUE: person != null === true
MyPerson.java:68: 注: requires (exists int i; 0 <= i && i < acquaintance.length; acquaintance[i].getId() == person.getId());
VALUE: exists int i; 0 <= i && i < acquaintance.length; acquaintance[i].getId() == person.getId() === true
VALUE: (exists int i; 0 <= i && i < acquaintance.length; acquaintance[i].getId() == person.getId()) === true
MyPerson.java:68: 注: requires person != null;
VALUE: person === REF!val!25
VALUE: null === NULL
VALUE: person != null === true
MyPerson.java:68: 注: requires (forall int i; 0 <= i && i < acquaintance.length; acquaintance[i].getId() != person.getId());
VALUE: forall int i; 0 <= i && i < acquaintance.length; acquaintance[i].getId() != person.getId() === false
VALUE: (forall int i; 0 <= i && i < acquaintance.length; acquaintance[i].getId() != person.getId()) === false
MyPerson.java:55: 注: throw new UnsupportedOperationException();
VALUE: new UnsupportedOperationException() === REF!val!105
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(_JML__tmp863 && _JML__tmp859._throwables != null) || _JML__tmp859._throwables != null
MyPerson.java:55: 注: PossiblyNullValue assertion: _JML___NEWOBJECT_1134_854 != null
MyPerson.java:68: 注: Terminated with exception
VALUE: _JML___exception === REF!val!105
MyPerson.java:1: 注: signals () false;
MyPerson.java:68: 注: ExceptionalPostcondition assertion: !Pre_13 || false
MyPerson.java:55: 注: Invalid assertion (ExceptionalPostcondition)
: Person.java:47: 注: Associated location
MyPerson.java:55: 警告: The prover cannot establish an assertion (ExceptionalPostcondition: Person.java:54: 注: ) in method queryValue
throw new UnsupportedOperationException();
^
Person.java:54: 警告: Associated declaration: MyPerson.java:55: 注:
@ public normal_behavior
^
TRACE of com.oocourse.spec1.main.MyPerson.queryValue(com.oocourse.spec1.main.Person)
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(java.math.BigInteger.ZERO != null && java.math.BigInteger.ZERO != null) || java.math.BigInteger.ZERO != null
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(java.math.BigInteger.ONE != null && java.math.BigInteger.ONE != null) || java.math.BigInteger.ONE != null
MyPerson.java:68: 注: requires person != null;
VALUE: person === REF!val!25
VALUE: null === NULL
VALUE: person != null === true
MyPerson.java:68: 注: requires (exists int i; 0 <= i && i < acquaintance.length; acquaintance[i].getId() == person.getId());
VALUE: exists int i; 0 <= i && i < acquaintance.length; acquaintance[i].getId() == person.getId() === false
VALUE: (exists int i; 0 <= i && i < acquaintance.length; acquaintance[i].getId() == person.getId()) === false
MyPerson.java:68: 注: requires person != null;
VALUE: person === REF!val!25
VALUE: null === NULL
VALUE: person != null === true
MyPerson.java:68: 注: requires (forall int i; 0 <= i && i < acquaintance.length; acquaintance[i].getId() != person.getId());
VALUE: forall int i; 0 <= i && i < acquaintance.length; acquaintance[i].getId() != person.getId() === true
VALUE: (forall int i; 0 <= i && i < acquaintance.length; acquaintance[i].getId() != person.getId()) === true
MyPerson.java:55: 注: throw new UnsupportedOperationException();
VALUE: new UnsupportedOperationException() === REF!val!103
MyPerson.java:68: 注: UndefinedNullDeReference assertion: !(_JML__tmp863 && _JML__tmp859._throwables != null) || _JML__tmp859._throwables != null
MyPerson.java:55: 注: PossiblyNullValue assertion: _JML___NEWOBJECT_1134_854 != null
MyPerson.java:68: 注: Terminated with exception
VALUE: _JML___exception === REF!val!103
MyPerson.java:1: 注: signals () false;
MyPerson.java:68: 注: ExceptionalPostcondition assertion: !Pre_13 || false
MyPerson.java:68: 注: ExceptionList assertion: !(_JML___exception instanceof java.lang.Exception) || (!Pre_13 || (false || _JML___exception instanceof java.lang.RuntimeException))
MyPerson.java:68: 注: Terminated with exception
VALUE: _JML___exception === REF!val!103
MyPerson.java:1: 注: signals () false;
MyPerson.java:68: 注: ExceptionalPostcondition assertion: !Pre_14 || false
MyPerson.java:55: 注: Invalid assertion (ExceptionalPostcondition)
: Person.java:54: 注: Associated location
规格中需要修改的地方有以下几点。
Person::compareTo的规格没有考虑p2 == null的情况，需要修改成允许扔出 NPE。Person::isLinked和Person::queryValue可以允许扔异常。
之后运行正常。
修改后的 Person.java 如下。
package com.oocourse.spec1.main;
import java.math.BigInteger;
public interface Person extends Comparable<Person> {
/*@ public instance model non_null int id;
@ public instance model non_null String name;
@ public instance model non_null BigInteger character;
@ public instance model non_null int age;
@ public instance model non_null Person[] acquaintance;
@ public instance model non_null int[] value;
@*/
//@ ensures
esult == id;
public /*@pure@*/ int getId();
//@ ensures
esult.equals(name);
public /*@pure@*/ String getName();
//@ ensures
esult.equals(character);
public /*@pure@*/ BigInteger getCharacter();
//@ ensures
esult == age;
public /*@pure@*/ int getAge();
/*@ also
@ public normal_behavior
@ requires obj != null && obj instanceof Person;
@ assignable
othing;
@ ensures
esult == (((Person) obj).getId() == id);
@ also
@ public normal_behavior
@ requires obj == null || !(obj instanceof Person);
@ assignable
othing;
@ ensures
esult == false;
@*/
public /*@pure@*/ boolean equals(Object obj);
/*@ public normal_behavior
@ assignable
othing;
@ ensures
esult == (exists int i; 0 <= i && i < acquaintance.length;
@ acquaintance[i].getId() == person.getId()) || person.getId() == id;
@*/
public /*@pure@*/ boolean isLinked(Person person);
/*@ public normal_behavior
@ requires (exists int i; 0 <= i && i < acquaintance.length;
@ acquaintance[i].getId() == person.getId());
@ assignable
othing;
@ ensures (exists int i; 0 <= i && i < acquaintance.length;
@ acquaintance[i].getId() == person.getId() &&
esult == value[i]);
@ also
@ public normal_behavior
@ requires (forall int i; 0 <= i && i < acquaintance.length;
@ acquaintance[i].getId() != person.getId());
@ ensures
esult == 0;
@*/
public /*@pure@*/ int queryValue(Person person);
//@ ensures
esult == acquaintance.length;
public /*@pure@*/ int getAcquaintanceSum();
/*@ also
@ public normal_behavior
@ ensures
esult == name.compareTo(p2.getName());
@ public exceptional_behavior
@ signals (NullPointerException e) (p2 == null);
@*/
public /*@pure@*/ int compareTo(Person p2);
}
MyNetwork 各方法
验证时，需要把所有的 Java 源代码都放入命令行参数中。
示例命令如下。
../jdk1.8.0_102/bin/java -jar openjml.jar -prover z3 -exec Solvers-linux/z3-4.3.0 -trace -subexpressions -esc /path/to/src/com/oocourse/spec1/exceptions/*.java
运行日志太长，难以贴出。规格中需要更改的地方有一点：
ensures语句没有实现对其中ot_assigned的静态检查。可以删除这条语句，应该不影响规格的正确性。
之后运行正常。
修改后的 Network.java 如下。
package com.oocourse.spec1.main;
import java.math.BigInteger;
import com.oocourse.spec1.exceptions.EqualPersonIdException;
import com.oocourse.spec1.exceptions.EqualRelationException;
import com.oocourse.spec1.exceptions.PersonIdNotFoundException;
import com.oocourse.spec1.exceptions.RelationNotFoundException;
public interface Network {
/*@ public instance model non_null Person[] people;
@*/
//@ ensures
esult == (exists int i; 0 <= i && i < people.length; people[i].getId() == id);
public /*@pure@*/ boolean contains(int id);
/*@ public normal_behavior
@ requires contains(id);
@ ensures (exists int i; 0 <= i && i < people.length; people[i].getId() == id &&
@
esult == people[i]);
@ also
@ public normal_behavior
@ requires !contains(id);
@ ensures
esult == null;
@*/
public /*@pure@*/ Person getPerson(int id);
/*@ public normal_behavior
@ requires !(exists int i; 0 <= i && i < people.length; people[i].equals(person));
@ assignable people;
@ ensures people.length == old(people.length) + 1;
@ ensures (forall int i; 0 <= i && i < old(people.length);
@ (exists int j; 0 <= j && j < people.length; people[j] == (old(people[i]))));
@ ensures (exists int i; 0 <= i && i < people.length; people[i] == person);
@ also
@ public exceptional_behavior
@ signals (EqualPersonIdException e) (exists int i; 0 <= i && i < people.length;
@ people[i].equals(person));
@*/
public void addPerson(Person person) throws EqualPersonIdException;
/*@ public normal_behavior
@ requires contains(id1) && contains(id2) && id1 != id2 &&
@ !getPerson(id1).isLinked(getPerson(id2));
@ assignable people;
@ ensures people.length == old(people.length);
@ ensures (forall int i; 0 <= i && i < old(people.length);
@ (exists int j; 0 <= j && j < people.length; people[j] == old(people[i])));
@ ensures getPerson(id1).isLinked(getPerson(id2)) && getPerson(id2).isLinked(getPerson(id1));
@ ensures getPerson(id1).queryValue(getPerson(id2)) == value;
@ ensures getPerson(id2).queryValue(getPerson(id1)) == value;
@ ensures (forall int i; 0 <= i && i < old(getPerson(id1).acquaintance.length);
@ old(getPerson(id1).acquaintance[i]) == getPerson(id1).acquaintance[i] &&
@ old(getPerson(id1).value[i]) == getPerson(id1).value[i]);
@ ensures (forall int i; 0 <= i && i < old(getPerson(id2).acquaintance.length);
@ old(getPerson(id2).acquaintance[i]) == getPerson(id2).acquaintance[i] &&
@ old(getPerson(id2).value[i]) == getPerson(id2).value[i]);
@ ensures getPerson(id1).value.length == getPerson(id1).acquaintance.length;
@ ensures getPerson(id2).value.length == getPerson(id2).acquaintance.length;
@ ensures old(getPerson(id1).value.length) == getPerson(id1).acquaintance.length - 1;
@ ensures old(getPerson(id2).value.length) == getPerson(id2).acquaintance.length - 1;
@ also
@ public normal_behavior
@ requires id1 == id2 && contains(id1);
@ assignable
othing;
@ also
@ public exceptional_behavior
@ requires !contains(id1) || !contains(id2) ||
@ (getPerson(id1).isLinked(getPerson(id2)) && id1 != id2);
@ signals (PersonIdNotFoundException e) !contains(id1) || !contains(id2);
@ signals (EqualRelationException e) contains(id1) && contains(id2) &&
@ old(getPerson(id1)).isLinked(old(getPerson(id2)));
@*/
public void addRelation(int id1, int id2, int value) throws
PersonIdNotFoundException, EqualRelationException;
/*@ public normal_behavior
@ requires contains(id1) && contains(id2) && getPerson(id1).isLinked(getPerson(id2));
@ ensures
esult == getPerson(id1).queryValue(getPerson(id2));
@ also
@ public exceptional_behavior
@ signals (PersonIdNotFoundException e) !contains(id1) || !contains(id2);
@ signals (RelationNotFoundException e) contains(id1) && contains(id2) &&
@ !getPerson(id1).isLinked(getPerson(id2));
@*/
public /*@pure@*/ int queryValue(int id1, int id2) throws
PersonIdNotFoundException, RelationNotFoundException;
/*@ public normal_behavior
@ requires contains(id1) && contains(id2);
@ ensures
esult.equals(getPerson(id1).getCharacter().xor(getPerson(id2).getCharacter()));
@ also
@ public exceptional_behavior
@ signals (PersonIdNotFoundException e) !contains(id1) || !contains(id2);
@*/
public /*@pure@*/ BigInteger queryConflict(int id1, int id2) throws PersonIdNotFoundException;
/*@ public normal_behavior
@ requires contains(id);
@ ensures
esult == getPerson(id).getAcquaintanceSum();
@ also
@ public exceptional_behavior
@ signals (PersonIdNotFoundException e) !contains(id);
@*/
public /*@pure@*/ int queryAcquaintanceSum(int id) throws PersonIdNotFoundException;
/*@ public normal_behavior
@ requires contains(id1) && contains(id2);
@ ensures
esult == getPerson(id1).getAge() - getPerson(id2).getAge();
@ also
@ public exceptional_behavior
@ signals (PersonIdNotFoundException e) !contains(id1) || !contains(id2);
@*/
public /*@pure@*/ int compareAge(int id1, int id2) throws PersonIdNotFoundException;
/*@ public normal_behavior
@ requires contains(id1) && contains(id2);
@ ensures
esult == getPerson(id1).getName().compareTo(getPerson(id2).getName());
@ also
@ public exceptional_behavior
@ signals (PersonIdNotFoundException e) !contains(id1) || !contains(id2);
@*/
public /*@pure@*/ int compareName(int id1, int id2) throws PersonIdNotFoundException;
//ensures
esult == people.length;
public /*@pure@*/ int queryPeopleSum();
/*@ public normal_behavior
@ requires contains(id);
@ ensures
esult == (sum int i; 0 <= i && i < people.length &&
@ compareName(id, people[i].getId()) > 0; 1) + 1;
@ also
@ public exceptional_behavior
@ signals (PersonIdNotFoundException e) !contains(id);
@*/
public /*@pure@*/ int queryNameRank(int id) throws PersonIdNotFoundException;
/*@ public normal_behavior
@ requires contains(id1) && contains(id2);
@ ensures
esult == (exists Person[] array; array.length >= 2;
@ array[0].equals(getPerson(id1)) &&
@ array[array.length - 1].equals(getPerson(id2)) &&
@ (forall int i; 0 <= i && i < array.length - 1;
@ array[i].isLinked(array[i + 1]) == true));
@ also
@ public exceptional_behavior
@ signals (PersonIdNotFoundException e) !contains(id1) || !contains(id2);
@*/
public /*@pure@*/ boolean isCircle(int id1, int id2)throws PersonIdNotFoundException;
}
两大工具的逻辑
可以看出，验证的逻辑有以下几个特点。
- 无法验证和没有实现验证的语句会报错。
- 失败会有连锁反应。
Person::compareTo方法的失败，导致之后上层调用的方法失败。 - 不考虑方法有意不实现的情况。如果直接扔出
UnsupportedOperationException会出错。 - 如果 JML 不规定，就不考虑异常情况，但在验证的过程中会考虑异常情况。
- 通过自带的标准库的 JML 进行验证。
部署 JMLUnitNG
环境
JMLUnitNG 的 Github 页面上似乎没有它的编译好的 JAR，需要到它的官方网站下载。[5][6]
下载以后，用 JDK 1.8.0_241 运行。
使用如下命令。
/path/to/jdk/bin/java -jar /path/to/jmlunitng.jar --verbose {Person,MyPerson,Group,MyGroup}.java -cp .
其中 --verbose 可以去掉。-cp 加入是为了避免如下错误信息。
JMLUnitNG exited because of an irrecoverable error:
org.jmlspecs.jmlunitng.JMLUnitNGError: Encountered 98 compilation errors:
openjml: -cp需要参数
用法: openjml <options> <source files>
-help 用于列出可能的选项
运行
运行时出现若干错误，比较明显的是如下错误。
MyGroup.java:78: 错误: 需要')'
graph[realPersonId].forEachOrdered((linkedRealPersonId, weight) -> {
猜测是不支持 lambda 表达式。因此把所有与 lambda 表达式相关的代码暂时改写。
实际上根本原因是 OpenJML 也不支持 lambda 表达式和钻石操作符，但之后实测支持了。[7]JMLUnitNG 可能因为更新较晚，所以支持不好。
改写后测试生成通过。
测试用例和数据分析
通过分析生成出来的文件，可以看出具体生成的测试用例和数据，在 *_JML_Data 中。其余的代码大都是胶水代码，是配合 OpenJML RAC 等动态检查器使用的。从 *_JML_Test.java 中也能看出来这一点。
jmlunitng.jar 内部实际上也有不同的生成策略，有些时候是靠内置策略生成的。
通过自动生成的测试用例和数据可以看出，测试数据的覆盖率很好，在测试极端情况和边界情况时比较充分。生成的数据不少都是在测试极端情况和溢出情况。而且，生成的测试数据重视规格、由规格产生，同时又由规格检验。
比如 Group::getAgeVar 方法，规格如下。
/*@ ensures
esult == (people.length == 0? 0 : ((sum int i; 0 <= i && i < people.length;
@ (people[i].getAge() - getAgeMean()) * (people[i].getAge() - getAgeMean())) /
@ people.length));
@*/
JMLUnitNG 就会生成覆盖规格两个分支的代码，不仅让组内成员数 >0，还让组内成员数 =0。
但是，JMLUnitNG 生成的数据缺乏通用性，进一步导致测试覆盖率可能不够。而且它的考虑不细致，想法没有特别深入。比如同样的方法，应该测试组内成员数在 >0 和 =0 之间不断变化的情况，它并没有测试。
总的来看，它还是一个重要的测试辅助工具。
架构设计梳理
概述
三次作业都采用的是以 Network 为中心的架构，以 Network 为中心维护数据。
数据结构除了标准库里的，都封装成独立的类，放在 util 包里。
模型构建策略
通过操作与模型对应的方式，梳理模型构建策略，如下表。
| 操作 | 意义 | 对应模型 |
|---|---|---|
add_personquery_conflictcompare_agecompare_namequery_people_sum |
添加人、查询对应信息、比较年龄、比较名字、查询人的个数 | 映射 |
add_relationquery_valuequery_acquatintance_sum |
添加关系、查询关系权重、查询一个节点关系数、知道两个人之间是否有关系构成的路径 | 无向图 |
query_circle |
查询两个人之间通过关系是否能形成路径 | 并查集 |
query_name_rank |
知道名字在其集合中的次序 | 能够获取元素次序的集合 |
add_group |
添加组 | 映射 |
add_to_groupdel_from_group |
把人添加到组，把人从组中删除 | 集合 |
query_group_sumquery_group_people_sumquery_group_relation_sumquery_group_value_sumquery_group_conflict_sumquery_group_age_meanquery_group_age_var |
查询组内的各种信息 | 缓存 |
query_age_sum |
查询某个年龄区间里的和 | 集合区间和 |
query_min_path |
查询两个人之间关系权重之和最小的路径 | 无向图的最短路径 |
query_strong_linked |
查询两个人之间是否有两条路径，两条路径包括的人的集合除这两人外不能相同 | 无向图的点双连通分量 |
query_block_sum |
查询图中有多少个块，块内能够通过关系连通，块外不连通 | 无向图的连通块个数 |
borrow_from query_money |
借钱和查询钱 | 映射 |
数据结构
| 模型 | 数据结构 | 实现细节 | 原因 |
|---|---|---|---|
| 映射 | 整数到整数的哈希表 | 通过质数再散列法解决冲突 | 本单元的映射都是整数到整数的映射； 开整数数组且用质数再散列法效率较高且抗碰撞； 方便对人和组的离散化 |
| 图 | 邻接矩阵 | boolean 二维数组 |
对人离散化后时间和空间代价都比较小 |
| 图 | 边权 | int 二维数组 |
同上 |
| 图 | 邻接表 | 动态申请存储空间的 AVL 树，一条无向边表示成两条有向边 | 为了遍历的次序稳定性和较小的遍历代价，对有向边的出点进行排序； 动态申请存储空间，避免第二次作业 10 万条数据加边超时的问题； AVL 树比较好写而且不会被特殊数据卡； 可以按照线性复杂度对一个节点的所有邻居进行遍历 |
| 并查集 | 数组实现并查集 | 按秩合并 | 最坏复杂度有保障[8] |
| 能够获取元素次序的集合 | Order Statistic Tree | 维护节点 size 和 count 信息的 AVL 树，带字符串到节点的缓存 |
AVL 树比较好写而且不会被特殊数据卡； 带字符串到节点的缓存保证加入字符串的时间代价较小，且通常情况下只需要比较一次 |
| 集合 | 桶 | boolean 数组 |
对人离散化后时间和空间代价都比较小 |
| 缓存 | N/A | 见下节 | 缓存可以使组查询的复杂度降到常数级别，把复杂的修改操作均摊 |
| 集合区间和 | 线段树 | 限定范围为 $ left[ 0,2000 ight] $ | 加入和查询的时间复杂度都是对数级别； 不会被特殊数据卡 |
| 图的最短路径 | Dijkstra | 采用 min heap 进行堆优化 | 复杂度比较正常，不会太高； 其它堆不好写而且常数不一定小[9] |
| 图的点双连通分量 | Tarjan | 对当前连通分量进行特判，找到一个至少 3 个点的连通分量且包括源点和目的点就退出 | 复杂度比较正常，不会太高 |
| 图的连通块个数 | 数组实现并查集 | 复用原来的并查集，在添加新节点时加一个连通块，在合并时如果根不一致就减少一个连通块 | 常数复杂度 |
缓存机制
| 缓存 | 更新时机 | 更新操作 |
|---|---|---|
| 组内人数 | 添加人 | +1 |
| 组内人数 | 删除人 | -1 |
| 组内关系和 | 添加人 | +2，然后遍历该人在图中的所有邻居，如果邻居也在该组内，就增加 2 |
| 组内关系和 | 删除人 | -2，然后遍历该人在图中的所有邻居，如果邻居也在该组内，就减少 2 |
| 组内关系权值和 | 添加人 | 遍历该人在图中的所有邻居，如果邻居也在该组内，就增加对应边的权值的两倍 |
| 组内关系权值和 | 删除人 | 遍历该人在图中的所有邻居，如果邻居也在该组内，就减少对应边的权值的两倍 |
| 组内冲突和 | 添加人 | 异或上该人的性格 |
| 组内冲突和 | 删除人 | 异或上该人的性格 |
| 组内年龄和 | 添加人 | 加上该人的年龄 |
| 组内年龄和 | 删除人 | 减去该人的年龄 |
| 组内年龄平方和 | 添加人 | 加上该人的年龄平方 |
| 组内年龄平方和 | 删除人 | 减去该人的年龄平方 |
方差计算
通过以下公式进行计算。
$ n V = sum_{i} (a_i - ar{a})^2 = sum_{i} (a_i^2 - 2 a_i ar{a} + ar{a}^2) = sum_{i} a_i^2 - 2 ar{a} sum_{i} a_i + sum_{i} ar{a}^2 = sum_{i} a_i^2 - 2 ar{a} sum_{i} a_i + n ar{a}^2 $
因此只需要缓存组内年龄和和组内年龄平方和。
注意整数除法需要放到最后做。
因为在 overflow arithmetic 下，int 形成一个环，所以直接加且不考虑溢出的行为是可以的。[10]
最大方差是 $ frac{c^2}{4} $，其中 $ c = 2000 $。[11]
性能分析
由于使用了比较高效的数据结构，三次作业没有遇到太大的性能问题。
一个性能瓶颈是 del_from_group 的时候，不需要真正更新，可以把组更改的日志记下来。但是这也是一种空间换时间的做法，实现难度略微有点大，就没有实现。
Bug 及其修复情况
一共出现了两个 bug，都是第一次作业的 bug。
首先是 Network::queryValue 没有考虑 id1 == id2 的情况，直接导致输出错误。
然后是没有考虑人有重名的情况，一开始没在 order statistic tree 里加入 count 域表示同样的字符串有几个。
在之后的作业里，通过认真阅读规格、做好单元测试的方法，修复了 bug。这也是一种教训。
心得体会
撰写规格
实际上规格虽然看起来很形式化、很抽象，也是有规律可循的。撰写规格和编写代码一样，都需要注重层次化、逻辑、良好的理解性等方面。同时，规格和容器、specification pattern 结合，也能总结出不少有用的设计模式，使规格撰写本身系统化。
理解规格
规格体现了按照契约设计的思想，是避免自然语言二义性、准确指导软件开发的良好形式。通过规格，可以打破康威定律，明确各个部分的权利和义务，也能推动软件开发的良好进展。[12]同时，也可以通过规格进行形式化验证。[13]
参考文献
https://en.wikipedia.org/wiki/Eiffel_(programming_language) ↩︎
http://www.eecs.ucf.edu/~leavens/JML//refman/jmlrefman.pdf ↩︎ ↩︎
http://insttech.secretninjaformalmethods.org/software/jmlunitng/release_history.html ↩︎
https://www.luogu.com.cn/blog/Atalod/shi-jian-fu-za-du-shi-neng-fen-xi-qian-tan ↩︎
https://en.wikipedia.org/wiki/Fibonacci_heap#Practical_considerations ↩︎
https://stackoverflow.com/questions/30178301/do-c-sharp-and-java-longs-form-a-commutative-ring ↩︎
https://stats.stackexchange.com/questions/350270/what-are-the-minimum-and-maximum-values-of-variance ↩︎