OO第三单元总结

前言

相比于前两个单元，这个单元的代码量小了很多，但是对我们的单元测试能力和对数据结构的理解要求更高了。在完成作业的时候，我们首先需要看懂课程组提供的规格，并按照规格填写函数。完成方法填写之后，我们要学会运用junit来测试我们的程序。

1.JML语言总结

JML（Java Modeling Language）用于描述方法的特征，它可以告诉我们这个方法可以带来什么预期结果，而不去管这个方法具体是如何实现的。这个特征完全符合了面向对象的思想。

理论基础

JML表达式
- 原子表达式
  
  \result
  
  \old()
  
  \not_assigned()
  
  \not_modified()
  
  \nonnullelements()
  
  \type()
  
  \typeof()
- 量化表达式
\forall

　　\exists

　　\sum

　　\product

　　\max

　　\min

　　\num_of
- 操作符
子类型关系操作符 <:

　　等价关系操作符 <==>

　　推理操作符 ==>

　　变量应用 \nothing \everything

方法规格
- 前置条件 reqquires
- 后置条件 ensures
- 副作用范围限定 assignable modifiable
- signals子句

类规格
- 状态变化约束 constraint
- 不变式 invariant

应用工具链

使用openJML工具，可以测试JML语法正确性、方法静态检查和运行时检查。

JML语法检查

封装好openjml指令后，运行openjml -check Add.java即可对Add.java文件进行JML语法检测。这方面严格按照JML语法就不会有问题。

静态检测

举一个简单的例子，三次作业中都对数据进行compare处理，如果我们使用减法就会发生溢出问题。

public class Sub {
      //@ ensures a > b ==> \result > 0;     //@ ensures a < b ==> \result < 0; //@ ensures a == b ==> \result == 0; public static int compare(int a, int b) { return a - b; } public static void main(String[] args) { compare(1,2); } }

我们对Sub.java文件进行静态检测，执行

openjml -esc Sub.java

运行结果

Open/Sub.java:6: warning: The prover cannot establish an assertion (ArithmeticOperationRange) in method compare: underflow in int difference return a - b; ^ Open/Sub.java:6: warning: The prover cannot establish an assertion (ArithmeticOperationRange) in method compare: overflow in int difference return a - b; ^ 2 warnings

出现溢出。

2.JMLUnit总结

由于Graph接口过于复杂，我先测试了几个规模小的java文件。沿用上面的Sub.java,使用JMLUnitNG自动生成测试用例执行以下命令

java -jar jmlunitng.jar Open/Sub.java  javac -cp jmlunitng.jar Open\*.java  java -jar openjml.jar -rac Open/Sub.java  java -cp jmlunitng.jar Open/Sub_JML_Test

运行结果

[TestNG] Running:   Command line suite  Passed: racEnabled() Passed: constructor Sub() Passed: static compare(-2147483648,-2147483648) Passed: static compare(0,-2147483648) Passed: static compare(2147483648,-2147483648) Passed: static compare(-2147483648,0) Passed: static compare(0,0) Passed: static compare(2147483648,0) Passed: static compare(-2147483648,2147483648) Passed: static compare(0,2147483648) Passed: static compare(2147483648,2147483648) -1 Passed: static main(null) Passed: static main({})  =============================================== Command line suite Total tests run: 12, Failures: 3, Skips: 0 ===============================================