(1)梳理JML语言的理论基础、应用工具链情况
Java 建模语言(JML)将注释添加到 Java 代码中，这样我们就可以确定方法所执行的内容，而不必说明它们如何做到这一点。有了 JML，我们就可以描述方法预期的功能，无需考虑实现。通过这种方法，JML 将延迟过程设想的面向对象原则扩展到了方法设计阶段。
JML的核心包括以下三个部分：
前置条件：requires
后置条件：ensures
副作用：assignable/modifiable
同时它也能够对程序的各种执行条件进行划分：normal_behavior/expectional_behavior
由于JML具有规范性，所以可以用JMLUnitNG/JMLUnit等工具生成测试用例，对相应的程序进行自动化测试。当然测试的正确性是有前提的：JML规格必须得写对了。
(2)【改为选做，能较为完善地完成的将酌情加分】部署SMT Solver，至少选择3个主要方法来尝试进行验证，报告结果
这部分先跳过吧。
(3)部署JMLUnitNG/JMLUnit，针对Graph接口的实现自动生成测试用例
在自己的电脑上根本没法部署。由于某个我不知道的原因，这个学期我的cmd上一直没法跑java，无论怎么改环境变量都不管用，连个
java -version
都识别不了，别说openJML，连上学期的logisim和Mars都跑不了。
这一部分暂时先咕掉，看看有没有什么其他的解决办法。
(4)按照作业梳理自己的架构设计，并特别分析迭代中对架构的重构
个人觉得这次作业不需要怎么画UML图了，因为实现的接口都是定死了的。整个单元作业的精髓在于各种实现方法的选择，包括但不限于数据结构（容器）、算法。
第一次作业开始，我就采用了讨论区里所一致推崇的双向HashMap存储点数关系的方法，这个方法在第一次作业中主要针对DISTINCT_NODE_COUNT指令，而从整单元作业来看，这个方法为本单元之后的两次作业打下了良好的基础。
在第一次作业中，我直接采用数组来作为Path的保存容器，后来简单起见改成了ArrayList。
第二次作业开始涉及图结构，对图结构的保存，我采用了可能稍微特别的方法：在上次作业保存的点集基础上，新增一个HashMap来保存边集，而遇到最短路径的计算时，再将点集和边集转化为邻接矩阵，运用DIjkstra算法求最短距离（现在想想这个转换是否有必要有待商榷），每跑一次Dijkstra算法可以算出n组点之间的最短距离，然后再用一个HashMap保存起来，用这种滚雪球的方法对抗时间复杂度。如果遇到增删，则在下次求最短距离时要把最短路径HashMap，邻接矩阵等内容进行更新（懒汉思想，不用就放着不管）。
第三次作业变成带权图，并且涉及换乘点的处理，复杂度进一步提升，牵扯到算法的选择。想到的第一种方法是，拆开每个换乘点，在换乘点间建立虚路径，对这些虚路径和实际存在的路径按要求赋相应的权值，完成各种不同的要求。但这样就涉及到了一个很要命的问题：极端情况下，换乘点可以高度重合（最极端的情况是所有路径全部重合，每个点都是换乘点，每个换乘点都可以换乘所有路线），这样的话图的点数就会爆炸，按普通Dijkstra算法的时间复杂度（O(n^2)，n为点数）肯定是不行的，尽管可以做堆优化把复杂度降到O(mlogm)（m为边数），但一个现实问题是：没找到Java版的堆优化代码，现有的C++版代码又看的不是很懂，而且大多数采用的是邻接表存储，这意味着可能要对程序的图存储结构进行较大调整，怎么给每条线路拆分出一个换乘点并以合适方式进行表示也是个问题。
所以最后我采用了另一种方式，在各条路径内部计算出路径上两点之间的各种最小值，包括换乘次数（其实没有这个，因为恒为0），票价（其实就是最短距离），不满意度并存储，并存入图中，然后在矩阵初始化时用两点间最小值加上换乘相关的权值（比如最小换乘就是1，最低票价是2，最小不满意度是32），在跑完Dijkstra算法后在减去相应值，就能求出最后的结果。相比上一种做法，复杂度来源主要在于路径内部又跑了一遍Dijkstra，但由于一条路径上就那么些点，所以效率还可以，不过肯定不如第一种算法。（说白了因为菜写不出来好的实现，我写代码像cxk.gif）
(5)按照作业分析代码实现的bug和修复情况
第一次作业：最开始的反向HashMap采用的不是Path映射PathId，而是Path的Hash值映射PathId，这就导致了存在Hash值重复的情况，虽然过了强测但互测被Hack一次。后来利用instanceof关键词重写了equals方法消除了Bug，也为后两次作业打下了正确的基础。
第二次作业：没Bug，表现不错。
第三次作业：灾难。由于对两条路径纠缠在一起的情况没有考虑到，导致初始化的时候出现问题（正常应该存两点间最小值，但我忽略了这种情况，按两点间只有一个值写的代码，导致这个值被错误刷新），另外还有一处明显的手误没看出来，在中测一遍过的情况下，强测10分，互测被Hack19次。但Bug越多，往往也意外着错误越明显、越简单，总共37个Bug被一次性修复，也算是一个尴尬的纪录了。
(6)阐述对规格撰写和理解上的心得体会
在写这次作业之前，我看到有人的作业中提出JML比较适合大型程序的结构描述，但我并不这么认为，因为从这几次的作业和课上实验来看，每次给出的JML规格都存在或多或少的错误，这就说明了一个问题：用JML语言准确描述代码要做什么，并不是一件容易的事情，代码越复杂，描述起来的难度就越大。具体到作业中，JML代码描述一些规模较小、功能较简单的方法还是比较容易的，但描述一些功能复杂、规模较大的方法则显得力不从心，比如最后一次作业中实现的Graph类中几个查找函数，与其从冗长且可能存在Bug的JML描述中进行对照，不如直接从指导书get到函数的实现要点。
再者说，JML的一个好处是没有限制实现方式，但这种没有限制实现方式的情况在实际的工业生产与大型程序设计中并不多见。以我们亲爱的OS实验课为例（当然OS肯定不会用Java写，这里仅仅做一个假设），在OS的课程中，每个函数之间的调用关系都非常紧密和复杂，JML代码能不能写对都是问题，即使写对了，在函数体内部，每个函数所执行的流程都非常固定，很难有自由发挥的空间，这种情况下，写一份JML描述几乎和写出程序代码无异！比如下面的函数，我想不出如果用JML能描述出什么花样来，更想不出写出的JML和程序代码能有多大区别：
15 u_int
16 diskaddr(u_int blockno)
17 {
18 if ( super && blockno > (super->s_nblocks)) {
19 user_panic("diskaddr failed!");
20 }
21 return DISKMAP+blockno*BY2BLK;
22 }
JML能胜任的情况，也就是在一些中小型程序（比如这种作业）中，程序员能够决定整个程序所采用的架构（尤其是数据结构）的情况下来描述程序，因为这种情况下是真正的只在意功能的正确性而不在乎如何实现，而在稍微大型的系统（比如OS的小操作系统，实际上它也没那么大）中，架构已经定的死死的，就很难有JML发挥的余地，这时候就只能用自然语言描述方法所期望的功能，然后由程序员套用现有的架构来实现功能。这种情况实际上在本单元的后两次作业中就体现了出来，在第一次作业后，Path，和PathContainer中的相关容器已经确定，这时候再看JML中的描述，就要在头脑内将其翻译成用我们对应的容器的实现方式，与其做这样烧脑的翻译工作，还不如直接看指导书的自然语言描述然后实现来得快呢。倒是描述一些边界、异常情况时，JML的准确性还算是起到了一点帮助。
另外说到准确性，从作业和实验课JML多次的改动中，就能看出一个致命的问题：用规格来确保程序的正确性，那么用什么来确保规格的正确性呢？
（说起来课程组可以考虑组织一次关于JML的辩论，效果绝对好）
但除开JML，我在第三次作业的一堆Bug中，深刻体会到了测试的重要性。因为测试不够强（不管是自己做的测试还是提交的中测），我强测只拿了10分，互测被各种Hack了19次（最后这37个样例被一波带走是最骚的）。虽然也尝试过用JUnit来进行测试，但还是没能想到初始化的可能情况，因而也构造不出复杂的样例。从这里就能看出随机测试的必要性，它能覆盖程序员没注意到的地方，对意想不到的Bug进行发现。所以，感觉测试程序的重要性真的不亚于写出程序。但每次写完作业后，总是感觉测试的时间和精力不够，这个问题一直困扰着我，说到底还是希望能够好好实践一下测试方法，尤其是随机测试的方法。