一、梳理JML语言的理论基础
（1）理论基础
JMl的出现很大程度上一为了行为接口的规范化，用这种语言来指定特定模块的特定功能。JML的核心部分分为三个部分：前置条件（requires）、后置条件（ensures）、副作用（assignable）。通过JML的使用，程序员可以轻松的描述一个方法的与其功能而不用管具体的实现方法，JML把过程性的思考延迟到了方法的设计中，从而扩展了面向对象设计的这个原则。
（2）应用工具链
OpenJML可以检查JML描述语言语法的正确性、以及所实现的代码能否满足JML语言所描述的要求，并提示问题的所在。
Junit可以单独测试某一个方法的正确性，可以帮助编程者对程序进行彻底的排查，准确的定位出BUG。
Javadoc是提供编写Java注释程序模板的工具，在真正写JML注释时只需要调用提前编写好的模板就可以了，将会省去做大量的重复工作的时间。
二、JML Unit自动测试
JMLUnitNG是一个为使用了JML注释的java代码生成自动化测试的工具。
使用其的基本流程是首先进行环境配置，然后就可以使用工具生成文件的测试类，编译需要进行测试的文件，最后运行test类就可以了。
在测试后发现JMLUnit可以产生一些边缘数据和常规数据来对我们的代码进行检测。
三、梳理框架结构
第一次
第一次作业要求完成MyPath和MyPathContainer两个类。
在MyPath中我构建了两个容器，一个是储存当前所有节点以及节点顺序的ArrayList，以及储存非重复节点的容器HashSet。
nodes可以解决大部分查找点的问题，而nodeSet可以快速解决getDistinctNodeCount的问题。
在MyPathContainer中我构建了三个容器：
前两个可以完成ID与path之间的快速转换，而第三个HashMap是表示节点出现的次数，在每次add和remove时都要对这三个容器进行更新操作，虽然对于add和remove操作的速度回下降，但是对于getDistinctNodeCount问题可以把复杂度简化为O(1)。
第二次
第二次作业主要是完成MyGraph中的四个新方法：containsNode，containsEdge，isConnected和getShortestPathLength。其中containsNode可以通过上一次的total来迅速得出
我新构建了两个类：Edge和Connect
Edge类用来保存所有的边信息，也就是所构建出的一个邻接矩阵来存放边的信息。
Connect类用来储存两点之间shortestPath的信息。
用Edge类解决containsEdge，而isConneted和getShortestPathLength可以归为一类求解最短路径问题来考虑，只要存在最短路径必定相联通。所以每次输入from和to时如果已经储存在connect中就直接取出，否则就用dijkstra求解出最短边加入到Connect中。
第三次
第三次作业主要是完成MyRailwaySystem中的五个方法。
这次作业相较前两次有着较大的难度，首先困扰我的是如何解决不同路线的换乘问题。在看了讨论区的方法之后我的眼前豁然开朗。可以将一条路径根据不同的需求已不同的权重拆分成多段小路径并加入到相应的图中，之后只用遍历所求问题所对应的图就可以了。为此为三种不同的问题分别对应不同的边权重来各构建了两个图，一个是储存当前信息的图，另一个是储存所计算出来的最短结果的图。
每一个图求最短路径都用dijkstra的方法。
连通块个数的求解是运用深度优先遍历（DFS）的方法求解。
四、bug分析和修复
这三次作业每一次都是继承自上一次作业的接口，环环相扣，很可能由于第一次的构思不当而导致最后一次的结构十分复杂。就说我的程序，最后一次尽然达到了十二个图之多，每一次的addPath和removePath都是一次巨大的工程量。
但是这次作业方便的地方在于，只要你能够保证自己所写的程序和课程所提供的JML完全匹配，就基本上没有错误，再加上有许多辅助工具的帮助，只要算法充分掌握就应该没有什么难点了。所以我三次强测和互测都没有被找到BUG。
同学们所犯的错误大都分为两类：一是边界问题没有考虑清楚，或者是有些没有验证到的地方有输出错误，大多都是可以通过特殊样例检测以及全面测试而检测出来的；第二类则是数据结构比较简单，没有进行时间上的优化。对于这类问题，单靠自己空想是很难想到优秀的算法的，这时就要多搜索查找快速且方便的算法，多与同学们交流讨论，这些都是最快的取经之道。
五、心得体会
通过本次作业我感受到了JML的强大之处，明白了类规格，方法规格，数据规格的写法，感受到了规格的巧妙之处。方法规格由前置条件、副作用和后置条件所组成，用来方便上层统筹，下层协作。众多编程者都可以根据JML的描述完美无缺的来完成一个庞大的作业。
通过这次OO作业，我发现可以通过复杂的数据结构来节省出重复计算的时间开销，就是用时间换空间当我们的程序对于时间的要求交高而对空间限制几乎没有的时候，我们就可以将每一次计算所得的数据都记录下来，当下次要再次使用时在就可以快速查找了。在使用这种方法时一定要注意数据的更新与重置，一旦忽略了一步那么后面的数据都会出问题。总而言之，写程序讲究的就是一个小心仔细