OO第三单元博客作业

OO第三次博客作业

1. JML理论基础

   JML是用于对Java进行规格化设计的一种表示语言。JML一方面可以在测试时为开发人员提供逻辑严格规格以避免二义性，另一方面可以提高代码的可维护性。

   JML包含了类型规格、数据规格、方法规格等形式。其中，方法规格包括了前置条件、后置条件、副作用范围限定等约束。

2. JML工具链

   Openjml：以SML Solver为组建，进行jml语法检查、代码静态检查、生成运行时测试类

   JMLUnitNG/JMLUnit： 针对类自动生成测试样例并进行测试。

3. 部署JMLUnitNG并自动生成测试用例

通过JMLUnitNG对Group类自动生成的测试用例并进行的测试如图，可以看出，JMLUnitNG主要对边界数据进行了测试。其中，addPerson和delPerson方法由于在规格中没有规定当person == null时的情况而出现bug；updateRelation方法当value过大时，出现了溢出情况。

4. 架构设计分析

   三次作业的架构主要以课程提供的规格为约束。

   第一次作业：对Person的存储使用了<PersonId, Person>的Map结构。

   第二次作业：新增Group类，为了降低程序复杂度，对Group中的一些计算结果进行储存。

   第三次作业：NetWork中新增大量方法，为了降低isCircle方法和queryBlockSum方法的复杂度，person之间的关系采用并查集结构来实现；queryMinPath方法采用迪杰斯特拉算法来实现；queryStrongLinked采用两层dfs方法来实现

5. bug分析

   第一次作业：较简单，未出现bug。

   第二次作业：addToGroup方法中对Group人数进行了限制，而在代码实现时没有考虑到这一点。

   第三次作业：queryMinPath方法的时间复杂度过高，以至于CTLE；queryStrongLinked方法采用两层dfs方法在数据量过大时发生了爆栈。

6. 心得体会

   1. 在撰写规格时，应尽可能将前置和后置条件以及可能出现的异常都写清楚，不要留下逻辑上的漏洞；同时对代码实现的方式不要做过多的限制，比如add方法可能会存在的默认插入顺序问题。
   2. 在通过规格实现代码时，一定要满足规格中的所有条件；在此基础上，不要被规格中的数据结构所限制，尝试使用效率更高的实现方法。