随着第三单元的结束，本学期的OO课程也即将步入尾声，我也从中获得了很多东西。这个单元主要是围绕着规格来展开的，根据题目所给的规格来实现方法内容，当然在实验课我们也亲自动手尝试写了几次JML语言，不得不说JML的用处还挺多的，如何完全覆盖的测试自己的程序是我们这个单元主要需要思考的问题。
那么话不多说，开始进入我们的作业。
在开始本单元作业之前，我们首先需要完成对JML语言的学习。
其实JML的基本语法在pdf教程中讲得已经十分详细了，那些接下来就汇总一下主要的概念：
前置条件(pre-condition)：前置条件通过requires子句来表示 requires P，要求调用者必须要保证P为真，规格中可以有多个reqiures子句。
后置条件(post-condition)：后置条件通过ensures子句来表示： ensures P， 要求方法实现者确保方法执行返回结果一定满足P为真，同理，规格中也可以有多个ensures子句。
副作用范围限定(side-effects)：副作用指方法在执行过程中会修改对象的属性数据或者类的静态成员数据，从而给后续方法的执行带来影响，用关键词assignable(可赋值)或modifiable(可修改)来表示。
通过阅读这几个部分，方法实现者就大致明白这个方法需要做什么，数据应该怎么处理，在处理过程中需要哪些变量达成什么结果。
JML工具感觉并不多，可能是因为JML在企业单位使用并不广泛。除此之外，学习这些插件的使用也是一件令人头疼的事情。那么，以下是一些常见的JML工具(插件)：
OpenJML: 基于JML规范实现的JML检查工具，用于进行基本的JML语法检查。同时也可以生成运行时检查程序是否符合JML规格的class文件(虽然我没有自己实现过)。
SMT Solver：用于证明程序逻辑结构是否等价，可以对代码进行形式化验证。
JMLUnitNG：根据代码中的JML规格，能够自动生成测试样例，对自己实现的程序进行覆盖测试。
由于水平原因，无法对Graph类生成测试文件，出现了某些未知的问题，因此我写了个小程序进行测试。
public class test { /*@ ensures a < b ==> \result == a; @ ensures a >= b ==> \result == b; */ public static int Min(int a, int b) { if (a < b) { return a; } return b; } public static void main(String[] args) { int a = Min(123, 123); System.out.println(a); } }
测试结果如图：
这三次作业从架构上看差别并不大，我也没有进行什么代码重构。排除一些可以直接按照规格描述的方法，我主要针对每次作业比较关键的地方谈谈程序是如何实现的。
这次作业主要需要注意的地方是时间复杂度的问题，大多数地方按照JML规格就能实现。
我认为这次作业的难点在于PathContainer类中distinctnode方法的实现，如果在每次调用distinctnode方法时都对PathContainer容器中的所有Path都进行一次遍历，那么这样两个for循环后代码的时间复杂度会达到o(n^2)，这样肯定会在强测中出现TLE的问题。我的设计思路是在每次构建Path对象的时候利用一个HashSet将该对象中所有不同的点存起来，那么在PathContainer中用一个HashMap<Integer><Integer>存取每个Path中出现的点并计数，这样在每次addPath和removePath时只需要遍历一遍Path的HashSet对容器中存储不同点个数的HashMap进行更新即可。这个时候在调用distinctnode方法时，只需要调用size()方法就能够得到所有出现的不同点的个数之和。
这次主要涉及到一个建图的问题，Graph的构建好坏对于第三次作业是有很大影响的，听说有些同学在第三次作业建图时选择了重构。这次作业我大部分沿用了第一次作业的代码实现，需要添加的方法有四个，那么我觉得这次作业最难的地方在于getShortestPathLength方法的实现。
总体来说，这个方法实现依赖于自己的graph图是否能正确建好。我采用的是HashMap<Integer><HashMap<Integer><Integer>>的方法来建图的，这个图能够保存所有边的信息，那么在每次addPath和removePath的时候对边容器进行更新就好。在每次调用getShortestPathLength方法时，判断边图是否发生改变，如果发生改变则需要重新遍历边图来建立一个HashMap<Integer><HashMap<Integer><Integer>>用于计算最短路径。这里我采用了bfs算法，将图中每个点之间的距离都算好，如果两个点不想连，就把值设为一个max数，这个时候就直接查找两个点的距离就可以了。
在这次作业中，主要涉及到一个换乘的问题，那么如何解决换乘问题在讨论区已经有技术贴了，通过一个非常巧妙的离散数学中图论的方法解决了计算换乘点的问题，链接如下： https://course.buaaoo.top/assignment/75/discussion/213
除此之外，还需要解决权值的问题。在第二次作业求最短路径的图中是没有带权值，在算上权值后就不能简单使用bfs算法了，我选择的做法是回归最原始的floyd算法，因为我所构建的图很接近完全无向图，所以使用floyd也不会慢到哪去。
最后还有一个计算连通块数量的问题，我采用的是dfs算法进行深度优先遍历，这个时候只需要对第二次作业建立的那个边图进行遍历就能求出连通块数量。
由于我三次作业是一步一步进行增改的，所以UML类图就给出第三次作业类图，如下：
整个程序的综合复杂度如下：
bug：这次作业前两次作业还是没出现问题的(虽然第三次作业的bug是由于第二次建图产生的)，我在第三次作业计算连通块时出现了问题。在完成getConnectedBlockCount的时候我采用了dfs算法对边图的点集合进行遍历，但是我在建图的时候，remove(Path)出现了问题，代码如下：
ArrayList<Integer> mylist = myPath.getNodeList(); int numbefore; int numafter; int n = path.size(); for (int i = 0; i < n; i++) { int num = mylist.get(i); if (i == 0) { numafter = mylist.get(i + 1); deletenode(num, numafter); } else if (i == n - 1) { numbefore = mylist.get(i - 1); deletenode(num, numbefore); } else { numafter = mylist.get(i + 1); numbefore = mylist.get(i - 1); deletenode(num, numafter); deletenode(num, numbefore); } if (mygraph.get(num).size() == 0) { mygraph.remove(num); } }
以上为部分代码段，我采用了HashMap<Integer><HashMap<Integer><Integer>>存图，需要注意的是，在删除路径过程最后，我会判断graph中该点对应的HashMap是否已经没有对应点了(即判断这个点上是否还有边)，如果没有就会在将这个点删除。那么注意if (mygraph.get(num) == null)其实是不起作用的，因为get方法只有在mygraph中不存在这个num时才会返回null，而num对应的HashMap即使为空时这个值也不是null，这个时候独立点就没有删掉。这样在dfs遍历时，对多算上独立点的个数作为连通块。
bug修复：把这句话改成if (mygraph.get(num).size() == 0)就能够有效删除num点的索引，这样就不会出现问题了(修改一句话修复了20个bug。。也算是收了个教训吧)。
这个单元的主题为规格，至于为什么要学习规格，我觉得一部分是为了规范我们的代码风格，另外在实际的大工程中也是有分工的，那么需要统一接口，这就要用到JML了。
其实总的来说，我觉得使用本次作业JML语言确实能够避免一些自然语言的二义性，在前几次作业中，不免有一些同学对题意理解出现问题，在引入了JML后，很大程序上解决了这个问题。但是从另一个角度上来看，这也在一定程度上帮助我们进行程序架构，我们会侧重于如何实现功能而不是为什么要实现这个功能，可以说各有优劣吧。
在使用JML的同时，我们还能自动化生成程序对自己的代码进行测试，这点也能有效帮助我们找到自己程序的bug(虽然我还是没有测出自己第三次作业的bug2333)。
那么这也是最后一个有三次作业的单元了(听说下个单元只有一次作业?)，不管怎样就是祝大家能够顺利完成OO下个单元的学习吧，go fighting！
原文：https://www.cnblogs.com/lufe1/p/10908430.html