-
(1)梳理JML语言的理论基础、应用工具链情况
·关于建模语言
JML（Java Modeling Language）直译成中文就是Java建模语言；建模语言是一种描述信息或者数据模型的概念的语言，其目的在于实现模型概念的传递，提供了系统的设计蓝图，在工程上主要是为了以合理的性能价格并在预定的时间内开发出高质量的软件。
从60年代侧重于编码阶段的研究到70年代广泛采用软件工程学的观点，及至80年代对软件工具和环境的研制，软件开发的主要研究方向在于通过各种方法和技术来提高软件产品的生产率和质量。但随着软件项目规模的越来越庞大，系统也日益复杂，这个问题远未得到较好的解决。
而建模语言的提出是基于如下的认识：软件和其它工业产品一样，其生产率和质量的高低最终取决于生产产品的过程的好坏，故通过对软件过程本身的研究，改进软件过程的质量，可以使软件项目的实施更有效，更可预见，获得高的生产率和高质量的软件。
·jml语法
1、常用关键字及其含义
\nothing 无
\result 方法返回结果
\forall 全称量词
\exsits 存在量词
pure 表示此方法不会修改任何值
also 连接两个不同的行为
requires 要求输入满足的条件，前置条件
ensures 返回结果保证的条件，后置条件
signal 发出异常信号
invariant 不变量
not_null 被修饰对象非空
2、数据规格约束语句
invariant ：在成员处于可见状态下必须满足的特性，不变式约束
constraint ：变化约束。
3、方法规格约束语句
前置条件 requires BoolExpr1 || BoolExpr2 || …;
后置条件 ensures BoolExpr1 || BoolExpr2 || …;
副作用影响要求 assignable modifiable
无副作用声明：pure
方法的异常行为声明：normal_behavior, also, exceptional_behavior, signals () expr, signals_only;
4、其他
对于变量的描述语法和java基本相同。
·应用工具链情况
1、用于自行编写单元测试代码
JUnit：单元测试工具，可以对某一个类的特定方法进行测试。
JMLUnitNG：可以自动生成测试用例进行JUnit测试。
2、用于验证相关方法是否满足jml规格
OpenJML：可以根据程序的规格进行静态和运行时检查，检查程序是否遵守了规格。
SMT Solver：形式化验证工具，已经集成在了OpenJML里面。
3、相关链接
OpenJML
官网：
JMLUnitNG
官网：
jar链接：
-
(2)部署JMLUnitNG/JMLUnit，针对Graph接口的实现自动生成测试用例。
1、生成的相关测试文件
2、用 jmlc编译自己的文件并运行测试
-
(3)按照作业梳理自己的架构设计，并特别分析迭代中对架构的重构
·第一次作业：实现一个路径管理系统
第一次作业实现起来似乎很简单，只需要按照jml的要求写就行了，所以在结构上：
·第二次作业：实现一个无向图系统：
第二次作业本来应属于第一次作业的迭代开发，结果我没有使用继承，而是使用了复制第一次作业的相关代码加入第二次作业中，并且在开发过程中，没有太多的考虑结构或者代码的可阅读性。虽然写得时候似乎是“很流畅”。其实最后回过头来看，觉得真的没有一点面向对象的编程感觉，实在应该检讨。结构如下（第一次作业实现的PathContainer被删了。。。全复制到Graph里）：
在第三次作业开始时一方面第二次作业因为数据结构选的不对导致RTL，需要更改原先滥用HashMap 的数据结构；另一方面在此开代码时，有感结构问题，于是重新写过了一次，结构如下（完成时间晚于debug截止时间）：
·第三次作业：实现地铁票价计算系统
未在规定时间内完成，以下是修复bug阶段完成的工作，在结构上还是勉强比之前的好的。。。
-
(4)按照作业分析代码实现的bug和修复情况
·第一次作业
没有被测出bug
·第二次作业
强测有四个点没过，似乎是由于过多的使用了HashMap的缘故，互测时被刀的样例也在此列。
修复时赶上第三次作业发布，因为感觉到floyed算法在第三次作业似乎不好实现，且架构很不合理，正如上文说的没有做到继承；第二次作业写得很乱，于是乎做了一个错误的决定：同时重构架构与算法实现。于是交了十几个版本都没有过，然后的然后，由于各种时间安排的原因，导致Debug和第三次作业都没有按时完成。。。
·第三次作业
没有进入互测，功能上并没有完全实现。
-
(5)阐述对规格撰写和理解上的心得体会
规格有时候感觉没有直接写文字描述来的好理解，但毕竟它很有条理的列出来各类要求，描述精确。尽管写代码前要面对一大堆与代码没有“直接”关系的规格很头疼，也会花许多时间，但毕竟避免了莫名其妙的bug，这三次作业如果数据结构选的好的话，基本上不会有对题意理解不清或者是没有实现题意的bug，由此可见规格对代码开发有很大的帮助。
另一方面，规格对于自己的覆盖性测试也很有帮助，且不谈现在一些直接根据jml生成测试的工具链，其实自己写代码的时候稍加用心，可以做到自己思路内的覆盖测试。