OO_Unit3_JML规格模式

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

[CSDN博客连接](https://blog.csdn.net/weixin_43387647/article/details/90451173) @[toc] ## 1、JML语言的理论基础及应用工具链 #### （一）定义： JML(Java Modeling Language)：对Java程序进行规格化设计的一种表示语言。JML是一种行为接口规格语言 （Behavior Interface Specification 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生成测试样例，进行单元化测试

2、部署SMT Solver并验证

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

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

3、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修复处分析了具体缘由及解决方式。

4、架构设计

（一）类图设计

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

• 使用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();

2. 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，算法较为简单

3. 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. 依赖关系

Class	Cyclic	Dcy	Dcy*	Dpt	Dpt*
Edge	0	0	0	3	5
Main	2	2	6	2	3
MyGraph	2	3	6	1	3
MyGraphTest	0	0	0	0	0
MyPath	0	0	0	2	4
MyPathContainer	0	0	0	1	4
MyRailwaySystem	2	4	6	2	3
MyRailwaySystemTest	0	2	7	0	0
Node	0	1	1	1	4

均在正常范围内

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

Method	ev(G)	iv(G)	v(G)
MyGraph.isConnected(int,int)	4	2	5
MyGraph.nodeEdgeOk(int)	4	3	4
MyRailwaySystem.getLeast(int,int,int)	5	3	5
MyRailwaySystem.renewNodeMap(int,int)	3	13	14
Node.add(Node)	5	6	6

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

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

5、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) （第二次遍历，注意更新）
  • 第六、7步：同上五、6

（三）null指针

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

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

6、心得体会

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

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

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

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

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