面向对象第三单元总结

Posted 2021-12-02 lchbuaa2017

面向对象第三单元总结

一、JML

JML理论基础

Java 建模语言（JML）将注释添加到 Java 代码中，这样我们就可以确定方法所执行的内容，而不必说明它们如何做到这一点。有了 JML，我们就可以描述方法预期的功能，无需考虑实现。JML 为说明性的描述行为引入了许多构造。这些构造包括模型字段、量词、断言的可见度范围、前提条件、后置条件、不变量、合同继承以及正常行为与异常行为的规范，这些构造使得 JML 的功能变得非常强大。一般而言，JML有两种主要的用法：
（1）开展规格化设计。这样交给代码实现人员的将不是可能带有内在模糊性的自然语言描述，而是逻辑严格的规 格。
（2）针对已有的代码实现，书写其对应的规格，从而提高代码的可维护性。这在遗留代码的维护方面具有特别重要 的意义。

JML应用工具链

JML是一种为Java 量身定做的形式化的行为接口规范语言，用来规范Java 程序模块(如类和接口)的行为及详细设计决策。使用JML书写的形式化的接口规范可以推动程序的自动化测试，减少单元测试的负担。目前，许多基于JML的验证、调试和测试工具已经非常成熟，例如OpenJML、JMLUnit、JMLUnitNG等等。利用这些支撑工具JML规范可以被翻译为可识别的程序代码，可以进行测试框架、测试用例等的自动生成。

二、SMT Solver

三、JMLUnitNG/JMLUnit

比较简单的例子，测试两个int变量的加减乘除运算

可以看出，Jmlunitng主要用int范围的临界值，来生成测试样例。在div方法中，有潜在除于0的风险，被自动测试测出。从Jmlunitng生成的测试数据来看，其仍有改进的地方。

四、架构设计

三次作业分别实现了PathContainer,Graph,RailwaySystem。三次作业的层次关系比较明显，好的架构设计能够较为容易实现迭代开发。

第一次作业主要涉及路径容器的基本操作，实现增删查等功能。具体实现是：MyPath用一个ArrayList和HashSet来存储Path的结点。ArrayList用于返回迭代器，getNode操作；HashSet用于containsNode操作。MyPathContainer用两个HashMap(pidmap，pmap)来存储Path，分别用PathId和Path作为键，原因是HashMap在增删查方面的时间复杂度都比较低，这里采用了以空间换时间的设计。第一次作业比较简单，按照JML规格来写代码，基本没什么问题。

第二次作业由PathContainer扩展为Graph，增加了一些关于图的基本概念与算法——是否包含某条边（containsEdge）、两个节点是否连接（isConnected）和计算两个节点的最短路径（getShortestPathLength）。涉及到图，首先考虑图如何存储，因为在任何时候总结点个数都不超过250个，所以可以采用邻接矩阵的方式存储（需要建立节点和邻接矩阵下标之间的映射关系）。根据节点和邻接矩阵下标的对应关系，就能够判断某条边是否存在。图的最短路径算法有Dijkstra求单源最短路径、BFS广度优先寻找最短路径和Floy求多源点最短路径。考虑到图变更的指令最多只有20条，因此只要在变更时跑一遍Floyd，之后的查询时间复杂度是O(1)，而且能根据Floyd的结果判断两个节点是否连通。这样下来，整体的时间复杂度并不高。

第三次作业在第二次作业基础上实现RailwaySystem，新增了计算无向图连通块的数目，两个节点之间的最低票价、最少换乘次数和最小不满意度。这次作业我认为较难的就是对换乘的处理，最后的解决方案是先对每个Path中的任意两点求出三个最优解（最低票价、最少换乘和最少不满意度）此时不需要换乘；然后遍历所有的Path，对具有相同起点和终点的最优解进行刷新，放入邻接矩阵中；最后邻接矩阵的具有相同起点和终点的最优解进行刷新，此时可能需要换乘。由于第二次作业的扩展性比较差，因此我进行了重构设计，新建一个Edge类，其数据成员有exist（边的存在性），length（两个节点的最短距离），transfer（两点的最少换乘），price（两点的最低票价），unpleasent（两点的最少不满意度）；新建一个PathInfo类，存放路径的Id和每个Path中任意两个节点之间Edge的信息；MyRailwaySystem类中用HashMap(graph)来存储路径，其key是Path，Value是PathInfo。只需对邻接矩阵matrex(其元素是Edge)，用一次Floyd算法，就能计算出三个最优解。节点之间的连通性计算出来之后，遍历所有节点，把能连通的放到一个集合，集合的个数就是连通块的数量。

五、代码实现的bug与修复

三次作业在强测中都出现bug。第一次作业是因为cpu超时，在bug修复时，我对HashMap变量都设置初始容量之后，能够通过测试点。第二次作业是因为在执行Path_Remove指令时，有时会错误更新图的邻接矩阵信息。具体修复是用二维数组存放两个节点边的数量，在执行Path_Add时对Path包含的边对应数组中的元素进行加1的操作，同理在执行Path_Remove时，对Path中包含的边进行减1的操作。第三次作业是触发空指针异常，在bug修复时，对要访问的变量先判断是否为null，然后进行访问。

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

通过两次实验对JML规格的撰写和作业根据规格完成程序，我进一步认识了规格。我们在平时写程序时，很少做到先写规格再功能实现，但使用JML来声明性地描述一个方法或类的行为可以显著提高整体的开发进程。把规格加入到Java程序中有以下好处：

• 能够更为精确地描述方法和类要实现的功能是什么（避免自然语言在描述时可能产生的歧义）
• 能够高效地发现和修正程序中的bug（方法执行前后哪些变量的状态发生变化是确定的）
• 可以在应用程序升级时降低引入bug的机会
• 可以提供与程序代码完全一致的JML格式的文档