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

Java建模语言（JML）是一种行为接口规范语言，可用于指定Java模块的行为 。它结合了Eiffel的契约方法设计 和Larch系列接口规范语言的基于模型的规范方法 ，以及细化演算一些元素 。

JML有标准的注释结构，由JML的语法表达式构成，有固定的方法规格和类型规格。

JML应用工具链

openjml是所有工具链的核心，可以通过命令行工具对代码进行jml的语法检查，代码静态推导和动态检查。

在eclipse中，有jml的官方gui，但是仍然是基于openjml命令行的，命令行有的问题gui里一应俱全，不过gui中可以更有针对性的给出一部分推导过程，使用起来很方便。

jmlunitNG则是一个根据testNG进行测试，能根据jml来生成测试样例的工具。

• (2)【改为选做，能较为完善地完成的将酌情加分】部署SMT Solver，至少选择3个主要方法来尝试进行验证，报告结果

 (3)部署JMLUnitNG/JMLUnit，针对Graph接口的实现自动生成测试用例（简单方法即可，如果依然存在困难的话尽力而为即可，具体见更新通告帖）， 并结合规格对生成的测试用例和数据进行简要分析

测试样例

测试结果

 

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

三次作业类图

第一次采用hashmap以pair<>为key存储边，value存储边的个数，同样点也这样存储。

对于removebyid和removebypath，采用双向hashmap，path为key存储边，value存储边的值，另一个反之

第二次加入了图

用佛洛依德算法，利用边集重构

每次加入和删除操作重新构建最短路径

第三次综合了地铁路线

我们构建不同的图，最短路径，最低价格，最低满意度，构建不同的权重图，但是用一样的迪杰斯特拉算法

对于换乘采用了拆点算法

• (5)按照作业分析代码实现的bug和修复情况

第二次的用PAIR导致cpu超时，用简单的数组矩阵会提高更多的效率

• (6)阐述对规格撰写和理解上的心得体会

感觉JML规格能很好的规定数据的改变，和算法的约定。