BUAA-OO-第三单元总结
又经过了三周的学习后，我们终于又度过了一个单元。本单元主要讲的是关于JML规格的一些设计，下面我将详细分享一下我对JML的一些理解以及这三次作业中我对JML UNIT等相关工具的应用。
一、什么是JML
JML是Java Modeling Language的缩写，顾名思义，它是一种Java建模语言。它有一套自己的语法，这套语法描述出一个方法的正常和异常情况、前置条件、改变量与不变式、后置结果。也就是说它可以准确描述出一个方法用来干什么以及如何使用。比如在这几次的作业中，我们只需继承几个类，实现这几个类中的方法，并将类传入到AppRunner中，即可完成AppRunner的全部功能，得到我们想要的标准输出或异常输出结果。
具体语法内容包括：
行注释：//@xxxx 块注释：/*@xxxxx@*/
原子表达式： esult；old
量化表达式：forall；exits
等价关系：<==>；推出：==>
前置条件：requires；后置条件：ensures；副作用：assignable
不变式：invariant；状态变化约束：constraint
工具链：
比较常用的有OPENJML对JML语法的检测，JMLUNITNG自动生成测试样例等。
二、JMLUnit/JMLUnitNG的使用
如图为我随便写的一个测试程序，包括了add和div
接着使用JMLUnitNG生成的自动测试用例及结果如下
可以发现add涉及到了溢出问题，div涉及到了除数为0的问题。
三、三次作业的架构设计
第一次作业
第一次作业比较简单，但普通的做法会卡cpu时间，所以必须把PATH_GET_ID，PATH_GET_BY_ID，PATH_DISTINCT_NODE_COUNT等指令均摊在add和remove中。我采用了双hashmap使得id和path相互对应，并且还使用了一个hashmap记录不同结点的个数，每次add和remove时都会更新这3个hashmap，这样在进行其它指令时只需到相应的hashmap中查找，或者返回hashmap的大小即可。
第二次作业
第二次作业在第一次作业的基础上，新增了间结点是否有边，是否相连以及最短路径的指令。做法同第一次，在每次add和remove的时候更新相应的值。所以我新增了两个hashmap套hashmap的结构edge和arrive模拟二维数组，在每次add时将每个结点直接相连的结点存在edge中，然后用BFS算出该节点的最短路径存在arrive中，这样是否有边和是否相连就可查找edge和arrive解决，最短路径返回相应的arrive的value即可。
第三次作业
第三次作业是最难的，在第二次作业的基础上，新增了连通块数量、最低票价、最少换乘、最少不满意度4条指令。同样需要把这4条指令摊在add和remove中。这次由于使用二维矩阵比较好做，所以我新建了4个静态int型二维矩阵，分别为side,change,price,pleasant此外，还需要将节点id和数组下标相对应，所以我新增了2个hashmap使id和下标相互对应，并且新加了一个Queue在删除时维护下标队列。至此准备工作完成。具体算法我采用的是讨论区wjy大佬说的不拆点做法，也就是给每个path的可达矩阵赋不同权重，用floyd算法后，将该可达矩阵赋值到change/price/pleasant矩阵，之后再用一次floyd算法，即可得到最少换乘/最低票价/最少不满意度。连通块的个数我是采用类似并查集的做法，通过edge计算后存下来即可。最后在调用相关指令时去访问相对应矩阵中的元素即可。
从三次作业的变量名也可看出我并没有进行过重构，只是在原有的基础上加了新的需求。因为原来的需求是不变的，这样我至少可以保证旧的需求的正确性，在此基础上添加新内容出现bug的几率比较小。
四、bug情况
很幸运的在三次作业的强测和互测中都没有出现bug，3次强测中最长CPU时间分别为5.0s,6.9s,9,0s左右，与限制的最大CPU时间相差较远，所以我自我感觉这三次作业我设计的还是不错的。
五、心得与体会
我觉得这一单元还是比较有趣的，就像是在实际场合中下发一个任务，我需要完成它。这三次作业的整体难度并不大，但其中涉及到一些图论的知识以及数据结构相关知识，由于之前学的不太好导致在编码过程中出现了问题。此外，我认为JML是一个很好的建模语言，它提供了一个标准，架构师把标准定好，实现人员只需要按照这个规格实现即可。它避免了因为自然语言上的二义性或者不同人的理解问题带来的差异，在一个大型的工程中，需要很多人完成不同的项目，最终整合成一个大项目。如果有了JML这样的语言，就可以使每个人准确无误的完成各自的任务，避免因为理解不同而带来的问题。至于JMLUnit之类工具的使用，只是简单的进行了尝试应用，希望以后能够更加灵活使用这种自动化测试的方法。