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

相关资源：各显卡算力对照表！