BUAA-OO-第三单元总结

面向对象第三单元JML总结

JML理论基础及工具链梳理

JML语言理论基础

• JML语言是对于JAVA进行规格化设计的一种表述语言，他能以一种统一化语言，逻辑性强的格式，向程序设计者描述这一方法实现的功能，从而规范设计者去按照这一方向实现方法。从而避免了使用自然语言而导致描述上不清晰的问题，并且也提供了代码的可维护性，其他程序员可以通过阅读规格从而更好地理解代码。

• 本次JML三次作业中主要使用的JML语句如下：

  •  forall  表达式语法类似于for语句的语法，是全称量词修饰表达式，表示给定范围的一定元素，均满足一定要求。
  •  exists  表达式语法和for相似，是存在量词修饰表达式，表示给定范围一定元素，存在元素满足对应的要求。
  •  old  表达式用于表示对于实现方法前的取值
  •   esult 表达式表示一个有返回值的方法在执行完成后的返回值
  •  requires 代表前置条件，即调用方法前需要保证的前置条件
  •  assignble 代表方法使用过程中的可赋值修改副作用
  •  modifiable 代表方法使用过程中的可修改副作用
  •  ensures 代表后置条件，即调用方法后需要保证的后置条件
  •  ==>  代表推出，即推理表达式
  •  <==> 代表当且仅当，即等价逻辑表达式
  •  == 等于号，由于JML是逻辑描述语言，因此不涉及任何过程描述，仅是描述状态，因此需要用逻辑等号代表状态

• 此外，JML语言描述过程中，为了简化重复调用一些已经描述的过程，可以在JML语句中调用pure类型的方法，因此，一些不对任何变量修改的函数可以修饰为pure类型，供JML调用，例如：

 public /*@ pure @*/ int getNode(int index);

• JML还提供了signals字句定义抛出异常的行为，具体描述可以如下：

    /*@ normal_behavior
      @ ......
      @
      @ also
      @ exceptional_behavior
      @ ......
      @
      @ singals (Exception_1 e1) .....
      @ singals (Exception_2 e2) .....
      @*/

JML使用工具链梳理

• 本单元三次作业围绕的是根据JML规格编程，因此可能需要一系列JML工具辅助检查，包括JML语法检查，JML程序静态规格检查，JML程序运行时动态检查。因此可能需要以下工具：

  • OpenJml，检查JML语法和进行规格静态检查，检查规格是否符合规格。
  • JMLUnitNG，自动生成测试样例动态检查程序是否符合规格。
  • SMT Solver，由于OpenJml工具中自带的 z3 失效，需要再重新找z3的Solver程序，或者使用OpenJml自带的cvc4进行检查。
  • JUnit4，除了使用JML检查工具外，为了对代码的一些具体功能进行单元测试，还可以使用 JUnit 工具进行检查。

JML语法检查

• 在对程序框架设计过程中，对于自定义的一些方法为了规范化其实现功能，使用JML语言对方法进行建模，描述程序功能，方便程序员实现。因此在书写完方法规格后，需要对自己书写的方法检查方法是否符合JML语法。
• 使用 OpenJml 对程序规格是否符合语法要求，以第九次作业的 Path 为例，将 Path.java 中的规格拷贝到自己实现的 MyPath.java 当中，并且对规格中定义的 nodes 数组修改为自己使用的数据结构类型，之后在 cmd 或者 powershell 中输入如下命令（其中笔者的OpenJml路径为 D:OpenJml ）：

    java -jar D:OpenJmlopenjml.jar -check .Path.java

• 若命令执行结束后不输出任何信息，代表JML符合语法，否则会提示错误信息

程序规格测试（静态）

• OpenJml使用封装好的 SMT Solver 对程序设计是否符合JML规格进行静态测试
• 由于OpenJml中提供的封装好的Windows下的 SMT Solver 中的 z3 文件失效，因此可以使用cvc4解决：

java -jar D:OpenJmlopenjml.jar -prover cvc4 -exec D:OpenJmlSolvers-windowscvc4-1.7-win64-opt.exe -esc .Path.java

• 若执行结束后无输出，代表程序设计符合JML规格，否则会提示错误信息。

程序规格测试（运行时检查）

• OpenJml提供对含有 main 方法的程序提供JML程序进行运行时检查，检查是否能够正常运行且满足规格设计
• 假设 Demo.java 文件中完成了一个使用JML描述的一个类，并且定义了 main 方法，用于测试这些方法，因此可以使用如下命令进行运行时的JML检查：

java -jar D:OpenJmlopenjml.jar -rac .Demo.java
java -cp D:OpenJmljmlruntime.jar; Demo

• 一般情况下的单元测试，是没有 main 方法的，因此该方式的JML单元测试一般结合JMLUnitNG自动生成测试样例来辅助完成。

结合JMLUnitNG生成测试样例检查

• OpenJml提供了运行时检查的功能，但苦于单元测试中一般不含有 main 方法而难以进行，因此可以使用JMLUnitNG工具自动生成测试样例辅助检查。（笔者的 jmlunitng.jar 安装在 D:OpenJml 路径下）

java -jar D:OpenJmljmlunitng.jar .Path.java -d .
javac -cp .;D:OpenJmljmlunitng.jar; .*.java
java -jar D:OpenJmlopenjml.jar -rac .Path.java
java -cp .;D:OpenJmljmlruntime.jar;D:OpenJmljmlunitng.jar; Path_JML_Test 

• 这样就可以使用 JMLUnitNG 自动生成的测试样例，结合 OpenJml 的运行时检查功能，对Path中实现的方法进行运行时检查。
• 这一方法为单元测试提供了便利，但苦于 JMLUnitNG 中自动生成的测试样例有限且比较极限，可以使用 JUnit （与JML无关）工具对代码的功能进行单元测试。

使用JUnit进行单元测试

• 在IDEA安装好JUnit4插件后，可以自动生成测试类文件。在测试类文件中编写测试方法对程序的部分方法功能进行断言测试，可以进行自定义的断言测试。
• 使用JUnit单元测试的好处在于生成测试数据可以自定义，进行更加复杂的自定义功能测试，不依赖于JML。

OpenJML封装的SMT Solver方法验证

• 考虑到 OpenJml 对于部分复杂的规格不能进行验证，以及对于与规格要求的数据结构不同时不能进行正确验证。因此对 Path.java 规格做以下修改：

  • 首先将规格中 //@ public non_null int nodes[]; 删去，在自己的代码中定义的 private //@ spec_public @// ArrayList<Integer> nodes; 
  • 由于对于类似 //@ forall int[] arr...... 或者 //@ exists int[] arr...... 不能进行静态检查，因此对于Path.java中只选取三个方法进行验证，具体代码如下：

package custompath;

import java.util.ArrayList;

public class Path {
    private /*@spec_public@*/ ArrayList<Integer> nodes;

    public Path(int... nodeList) {
        if (nodeList == null) {
            nodes = new ArrayList<Integer>();
        } else {
            nodes = new ArrayList<Integer>(nodeList.length);
            for (int i : nodeList) {
                nodes.add(i);
            }
        }
    }

    //@ ensures 
esult == nodes.size();
    public /*@pure@*/ int size() {
        return nodes.size();
    }

    /*@ requires index >= 0 && index < size();
      @ assignable 
othing;
      @ ensures 
esult == nodes.get(index);
      @*/
    public /*@pure@*/ int getNode(int index) {
        return nodes.get(index);
    }

    //@ ensures 
esult == (nodes.size() >= 2);
    public /*@pure@*/ boolean isValid() {
        return nodes.size() >= 2;
    }
}

• 使用cmd输入以下命令： 

java -jar D:OpenJmlopenjml.jar -prover cvc4 -exec D:OpenJmlSolvers-windowscvc4-1.7-win64-opt.exe -esc .Path.java

• 程序运行结束后，没有提示任何警告信息，说明设计符合规格。
• 或使用IDEA的OpenJml插件，运行结果如下：

      

• 没有提示任何错误或警告信息，说明设计符合规格。

JML UnitNG测试样例生成与分析

• 对于上述代码使用JML_UnitNG生成测试样例进行测试，在 cmd 中输入以下命令：

java -jar D:OpenJmljmlunitng.jar .Path.java -d .
javac -cp .;D:OpenJmljmlunitng.jar; .*.java
java -jar D:OpenJmlopenjml.jar -rac .Path.java
java -cp .;D:OpenJmljmlruntime.jar;D:OpenJmljmlunitng.jar; Path_JML_Test 

• 测试结果如下：

       

• 考虑到对于 getNode 方法中，没有对非法输入数据进行判定，因此将 getNode() 方法规格修改如下：

/*@ assignable 
othing;
      @ ensures (index >= 0 && index < size()) ==> (
esult == nodes.get(index));
      @ ensures (index < 0 && index >= size()) ==> (
esult == 0);
      @*/
    public /*@pure@*/ int getNode(int index) {
        if (index >= 0 && index < size()) {
            return nodes.get(index);
        } else {
            return 0;
        }
    }

• 测试结果如下：

       

三次作业总结

第九次作业

设计框架

• 第九次作业框架较为简单，设计的类按照规格进行设计，仅设计 RealPath 和 RealPathContainer 两个类，具体类图关系如下：

         

•  RealPath 类中各方法按照接口 Path 规格设计。
•  RealPathContainer 类中各方法按照接口 RealPathContainer 规格设计。

RealPath类

•  private ArrayList<Integer> nodes ：用于存储一条Path中的所有节点Id
•  private HashSet<Integer> diffnodes ：用于存储Path中所有不同的节点，Set的大小代表不同节点数
•  private int sum ：用于保存全部不同节点数，即 sum = diffnodes.size() 
•  private int code ：用于保存hashCode的值，即 code = nodes.hashCode() 

RealPathContainer类

•  private HashMap<Integer,Path> container ：用于存储Container中Path的ID到Path的正映射。即可以通过ID索引Path
•  private HashMap<Path,Integer> revcontainer ：用于存储Container中Path到Path的ID的负映射。即可以通过Path索引ID
•  private HashMap<Integer,Integer> nodes ：用于对所有Path包含的不同节点的计数，即Key为节点编号，Value为节点在Container中出现的次数。
•  private int counter ：用于对每一次新加入Container的Path进行编号。每次新加入一条新的Path，counter加一。

各方法具体设计实现

RealPath类

•  public int size() ：直接返回 nodes.size() 
•  public int getNode(int index) ：直接返回 nodes.get(index) 
•  public boolean containsNode(int nodeId) ：直接返回 diffnodes.contains(nodeId) ，因为HashSet的contains效率对于ArrayList一般情况下要快得多。
•  public int getDistinctNodeCount() ：直接返回 sum ，因为在构造方法时已经确定。
•  public boolean isValid() ：返回 nodes.size() >= 2 
•  public boolean equals(Object obj) ：根据规格，首先判断是否非空且为Path，再对obj中的每一个元素按顺序和当前的Path中每一个元素进行比对。
•  public int compareTo(Path o) ：对两个Path中每一个元素按照顺序进行字典序比对，返回结果。
•  public Iterator<Integer> iterator() ：直接返回 nodes.iterator() 
•  public int HashCode() ：直接返回 nodes.hashCode 

RealContainer类

•  public int size() ：直接返回 container.size() 
•  public boolean containsPath(Path path) ：先判断是否为空，之后返回 revcontainer.containsKey(path) 
•  public boolean containsPathId(int id) ：直接返回 container.containsKey(id) 
•  public Path getPathById(int id) ：若 container.get(id) 为空，抛出异常，否则返回其值。
•  public int getPathId(Path p) ：若Path不合法或者为空或者不存在，抛出异常，否则返回 revcontainer.get(p) 
•  public int addPath(Path p) ：若Path为空或不合法，返回0。之后查询Path是否已经存在，若存在返回旧id，否则将Path加入其中。对于加入新的Path，需要修改 container ， revcontainer ， counter ， nodes 。
•  public int removePath(path p) ：若Path不存在，则抛出异常，否则返回旧id，并且移除Path，修改的数据结构和addPath相似。
•  public Path removePathById(int id) ：操作类似 removePath ，不过查询方式为使用正映射。
•  public int getDistinctNodeCount() ：返回 nodes.size() 

第十次作业

设计框架

• 第十次作业设计框架采用沿用上一次作业设计的 Container 方式，在Container之上设计新的 RealGraph 类。因此 RealGraph 类采用继承RealContainer类的方式，完善Graph所需的功能，并且设计了新的类 VisitSet ，用于求最短路。
• 具体类图如下所示：  

         

• 各类中定义的数据结构以及具体功能如下：
• 对于RealPath类和RealContainer类均沿用于上一次作业，因此没有做任何改动。但对于父子类的沟通，为父类编写了一些 protected 的方法进行沟通。

RealGraph类

•  private HashMap<Integer,HashMap<Integer,Integer>> edges ：邻接边矩阵，用于存储邻接边计数。
•  private HashMap<Integer,HashMap<Integer,Integer>> map ：用于保存最短路结果的矩阵。
•  private boolean update ：用于标记是否需要更新 map 矩阵。对于不改变图总体结构的add或者remove过程，update为 false，但对于需要改变图总体结构的，需要为 true。

VisitSet类

• 该类设计主要是为了求最短路过程中保存已经走过的路的数据结构
•  private HashSet<Integer> visit ：用于保存当前结点已经走过的节点集合
•  private Integer now ：用于记录当前所在结点
•  private int size ：用于记录路径长度

各方法具体设计实现

RealGraph类

•  public int addPath(Path paht) ：首先调用父类addPath方法，记录返回值，并且对于add成功的路径进行邻接矩阵的修改。并且判断修改完邻接矩阵后是否需要更新最短路记录，若需要，则将map清空。
•  public int removePath(Path p) ：首先调用父类removePath方法，记录返回值，并且对于remove成功的路径进行邻接矩阵的修改，并且对于修改完邻接矩阵后图结构改变的时候，将map清空
•  public Path removePathById(int id) ：和上述方法类似
•  public boolean containsNode(int i) ：查询父类的 nodes 
•  public boolean containsEdge(int a,int b) ：查询邻接矩阵 edges 
•  public boolean isConnected(int a,int b) ：查询a到b的最短路，若存在，返回 true ，否则返回 false 
•  public int getShortestPathLength(int a, int b) ：首先判断对于a节点和b节点是否计算过最短路结果，若存在其中一个结点计算过但是查询不到a到b的最短路结果，说明a到b不连通，若存在结果，则返回；若两个结点均没有计算过最短路，则对a点为起点，计算最短路，并且返回结果。
•  private void addEdges(int a, int b) ：辅助方法，用于在addPath过程中更新邻接矩阵，计数邻接边。对于改变到图结构的，即开辟了一条新的邻接边，则设 update 为 true 
•  private void removeEdges(int a, int b) ：辅助方法，用于在remove过程更新邻接矩阵，过程类似 addEdges 
•  private int getRoadLen(int a, int b) ：辅助方法，用于查询map中a到b的最短路，对于查询不到的进行bfs算法更新最短路。

VisitSet类

•  VisitSet 类对于仅使用在计算最短路过程中，因此对于程序规格设计影响不大。主要设计思路为将其对象设计为不可变对象，对每一次bfs移动一个结点，需要重新new一个新的对象。

第十一次作业

设计框架

• 第十一次作业也采用保存上一次作业设计框架的模式，其中 RealRailwaySystem 类采用继承 RealGraph 类的方式，保存父类的数据结构以及一些方法实现，以及在此基础上新增了 UnionFindSet 类，并查集，用于计算图的连通性问题，新增 Pair 类，用于保存计算最短路过程的中间结果，新增RailMap类，用于保存地铁线路的真正的邻接矩阵， Road 类，路径类，保存三种路径的权值，包括不满意度，换乘数，票价， Station 类，用于描述不同的车站（对于所在Path不同或者结点号不同，即为不同车站）
• 具体类图结构如下：

         

• 各类设计的数据结构如下：

RealRailwaySystem类

•  private RailMap railMap ：用于记录地铁网络的邻接矩阵
•  private HashMap<Integer,HashMap<Integer,Integer>> priceMap ：用于保存计算最低price的矩阵
•  private HashMap<Integer,HashMap<Integer,Integer>> transMap ：用于保存计算最少换乘的矩阵
•  private HashMap<Integer,HashMap<Integer,Integer>> unpleasantMap ：用于保存计算最少不满意度的矩阵

UnionFindSet类

• 该类用于计算图的连通性问题，设计采用单例模式，所有查询方法均为静态方法
•  private HashMap<Integer,Integer> map ：用于记录每一个结点所在连通块的父节点，初始化为自己
•  private HashMap<Integer,Integer> size ：用于记录该父节点连通块上的结点数
•  private int realsize ：用于保存该图的连通块数
•  private boolean update ：用于记录是否需要更新 realsize 

Station类

• 该类用于描述不同的结点类
•  private int nodeId ：该站的结点编号
•  private int pahtId ：该站的路径编号，0为起点，-1为终点，用于后续求最短路服务

Road类

• 该类用于记录三种不同路径的权值
•  private final int price ：路径中票价权重
•  private final int transfer ：路径中换乘次数
•  private final int unpleasant ：路径中不满意度

RailMap类

• 该类用于保存真正的地铁网络中的邻接矩阵
•  private HashMap<Station,HashMap<Station,Road>> ：记录地铁站到地铁站之间的路径以及权值

Pair类

• 该类用于描述迪杰斯特拉求最短路途中的中间结果，因此用于保存当前走到的节点以及最短路大小。并且该类实现了 Comparable 接口，方便迪杰斯特拉做对应的堆优化。

各方法具体设计实现

RailMap类

• 由于该类用于保存站与站之间的邻接矩阵，因此需要为矩阵操作提供一些方法接口
•  public void putEdges(Station a, Station b) ：该方法将a站到b站的邻接边更新到map中。对于第一次加入的新节点，需要建立起点站以及终点站，即0号站和-1号站，为后续迪杰斯特拉做好构图准备。构图思路为：每一个结点均有与一个0号点连接的无向边，对于站点到0号点，边权不为0，对于0号点到站点，边权为0，同时也有一个到-1号点的有向边，边权为0
•  public Set<Station> canGo(Station a) ：该方法用于通过邻接矩阵的横坐标索引，返回矩阵这一行所有的元素集合。即代表a站能够到达的所有站。
•  public Road getRoad(Station a, Station b) ：该方法用于返回a站到b站之间邻接边Road，前置条件保证调用该方法前a和b存在邻接边。

UnionFindSet类

• 该类使用并查集算法，对于addPath行为，直接将邻接边加入并查集中并进行路径压缩，若remove行为，则先判断是否改变了图结构，即是否完全移除了一条邻接边，若移除了，则将并查集清零，从头开始进行计算
•  public static int findRoot(int a) ：寻找a结点的父节点，并且进行路径压缩、
•  public static void union(int a, int b) ：将a和b的邻接边加入到并查集中
•  public static int size() ：返回并查集记录的连通块个数
•  public static boolean isConnected(int a, int b) ：查询并查集，判断两个结点是否连通

RealRailwaySystem类

•  public int addPath(Path p) ：首先调用父类add方法，记录返回值，对于add成功的Path，将邻接边加入到 railMap 中
•  public int removePath(Path p) ：调用父类remove方法，记录返回值，对于remove成功的Path，更新 railMap 。即对remove的id删去对应的所有Station
•  public void removePathById(int id) ：调用父类方法，其他过程同上述方法
•  public int getLeastTicketPrice(int a, int b) ：使用迪杰斯特拉最短路算法，计算a到b的最短路径，邻接矩阵为 railMap 。使用 Pair 类记录中间结果并且存到堆中，并且更新结果矩阵。
•  public int getLeastTransferCount(int a, int b) ：同上
•  public int getLeastUnpleasantValue(int a, int b) ：同上
• 求最短路原则：首先查询是否已经求过a和b的最短路，若其中一个结点已经计算过，如果仍找不到a到b最短路结果，说明a和b不连通，若有结果，则返回；若两个结点均没有计算过，则计算
• 更新 raiMap 原则：每一次addPath和remove操作，若成功，对 railMap 进行更新，即增加或删去对应PathId的所有Station

测试和bug修复

• 本单元三次作业主要采用两种方式进行测试，分别对应编写程序过程中的单元测试，以及程序编写结束后的对拍测试。

单元测试

• 单元测试的方式采用的是使用JUnit4进行单元测试。在IDEA中安装对应的JUnit4插件和jar程序包。安装结束后可以正常使用。
• 首先对于要测试的类创建单元测试类。以第十次作业为例，对 RealGraph 类建立单元测试类。将光标移动到类名处，之后使用快捷键 Shift+Ctrl+T ，调出如下窗口：  

        

• 选择创建新测试类之后，创建对应的Junit4类，就可以编写对应的测试方法。
• 对于第十次作业，主要使用Junit4单元测试了 addPath 和 getShortestPathLength 方法，具体代码如下：

package test.java.graph;

import com.oocourse.specs2.models.Graph;
import com.oocourse.specs2.models.NodeIdNotFoundException;
import com.oocourse.specs2.models.NodeNotConnectedException;
import graph.RealGraph;
import graph.custompath.RealPath;
import org.junit.After;
import org.junit.Before;
import org.junit.Rule;
import org.junit.Test;
import org.junit.rules.Timeout;

import static org.hamcrest.CoreMatchers.is;
import static org.junit.Assert.*;

public class RealGraphTest {
    private Graph testGraph;

    @Before
    public void setUp() throws Exception {
        testGraph = new RealGraph();
    }

    @After
    public void tearDown() throws Exception {
        System.out.println("end");
    }

    @Rule
    public Timeout timeout = Timeout.millis(100);

    @Test
    public void addPath() {
        try {
            assertEquals(1,testGraph.addPath(new RealPath(1,2,2,3)));
            assertEquals(2,testGraph.addPath(new RealPath(2,2,3)));
            assertEquals(1,testGraph.addPath(new RealPath(1,2,2,3)));
            assertEquals(0,testGraph.addPath(new RealPath(1)));
        } catch (Exception e) {
            fail("Wrong result!");
        }
        System.out.println("success");
    }
    
    @Test
    public void getShortestPathLength() {
        try {
            assertEquals(1, testGraph.addPath(new RealPath(1,2,2,3,6,-1,3,4)));
            assertEquals(2,testGraph.addPath(new RealPath(2,3,2,4,5,1,4,0)));
            assertEquals(3,testGraph.addPath(new RealPath(5,6,4,2,0,4,7,2,3,7,7,8,20)));
            assertEquals(4,testGraph.addPath(new RealPath(30,40,-4,-7)));
        } catch (Exception e) {
            fail("Before construct!");
        }
        try {
            assertEquals(0,testGraph.getShortestPathLength(2,2));
            assertEquals(1,testGraph.getShortestPathLength(2,4));
            assertEquals(4,testGraph.getShortestPathLength(1,20));
        } catch (Exception e) {
            fail("Catch unexpected Exception");
        }
        try {
            testGraph.getShortestPathLength(1,-7);
            fail("Uncatch Exception!");
        } catch (NodeNotConnectedException e) {
            assertThat(e.getMessage().trim(),is("Node 1 and -7 not connected."));
        } catch (Exception e) {
            fail("Wrong Exception");
        }
        try {
            testGraph.getShortestPathLength(30,50);
            fail(("Uncatch Exception"));
        } catch (NodeIdNotFoundException e) {
            assertThat(e.getMessage().trim(), is("Node id not found - 50."));
        } catch (Exception e) {
            fail("Wrong Exception");
        }
    }
}

• 其中为了测试最短路算法的效率，还增加了时间限制 @Rule 一项。运行测试类，结果如下： 

        

• 对于第十一次作业也使用了类似方法，不再重述。

对拍测试

• 对于每一单元的作业，每次完成程序后都需要对程序进行对拍测试以保证程序的正确率。单元测试仅能测试单独方法的功能，对拍测试可以使用大数据量对程序进行测试。

• 本单元的对拍器主要有四个部分组成，分别是数据生成器 data_make.py ，调度程序器 feeder.py ，对拍验证程序 spec_judge.py ，是一个纯py互相配合的对拍器。

• 显然本次作业的对拍重要的在于数据生成器的构建。这三次作业数据生成器主要设计了三种模式针对不同的测试：

  • 随机测试：在每一条addPath和remove类型指令之间插入若干条不同的查询指令。
  • 稀疏图测试：该模式主要针对于第二次和第三次作业，对于每一次addPath的Path规模并不大，大概在2到20个结点之间，保证多条Path之间能够构成多个连通块，以测试对于图的维护和查询。
  • 针对查询测试：该模式主要测试remove指令执行后查询相关条件，是否会造成错误，也是测试图维护的一种数据。
  • 压力测试：该模式中大部分指令为最短路查询等耗时长的指令测试，以及所有结点数均调大最大饱和状态，主要测试最短路算法的正确性和效率。

• 上述几种数据模式基本能够测试出本单元作业所有bug的存在。

三次作业发现的bug

• 对于前两次作业，在公测和互测均没有发现bug，对于第三次作业，在公测中发现了较为大的bug。该bug的发现由对拍器和强测同时发现。

• 第三次作业中，addPath方法对邻接矩阵维护不恰当，导致bug的发生。

  • 每一次add方法执行后对于自己到自己的邻接边没有加入到邻接矩阵中，导致在邻接矩阵查询过程中会触发 NullPointerException 的问题。
  • 每一次add方法执行后，没有判断add是否成功，就将邻接边更新到 railMap 中，导致了 railMap 维护出错。

• 对于该bug的修复只需要在addPath方法中加入对是否add成功做判断，若不成功，直接返回，以及在从邻接矩阵中获取邻接边时，要对get为null的返回一个空Set。

心得体会

• 这一单元JML的学习，感悟很深，学到的东西有很多，不仅仅在于认识了规格化编程这一概念，体验了规格化编程的概念，也认识学习使用了一些检查规格正确性的程序。规格化的编程让我更好的理解了面向对象编程的概念，同时也知道如何写代码能够让自己的代码更为美观。
• 在程序测试方面，认识了单元测试这一概念，也学会了使用Junit4的方式对代码的基本功能进行单元测试。对于对拍器的构建也将重心转移到了测试数据生成方面，学会思考如何使用正确的数据生成方式，生成更有针对性的数据。