• (1)梳理JML语言的理论基础、应用工具链情况
JML 为说明性的描述行为引入了许多构造。这些构造包括模型字段、量词、断言的可见度范围、前提条件、后置条件、不变量、合同继承以及正常行为与异常行为的规范。使用JML来声明性地描述一个方法或类的预期行为可以显著提高整体的开发进程。
JMLUnitNG自动测试；
JMLUnit生成测试框架;
SMT Solver检查代码是否满足规格；
openJML检查规格；
• (2)部署JMLUnitNG/JMLUnit
在边界检查时都Failed;
• (3)按照作业梳理自己的架构设计，并特别分析迭代中对架构的重构
第一次作业中，对于getDistinctNodeCount()函数，开一个HashMap，在每次增减Path时更新，该函数里return 其size即可。为了快速查找，再开两个HashMap，一个以Path为Key，令一个以id为Key。
第二次作业在第一次基础上增加图，用二维数组存储图和边，将id映射到数组下标，在增减时用floyd算法更新图，就能完成新增加的需求。
第三次作业是地铁系统，又增加了三个图来存储不同的边权值，用的讨论区里的方法，没有拆点，几个图的权值不同，也是用floyd算法来的到对应的需求。
这三次作业我都是三个类实现，没有新开出类，这种架构当然是不好的，以后还是得多多思考架构方面；在每次迭代中，并没有重构，如果需求又增加了，那我这架构大概率得重构。而且，对于cpu时间的限制，并没有用到什么技巧，都是在增加减少Path时直接更新图，貌似时间也挺宽松。看了别的同学的代码，觉得在架构方面确实跟别人差的蛮大。我基本不会想太多，怎么方便怎么来。
• (4)按照作业分析代码实现的bug和修复情况
无
• (5)阐述对规格撰写和理解上的心得体会
对规格这东西还是有点糊涂，特别在第三次作业时，规格描述很长，看得就很麻烦。由于该系列只是根据规格写代码而没有让我们自己写规格，整体下来还是挺轻松的。