第三单元的作业主要是围绕JML规格对编程进行训练。三次作业都是实现课程组所给的带有规格的两个接口，Path接口三次作业中基本不变，另外的接口根据作业需求而改变，从第一次的PathContainer容器的实现，到第二次的Graph图的实现，再到第三次的RailwaySystem的实现。三次作业在练习按照JNL规格编程的过程中，同时还对Java下的图算法进行了训练，收获还是很多的。

  一. JML的语言基础

  JML是对Java程序进行规格化设计的一种表示语言，为严格的程序设计提供了一套行之有效的方法。通过JML及其支持工具，不仅可以基于规格自动构造测试用例，并整合了SMTSolver等工具以静态的方式来检查代码实现对规格的满足。语言基础如下:

 1.注释结构

    JML以javadoc的方式来表示规格。注释结构有两种，行注释//@annotation和块注释/*@annotation@*/。

 2. 表达式

  在课程中用到的表达式有以下几种：

  \old(expr)：表示表达式expr在该方法执行前的取值。

  \forall 表达式：全称量词修饰的表达式，表示对给定范围的元素，每个元素都满足相应约束。

  \exists 表达式：存在量词修饰的表达式，表示对给定范围的元素，存在某个元素满足相应的约束。

  b_expr1==>b_expr2：当b_expr1为false或者b_expr1==true且b_expr2==true的时候，整个表达式的值为true。

  \nothing： 指示一个空集。

 3. 方法规格

  方法规格的核心内容包括三个方面，前置条件、后置条件和副作用约束。

    前置条件：通过requires子句来表示，requires P；要求调用者确保P为真。

    后置条件：通过ensures子句来表示，ensures P；方法执行者确定方法执行返回jie'guo一定满足谓词的要求，即P为真。

    副作用约束：指在执行过程中会修改对象的属性数据或者类的静态成员数据，使用assignable或者modifiable。

  同时为了区分正常功能行为和异常行为，使用public normal_behavior和public exceptional_behavior去区分。异常行为使用signals抛出异常。

4. 类型规格

  invariant P：要求在所有可见状态下满足的特性。

  constraint P：对前序可见状态和当前的可见状态的关系进行约束。

二. 工具链的使用情况

1. openJML

  在eclipse上安装教程安装了openJML，直接检查就可以。在IDEA上下载完成后，输入指令去检查。

2. JMLUnitNG

  下载jar文件后，在命令行输入命令并指定jar文件位置便可以自动生成测试文件。

三. JMLUnitNG的使用

  JMLUnitNG是一个用于JML注释的java代码的自动化单元测试生成工具，生成的测试使用TestNG的单元测试，目前会生成OpenJML、RAC等的测试。

  在本次的使用过程中，我是将三次作业中的Path接口的实现代码单独拿出来作为一个项目进行了测试。测试的指令分为三部：

(1)java -jar D:\oo\JMLUnitNG.jar src\MyPath.java

　生成如下的测试文件：

  接下来两步是使用如下指令:

(2)javac -cp src\;D:\oo\JMLUnitNG.jar src\MyPath_JML_Test.java(3)java -jar D:\oo\openjml-0.8.42-20190401\openjml.jar -exec D:\oo\openjml-0.8.42-20190401\Solvers-windows\z3-4.7.1.exe -rac src\MyPath.java   java -jar D:\oo\openjml-0.8.42-20190401\openjml.jar -exec D:\oo\openjml-0.8.42-20190401\Solvers-windows\z3-4.7.1.exe -rac -d out\produnction\test src\MyPath.java

  第三步是进行JML检测，如果在执行第一条语句之后运行MyPath_JML_Test.java程序出现如下错误，则在执行第二条语句即可。

Failure : racEnabled()

  执行完上述三步之后，便可以将JMLUnitNG.jar的包引入项目中，运行MyPath_JML_Test.java文件，结果如下图所示：

  可以看出在上述测试中，涵盖了所有的MyPath中的方法。

  (1).对构造函数进行null和{}的测试，可以看出在程序中没有考虑输入为unll的情况。

  (2).对compareTo方法进行了null的测试，可以看出方法中也没有考虑到null的情况。

  (3).对comtainsNode()方法和getNode()方法都进行了-2147483648、2147483647，0的测试，均Passed。

  (4)对hashCode()、isValid()、iterator()、size()都进行了测试并且都Passed。

  可以看出测试文件覆盖了几乎所有的方法。

四. 架构设计

1.第一次作业

  本次作业的类图如下图所示：

  对Path接口来说，为了实现功能的方便，使用了ArrayList、hashSet以及int数组去存储数据，ArrayList是在iterator中使用，利用HashSet存储的特性，可以直接得出getDistinctNodeCount的值。

  在MyPathContainer中，因为存在用id取path、用path得到id的方法，所以为了实现方便，使用HashMap<Path,Integer>、HasMap<Integer,Path>的数据类型，用不同的key值去存储path与id之间的对应关系。

2. 第二次作业

  本次作业的类图如下：

  Path类的实现和第一次作业是一样的，所以不在此赘述。

  在MyGraph中使用邻接表HashMap<Integer,HashMap<Integer,Integer>>去存储图结构，为了提高速度，使用n次的迪杰斯特拉算法去计算节点之间的最短距离。为了提高查询的速度，在每次加入路径或者删除路径的时候都会调用一次calDistanceDij去计算图中各个节点之间的最短距离。

3. 第三次作业

  第三次作业是实现一个RailwaySystem，具体的类图如下：

  Path类和前两次基本一样。

  这一次作业的重点是对最少价格、最低不满意度以及最少换成次数进行求解，采用的方法是拆点法，即将不同路径上的同一点分开，作为不同的点去处理。新建一个NodePath类，存储节点id以及路径id。新建一个邻接表HashMap<NodePath,HashSet<NodePath>>去存储新的图。计算这三个的过程依然是使用n次的迪杰斯特拉算法，只是在不同边的权重不一样，调用的类是DijChange。在求解连通块的时候，使用的是求解并查集的方法，调用的类是UnionFindSet。

五. BUG分析

 第一次作业没有明显的语义错误，在强测过程中出现了四次的CPU运行超时，个人感觉MyPathContainer.getDistinctNodeCount()方法中的循环时间超时。

  第二次作业的bug主要在迪杰斯特拉数组的初始化上，在初始化的过程中，由于一个节点的邻接表中是不包括自己的，忘记排除这一个情况，导致自己到自己的距离被设置为Integer.MAX_VALUE，导致两次错误。

  第三次作业除了前三个是Wrong Answer之外，剩下的都是超时。前三次的错误沿袭了第二次作业中的BUG,在计算最短距离的时候倒是注意了这个问题，在初始化剩下三个的数组的时候没有考虑到这种情况，导致其被赋值Integer.MAX_VALUE，出现错误，导致第三次作业得分为0。

六. 个人总结

  本单元的作业主要是基于课程组提供的JML，实现接口。锻炼了对JML的阅读、编写能力。我在本单元最大的收获是对不同的要求使用不同的数据类型，刚开始写的时候以为只能使用int数组，与大佬交流之后才知道可以使用不同的数据类型去实现功能，并且对图的相关算法得到了更深的了解。