一、JML规格与工具链应用
JML 概述
使用 JML 来说明性地描述所希望的类和方法的行为，可以显著地改善整个开发过程。将建模表示法添加到 Java 代码中，其好处包括以下几点：
能更加精确地描述代码所完成的任务
能有效地发现和纠正错误
能减少随着应用程序的进展而引入错误的机会
能较早地发现客户没有正确使用类
能产生始终与应用程序代码保持同步的精确文档
JML 注释始终位于 Java 注解(comment)内部，因此它们不会对进行正常编译的代码产生影响。当我们想将类的实际行为与其 JML 规范进行比较时，可以使用开放源码 JML 编译器。用 JML 编译器编译过的代码如果没有做到规范中规定它应该做的事，那么该代码在运行时会抛出 JML 异常。这不仅能捕获代码中的错误，还能确保文档(JML 注释格式)与代码保持同步。
二、JML工具链
可以使用的JML工具链包括
OpenJML：可以实现JML语法错误检查。
SMTSolver: 在逻辑层面、对代码实现形式化验证。
JMLUnitNG: 根据JML规格生成对应的测试样例来测试程序。
三、作业设计
第九次作业：
照搬规格即可。需要考虑的点有：
1.people、value用什么来存储
2.isCircle用什么算法来实现
对于第一个问题，我用的是Arraylist。第二个问题，我用的是bfs搜索。
第十次作业：
添加了Group接口以及组内查询方法，按照规格书写即可。
第十一次作业：
添加了查询最短路径的方法，以及添加查询两点是否在同一点双的操作。
其中前者我用了djstra算法，后者用了targan算法。
四、bug情况
这三次作业均通过了弱测中测，但是强测我出现了许多bug。
五、感想
JML是为契约式编程而生的。requires 描述先验条件，ensures 描述后验条件，old 描述副作用，exceptional_behavior 描述异常。理论上来讲，通过JML，可以进行形式化的验证，让bug不复存在。然而如何保证规格书写的全面和正确又是另一个问题。因此正确而全面的理解JML也成为了一个问题。通过对 JML 这门语言的学习，我对于契约式编程的理解更加深刻了。