一、JML语言的理论基础

　　面向对象分析和设计的原则之一就是应当尽可能地把过程设想往后推。我们大多数人只在实现方法之前遵守这一规则。一旦确定了类及其接口并该开始实现方法时，我们就转向了过程设想。

　　Java 建模语言(JML)将注释添加到 Java 代码中，这样我们就可以确定方法所执行的内容，而不必说明它们如何做到这一点。有了 JML，我们就可以描述方法预期的功能，无需考虑实现。通过这种方法，JML 将延迟过程设想的面向对象原则扩展到了方法设计阶段。

二、JML应用工具链

　　openJML可以检查规格是否符合JML语法规则。

　　SMT SOLVER可以验证jml规格和java代码的等价性。

　　JMLUnitNG可以实现自动生成生成测试样例进行测试。

三、JMLUnitNG自动生成测试用例

　　自己编写了一个简单的规格和方法后按照讨论区的指导进行了测试样例生成：

package demo;

public class Demo {
    /*@ public normal_behaviour
      @ ensures \result == a + b;
    */
    public static int sum(int a, int b) {
        return a + b;
    }

    public static void main(String[] args) {
        sum(1418941,152525);
    }
}

　　可以看出JMLUnitNG生成的测试样例都是边界值（最大int值、最小int值）和0。

四、作业架构设计

　　1.第九次作业

　　（1）Path使用ArrayList存储路径和不同的点。

　　（2）PathContainer设一个计数器counter生成id，使用HashMap<Integer, Path>存储id-Path键值对，用ArrayList存储容器中不同的点，设一个布尔型标志位标记不同的点的列表是否最新。

　　2.第十次作业

　　（1）Path沿用上次的设计。

　　（2）新建一个图计算类CalMap进行图相关的操作，在其中设标志位newest标记图结构是否最新，用邻接表HashMap<Integer, ArrayList<Integer>>存储图结构（id-邻接id列表键值对），用HashMap<Integer, HashMap<Integer, Integer>>存储最短路径缓存（id-<id-distance>键值对）。进行图相关查询时先根据newest决定更新（清空缓存，重建邻接表）与否，再进行查询（先查缓存，没有再进行计算）计算点对间最短距离时，用bfs计算单一源点到连通的所有点的最短距离，并将结果存入缓存。

　　（3）Graph继承PathContainer，在Graph中构造一个CalMap图计算对象，重写图结构变更方法（在图结构变更后将图计算对象的newest赋值false），进行图相关查询时直接调用图计算对象的接口。

　　3.第十一次作业

　　（1）Path除新增计算不满意度方法外不变。

　　（2）RailwaySystem继承Graph，新增的各种查询仍然调用CalMap类的相关接口来实现。

　　（3）主要更改CalMap这个图计算类。CalMap类要实现 1)存储地铁线路图；2)实现各种相关查询：①连通块个数②两站间最低票价③两站间最少换乘④两站间最小不满意度。

　　为存储线路图将每个点拆分为一个总站和经过该站线路数个站台，总站与该站的所有站台相连，每一条线路上相邻站台相连（新建Station类，根据节点号和和线路id实现拆点，总站对应线路id为0），采用无权无向图存储地铁线路图。

　　在查询连通块个数以及两站之间最低票价时直接在线路图上采用bfs，将得到的最低票价信息存入最低票价缓存（查询连通块个数时会得到一些点对之间的最低票价信息，另外这里的计算结果比实际票价大2）；

　　为查询最少换乘，根据线路图建一张总站与该站所有站台之间权为1，其它边权为0的带权无向图，在这张图上查询最短路径，并将中间结果存入最少换乘缓存（结果比实际结果大2）；

　　为查询最小不满意度，根据线路图和不满意度计算方法建立对应的带权无向图（总站与该站所有站台之间权为64/2=32），在这张图上查询最短路径，并将中间结果存入最少换乘缓存（结果比实际结果大64）。

五、bug分析和修复

　　第一次作业没有考虑到复杂度的问题，没有在PathContainer中维护一个容器包含的不同点的列表，每次查询不同点的个数以及是否包含某点时都要遍历一遍pathList，导致大部分测试点cpu时间超时。修复：维护一个distinctNodeList和newestDistinct（初始化为空列表和 true）,分别代表不同点的列表和该列表是否是最新的，在每次增加了路径时将这条路径中不在distinctNodeList中的点加入，在每次删除了路径后将newestDistinct置为false，在每次查询不同点的个数或是否包含某点时，如果newestDistinct为false则用pathList更新distinctNodeList，然后用distinctNodeList完成查询。

　　第二次作业在建立邻接表时犯了一个低级错误，导致每一条路径的第一个点会产生一个自环，所以当加入一条第一个点本没有自环的路径后，查询是否包含第一个点到第一个点的边，我的程序会给出yes，但事实上应该是no（例如 PATH_ADD 1,2　　CONTAINS_EDGE 1,1）。虽然说在第二次强测中侥幸得到满分，但是第三次强测暴露了这个问题，对建立邻接表的细节处理了一下后解决了这个问题。

六、规格撰写和理解上的心得体会

　　1.方法规格撰写时不应该注重如何实现方法，而应该偏重于方法的使用条件，会达到什么效果，应该是一个“去过程化”的操作。

　　2.撰写规格时应该尽量层次清晰、条理分明，这样写出来的规格既不容易出错又有很高可读性。

　　3.理解规格时按照jml的语法规则，分层次有条理地去看，就不会有障碍。

原文地址：https://www.cnblogs.com/Raze11he/p/10890267.html