OO_Unit3_JML规格模式

标签：details   结果   检测   构造   因此   rri   pre   方法   最小生成树   

---恢复内容开始---

CSDN博客链接
@

一、JML语言的理论基础及应用工具链

（一）定义：

JML(Java Modeling Language)：对Java程序进行规格化设计的一种表示语言。JML是一种行为接口规格语言 （Behavior Interface Speci?cation Language，BISL），基于Larch方法构建。BISL提供了对方法和类型的规格定义
手段。所谓接口即一个方法或类型外部可见的内容。

（二）契约式设计核心思想：

软件系统中的元素之间相互合作以及“责任”与“义务”

1. 期望所有调用它的客户模块都保证一定的进入条件：这就是函数的先验条件—客户的义务和供应商的权利，这样它就不用去处理不满足先验条件的情况。
2. 保证退出时给出特定的属性：这就是函数的后验条件—供应商的义务，显然也是客户的权利。
3. 在进入时假定，并在退出时保持一些特定的属性：不变式。

method A(){
   assert(前置条件)
    do something
   assert(后置条件)
   return 
}

（三）特点：

1. 跳过方法的实现，直接描述方法的功能
2. 规范化的注释，并且能够被自动检测正确性

（四）用法：

具体使用详见《JML Level 0手册》

1. 开展规格化设计。这样交给代码实现人员的将不是可能带有内在模糊性的自然语言描述，而是逻辑严格的规
   格。
2. 针对已有的代码实现，书写对应的规格，从而提高代码的可维护性。这在遗留代码的维护方面具有特别重要的意义。

（五）工具链：

1. 使用到IDEA的OpenJML插件，检查JML是否符合规格gitHub下载地址
   openJML。
2. 使用JUnit生成测试样例，进行单元化测试

二、部署SMT Solver并验证

很遗憾，电脑不兼容openJML，按照教程严格执行，却一直失败：

1. 下载时出错：
   
2. 配置时出错：
   用IDEA导入包时不能识别

三、JMLUnitNG/JMLUnit自动生成测试用例

（一）对Edge类的hashCode进行测试

• 源码：

public int hashCode() {
    int[] array = new int[3];
    array[0] = min;
    array[1] = max;
    array[2] = pathId;
    return Arrays.hashCode(array);
}

• 测试：

@Test
public void hashCodeTest() {
    assertNotEquals(new Edge(-69,54,1).hashCode(),
            new Edge(-68,23,1).hashCode());
    //Values should be different. Actual: -34843
    
    HashSet<Integer> set = new HashSet<>();
    for (int i = -50; i < 50; i++)
        for (int j = -50; j < 50; j++) {
            Edge edge = new Edge(i, j, 1);
            set.add(edge.hashCode());
        }
    assertEquals(set.size(), 5050);
    //java.lang.AssertionError: 
    //    Expected :2704
    //    Actual   :5050      i!=j: (100+1)*100/2
}

• 结果：发现此hashCode生成不能满足需求，使得两个不同的边hashCode的值不同
• hashCode与equals具有以下规范：
  1. 若重写equals(Object obj)方法，有必要重写hashcode()方法，确保通过equals(Object obj)方法判断结果为true的两个对象具备相等的hashcode()返回值。
  2. 如果equals(Object obj)返回false，即两个对象“不相同”，并不要求对这两个对象调用hashcode()方法得到两个不相同的数。
  3. Java运行时环境是怎样判断HashSet和HastMap中的两个对象相同或不同：先判断hashcode是否相等，再判断是否equals。
• 修正：
  反hash（希望建立一个hashCode到Edge本身一一对应的映射）的前提：任何两个同类型不同的对象的哈希值不同

public int hashCode() {
    return (min + "," + max + "," + pathId).hashCode();
}

（二）针对Graph接口的测试用例

@Test
    public void getLeastTransferCountTest() {
        Path path = new MyPath(1,2,3);
        MyRailwaySystem system = new MyRailwaySystem();
        system.addPath(path);
        path = new MyPath(2,4,5,6);
        system.addPath(path);
        path = new MyPath(3,5);
        system.addPath(path);

        try {
            assertEquals(system.getLeastTransferCount(1,6),1);
            //java.lang.AssertionError: 
            //Expected :2
            //Actual   :1
        } catch (Exception e) {
            e.printStackTrace();
        }
    }

根据说明信息，发现在dijstra更新过程中出现错误，在bug修复处分析了具体原因及解决方式。

四、架构设计

（一）类图设计

本单元作业要求依次实现四个类：

• 使用Path接口的MyPath
• 使用PathContainer接口的MyPathContainer
• 使用Graph接口的MyGraph
• 使用RailwayStation接口的MyRailwayStation

其中，MyPathContainer是MyPath的容器，并且实现了MyGraph的部分功能。因此，MyGraph中以MyPathContainer作为组成元素之一。同理，MyRailwayStation将MyGraph作为组成元素之一。各类包含关系如下：

在后续迭代过程中，不对前面实现过的类进行修改，仅是扩展添加新的属性及方法（遵循OCP原则：面对需求，对程序的改动是通过增加新代码进行的，而不是改变原来的代码。）

（二）算法设计

本次作业比较关键的几个方法为：

1. MyPathContainer.getDistinctNodeCount()

• 不能在每次接到指令DISTINCT_NODE_COUNT时都重新计算一遍，所花的时间复杂度是不能承受的。最开始我就是直接遍历，导致第一次强测爆40
• 需要有一个图来存每一个节点信息：

private HashMap<Integer, Integer> nmap = new HashMap<>();
//node的容器<node,number（node出现在各个路径中的次数）>

• 每次加入或删除路径时对其更新
• 接到指令DISTINCT_NODE_COUNT时直接返回nmap.size();

1. MyGraph.getShortestPathLength(int fromNodeId, int toNodeId)

• 使用到BFS：一种单元扩张的搜索方式。其适用的前提是保证value严格递增。
• 并且BFS的时间复杂度对单源是o(v+e)，对全图搜索复杂度为o(v(v+e))
• 需要有一个邻接链表存储点之间关联关系（使用到键为node，值为边集合的HashMap，因此还需要设一个建立从边的hash值到边本身的映射），一个距离矩阵来存储距离信息：

private HashMap<Integer, HashSet<Integer>> linkMap;
private HashMap<Integer, HashMap<Integer, Integer>> disMap;
private HashMap<Integer, Edge> edgeMap;//hashCode(edge)-->edge(a,b)

• 其中距离矩阵是周密矩阵：第二次限制|node|<=250，第三次限制|node|<=120
• 此处存距离的disMap其实直接用矩阵存储的时空效率更高
• 接下来是对单源距离图的更新：需要fromSet, nextSet进行广度优先搜索，每次将fromSet所连接而未到达的点放入nextSet，算法较为简单

1. MyRailwayStation.getLeastTicketPrice(int fromNodeId, int toNodeId)
   MyRailwayStation.getLeastTransferCount(int fromNodeId, int toNodeId)
   MyRailwayStation.getLeastUnpleasantValue(int fromNodeId, int toNodeId)

• 使用到dijstra方法：类似于最小生成树，是BFS的升级版，应用到邻接链表，其算法复杂度也是o(v+e)
• 用到的数据结构需要记录到达的节点，以及将要到达的节点
• 设置新的数据结构Node，组成链表结构：是四元组<node(Integer),value(Integer),edge(Edge),next(Node)>
• 正在到达的节点arrived为(next=null)的Node类型，将要到达的节点nextSet为Node类型的邻接链表，并且加入时按照value值递增
• dijstra的过程如下：
  1. 初始化：nextSet=new Node(0,0,null);nextSet.add(new Node(node,0,null));
  2. 将nextSet的首节点移出设置为arrived
  3. 遍历arrived连接的所有边并加入nextSet：for(Integer edgeHashCode: linkMap.get(arrive.getNode()))
  4. 根据arrived更新对应的最小单元图
  5. 跳回第二步，直到nextSet为空集
• 事后考虑到v=|node|<=120，而e=|edge|<=4000，实际上o(v^3)优于o(v(v+e))，使用floyed算法的效率要比dijstra效率高，事实也是如此，并且floyed算法要比dijstra简便很多

（三）代码复杂度分析

1. 依赖关系

均在正常范围内

1. 方法复杂度（显示超标）

其中MyRailwaySystem.renewNodeMap方法，即对于单源的dijstra方法长50行，为了兼容3个搜索，分支很多，而错误也正是出现在这里。

以后任意一个方法，行数最好不要超过30行，秉承SRP（单一职责原则），只做出一个行为，然后通过封装和组合达到最终实现行为的目的。

五、bug修复

（一）Edge类的hashCode错误

（前面已经测试过）

（二）换乘问题

• 要注意的是设有换乘，因此dijstra过程中不可避免碰到了如下问题：
• 构造一个简单的测试用例（前面进行了测试）
  
  如果严格按照之前的过程，会出现一个意想不到的问题：

1. 遍历node=1，nextSet: (2,0,1/2)
2. 遍历node=2, nextSet: (3,0,2/3)->(4,1,2/4)
3. 遍历node=3, nextSet: (5,1,3/5)->(4,1,2/4)
4. 遍历node=5, nextSet: (4,1,2/4)->(6,2,5/6) //->(4,2,4/5)
5. 遍历node=4, nextSet: (6,2,5/6) //->(5,1,4/5)
6. 遍历node=6, nextSet: null

最后发现node=6处value为2，实际上value应该为1

• 解决方式：
  • 在第4步，发现将要加入的(4,2,4/5)与(4,1,2/4)冲突（同node，同path，不同egde）时，加入较大者的新节点(5,1,4/5)，得到nextSet: (5,1,4/5)->(4,1,2/4)->(6,2,5/6)
  • 第5步：遍历node=5, nextSet: (4,1,2/4)->(6,1,5/6) （第二次遍历，注意更新）
  • 第6、7步：同上5、6

（三）null指针

在HashMap数据结构中，如果访问的key值不在其中，函数会返回null，而不是抛出异常，而后对null调用函数会报错NullPointerException。因此在这里常常出现诡异的bug，以后使用get时要小心，更好的方式是使用getOrDefault，没有key值就给出默认的数据。

此外，对于HashMap套HashMap现象，连续使用两次get()，会造成意想不到的错误，不如先将乱序节点通过一个HashMap映射到从1开始的正整数上，然后直接使用二维静态数组。

六、心得体会

JML是一种先进的契约式设计模式，将设计和实现不可跨越的鸿沟大幅减小。大体上解决问题分为从需求到设计，从设计到实现两个过程。而JML规范地描述了代码需要执行的约束条件，可以说是一种LLR(Low-Level Request)。

实际上，个人感觉JML更偏向于需求，而非设计。因为不管是你需要具体的数据结构，还是算法，都需要个人亲自去定义。并且为了描述一个需求，用大段大段的代码去规范和描述也不是一个简单的任务。很可能需要多层抽象，甚至有时根本找不出一个描述需求的严格的表达方式。写规格本身都要比实现一个需求难上许多。

但是比较受用的是自动测试生成JUnit，对类中的某一个具体的函数进行测试。虽然直接在控制台输入输出也很有效，但那样测完一次就结束了，没有办法对测试集进行管理。也没有办法在扩展修改了类以后保证类的兼容性。

总之，这一个单元是相当革新的，业界缺乏成熟的代码规格化设计方式，网络上对契约式设计也鲜有听闻，但是以后可能会日渐成熟。

---恢复内容结束---

OO_Unit3_JML规格模式

标签：details   结果   检测   构造   因此   rri   pre   方法   最小生成树   

原文地址：https://www.cnblogs.com/RyanSun17373259/p/10908267.html