面向对象第三单云总结

第三单元主要介绍JML的规则与使用。第9-11次作业围绕这一目标，逐层深入地实现了一个地铁系统。

一、梳理JML语言的理论基础、应用工具链情况

JML是用于规范化java程序的一种语言，它可以规定java的方法所实现的功能。JML以java注释形式存在于接口或类代码中，每行以@开头。它可以描述的java方法的行为包括：

normal_behavior	后面为方法的正常行为
exceptional_behavior	后面为方法的异常行为
requires	前置条件，通常为对输入的限制
assignable	副作用范围限定，列出方法能够修改的类成员属性
ensures	后置条件，通常涉及返回值或操作前后类成员属性
signals	异常描述

它通过表达式规定方法的具体功能。表达式中的成分包括：

　　1.原子表达式，有 esult，old， ot_assigned， ot_modified， onnullelements， ype， ypeof等

　　2.量化表达式，有forall，exists，sum，product，max，min， um_of， esult等

　　3.操作符，有<:，<==>，==>， othing everything等

应用工具链：

可以借助OpenJML完成对JML的静态检查。与z3, cvc4等SMT solver配合使用，可以检查代码的理论正确性。

对于windows系统，可以在cmd/powershell中通过以下命令使用OpenJML：

　　java -jar <filepath>openjml.jar -cp <classpath> -esc|-rac <target java file> -exec <solverpath>z3-4.7.1.exe

三、部署JMLUnitNG/JMLUnit，实现自动生成测试用例

public class Demo {
    /*@ ensures 
esult == (num1 + num2);
      @ */
    public static int add(int num1, int num2) {
        return num1 + num2;
}

对上述Demo.java，选择使用JMLUnitNG生成测试文件：

　　java -jar jmlunitng.jar Demo.java

生成的测试文件有Demo_JML_Test.java和Demo_InstanceStrategy.java，以下是运行结果：

[TestNG] Running:
  Command line suite

Failed: racEnabled()
Passed: constructor Demo()
Passed: 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)
Passed: static add(2147483647, 2147483647)

 可见JMLUnitNG具备测试java代码是否符合JML规范的能力。

四、按照作业梳理自己的架构设计，并特别分析迭代中对架构的重构

对我的第11次作业代码分析UML类图：

可以看到MyPath()相关的类图相对简单，其功能自从第9次作业之后也很少更改。MyRailwaySystem类继承了MyGraph类，而MyGraph没有继承MyPathContainer，这是因为在第10次作业时我重构了MyPathContainer并直接在它的基础上添加功能实现了MyGraph。在第九次作业时，我没有很好地实现MyPathContainer，导致其中部分功能不能满足下一次作业的要求。

五、BUG修复情况

一切BUG源于超时。第二次作业由于使用floyed算法极大地阻碍了时间复杂度，在第三次作业中更改为prim算法，使用拆点法实现新功能，并且保存每次更新的最小生成树以简化计算。但由于MyPath中没有使用哈希存储，containsNode()等方法占用了过多的时间，导致了大量测试点超时。

六、心得体会

在实现JML指定的功能时需要细心、耐心地逐字检查。

在很好地实现了要求的前提下，通过继承不断更新迭代实现新功能的过程其实挺爽的。

HashMap是个好东西，能用就用。