• (1)梳理JML语言的理论基础、应用工具链情况
JML(Java Modeling Language)是用于对Java程序进行规格化设计的一种表示语言。JML将注释添加到 Java 代码中，这样我们就可以确定方法所执行的内容，而不必说明它们如何做到这一点。有了 JML，我们就可以描述方法预期的功能，无需考虑实现。JML主要用于开展规格化设计，或者针对已有的代码实现，书写其规格，从而提高代码的可维护性。
工具：
SMT solver：使用SMT solver工具可以静态分析代码，检查代码对规格的满足情况。
JMLUnitNG：基于jml来自动生成测试用例。
• (3)部署JMLUnitNG/JMLUnit。
下面是运用JMLUnitNG针对MyPath.java中部分方法自动生成测试用例的运行结果。
可以看到自动生成的数据主要是null，0，int最大值，int最小值等情况。
• (4)梳理自己的架构设计
在第一次作业较为简单，在MyPathContainer中，我使用了两个HashMap来存储Path和id，减小getpathid和getpathbyid方法的复杂度，用了node的Hashset来减小getDistincNode方法的复杂度。
第二次作业中增加了图结构，我在MyGraph中增加了一个二维数组类型的成员变量存储图结构，新增了Edge类存储边，为下一次做了准备，并增加了求最短路的floyd方法。在调用add等变更图结构的方法时，都调用一次floyd方法，getShortPathLength时，只需要查询二维数组即可。其他地方与第一次作业基本一样。
第三次作业在图结构的基础上实现了地铁系统，本质上跟第二次作业没有太大差别。新增了最短换乘，最低票价等方法，实际上只是增加了边权的求最短路。我的架构与第二次也没什么区别，只是新增了几个不同的建图方法，不同方法中Edge的权值不同。同样也是在变更图结构是进行重新建图以及计算最短路。
第三次作业UML图：
• (5)bug和修复情况
第一次作业：强测出现bug。原因：不小心将cnt - 1写成了 --cnt；
第二次作业：强测和互测都没有出现bug。
第三次作业：强测和互测都没有出现bug。
• (6)对规格撰写和理解上的心得体会
规格的初衷是用比自然语言更严谨的方式描述方法的功能，让开发人员的理解更加准确。
然而在实际撰写和阅读规格时，我发现规格确实有严谨的优点，但也存在着难以表达，难以理解的缺点，在撰写一些较为复杂的方法的规格时，还可能需要引入一些其他的方法。要想更好地利用规格的优势，可能需要大量地阅读以及撰写规格。