OO第三单元总结

桃扇骨 2021-12-01 17:18 251阅读 0赞

# OO第三单元总结 #

### 综述 ###

这一单元的内容，相比以往，难度有所降低。但是，依旧在算法，数据结构和逻辑设计等部分上有着不少的难点。由于自己的一些怠惰，导致这三次作业没有太多地去处理整合抽象的过程，而是只在大脑中抽象地想好了步骤，然后就直接在一个类中实现了。

### JML梳理 ###

##### JML语言 #####

JML语言是一种java的规格描述语言。它可以无二义性地描述一个类或者方法的行为，并且对类的行为进行规约。从而在具体实现一个类或方法之前，首先了解到其预期功能和行为，提高工程实现的效率。

这个单元里常用的规格部分包括以下几部分

*  前置条件调用者在调用方法时，必须确保满足前置条件，否则无法完成相应功能。通过requires子句表示
 *  后置条件 方法在执行时，如果满足前置条件，则结果必须满足后置条件。通过ensures子句表示 
 *  可变元素 方法在执行过程中，可以进行修改的元素数据。通过assignable子句表示
 *  异常行为 方法在执行时，遇到特殊情况，需要抛出的异常和相关处理。通常用signals子句表示

##### JML工具链 #####

*  OpenJML 
    
     *  检查JML中使用规范注释的Java程序，并为JML的许多功能提供强大的支持。
     *  支持静态和运行时检查。运行时断言检查通常更容易编写规范，而静态检查可以更好地保证程序行为。
     *  与SMTSolver集成，可以使用Z3，CVC4和Yices等对代码逻辑进行证明。

*  JMLUnitNG
    
     *  基于JML注释的Java代码的自动化单元测试生成工具。
     *  生成的测试使用TestNG单元测试框架。可以自己运行（或假设适当配置的CLASSPATH）或作为更大的TestNG套件的一部分。

### JMLUnitNG部署 ###

作为一次简单的测试，先准备了一个简单的测试文件Add.java。

1 public class Add {
     2     /*@ public normal_behaviour
     3       @ requires a > 0 && b > 0;
     4       @ ensures \result == a + b;
     5       @*/
     6     public static int add(int a, int b) {
     7         return a + b;
     8     }
     9 
    10     public static void main(String[] args) {
    11         add(1, 1);
    12     }
    13 }

首先，对JML语言进行检查确认无误。

1 java -jar ../openjml/openjml.jar -check Add.java > re.txt

之后，按照评论区大佬的方法进行文件生成和编译

1 java -jar jmlunitng-1_4.jar Add.java 
    2 javac -cp jmlunitng-1_4.jar *.java
    3 java -jar ../openjml/openjml.jar -rac Add.java
    4 java -cp jmlunitng-1_4.jar Add_JML_Test

最终结果为

1 [TestNG] Running:
     2   Command line suite
     3 
     4 Passed: racEnabled()
     5 Passed: constructor Add()
     6 Failed: static add(-2147483648, -2147483648)
     7 Passed: static add(0, -2147483648)
     8 Passed: static add(2147483647, -2147483648)
     9 Passed: static add(-2147483648, 0)
    10 Passed: static add(0, 0)
    11 Passed: static add(2147483647, 0)
    12 Passed: static add(-2147483648, 2147483647)
    13 Passed: static add(0, 2147483647)
    14 Failed: static add(2147483647, 2147483647)
    15 Passed: static main(null)
    16 Passed: static main({})
    17 
    18 ===============================================
    19 Command line suite
    20 Total tests run: 13, Failures: 2, Skips: 0
    21 ===============================================

可以看出整个测试过程很快，效果也还是可以的。

### 架构设计 ###

##### 第一次作业 #####

这次作业只需实现Path和PathContainer两个具体类。

Path类就是通过HashSet去存储点集来优化对点的查询，通过ArrayList存储具体的路径。有点不足的就是在比较类用了太多if进行判断，没有更好地利用官方库的相关函数。

PathContainer类也是双HashMap来处理提高查询速度，然后维护一个HashMap来记录容器内的不同节点，在每次增删Path时对其进行修改。

##### 第二次作业 #####

这次作业是在上次PathContainer的基础上，添加了图的相关内容。

首先，我维护了一个关于邻接边的HashMap，类似与节点的HashMap，同样在每次增删时对其修改。然后，我实现了一个循环队列，用于将节点映射到。之后，又维护了一个邻接矩阵，在每次增删，对每个顶点按照映射，去修改对映的元素。最后，设计了一个更新标志。在每次查询时，先查询是否需要更新最短路径矩阵，如果需要，就以邻接矩阵为基础通过floyd算出结果，再进行查询。如果不需要，就直接查询。更新标志只在邻接矩阵被更改时才会置1。

##### 第三次作业 #####

这次作业是在Graph的基础上，再实现3个带权图，然后，同时实现图的连通块问题。

这次作业还是有着不小的重构，原因是上次作业因为懒，没有把图这个类抽象出来，而是直接在Graph里实现。所以，这次首先将其抽象出来，单独成类。由于上次作业查询是否连通，是直接通过floyd算出的结果来查的。所以，这次的连通块需要重新设计算法。对于另外三个带权图，其与上次的floyd的区别，主要在于初始时不能直接使用邻接矩阵，而需要基于权值做一些改动。但是，主要方法还是可以使用floyd。

所以，针对连通块问题，是在上次floyd计算的最短路径的基础上，通过并查集实现的。在每次查询前，如果需要，首先更新最短路径矩阵，然后通过并查集着色，最终获得连通块数。

针对其他三张图，与上次的图很像，不通过点在与初始化邻接矩阵时，或者对于这三张图已经不能称之为邻接矩阵。对于最小换乘图，只用将一条路径上所有点之间的元素设为1，简单的两重循环遍历即可实现。对与最小价格图和最小不满意度图，则需在Path上，对每个点求一下这个点到其他该Path的点的最短带权路径。由于floyd每次都要先初始化一张小图，再做更新，开销过大，所以选择了spfa算法对每个点进行计算，然后存入初始矩阵。在查相关图之前，与上次作业相同，如果需要，先更新图。

### bug情况 ###

这三次作业中，只有第二次作业在互测中出现了问题。具体原因是在更新邻接矩阵时，对于自环的增删出现了问题，导致自环在一开始设置距离为0后，后又被更新为1。删除时，在删边时，只查了边的HashMap，没有查点，导致自环被提前删除。

### 心得体会 ###

首先，JML工具在开发中，对于保证逻辑的完备性和工程的严谨性有着重要的作用。一个完备的JML规格，就如同黑箱的输入和输出要求及对应表。任何工程的具体实现只要满足了其要求，就能够保证工程这一部分的正确性。同样地，它也是工程测试的一个重要工具。在编写测试，我们完全可以抛弃具体实现，参考规格来设计测试数据，从而提高工程的效率。

### 总结 ###

首先，我通过这三次作业体会了一个简单的迭代开发的整个过程，对于开发设计方面有了更多的了解。二是，通过对JML这样的规格设计工具，学习到了开发设计和工程实现间的差别和联系。然后，就是对接口和继承有了更多的体会和了解。

转载于:https://www.cnblogs.com/-Ez-Blogs/p/10906203.html