OO第三次博客做业（第三单元总结）

(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进行发现。因此，感受测试程序的重要性真的不亚于写出程序。但每次写完做业后，老是感受测试的时间和精力不够，这个问题一直困扰着我，说到底仍是但愿可以好好实践一下测试方法，尤为是随机测试的方法。