第三单元主要介绍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是个好东西，能用就用。