标签：实现 数据 link 复杂度 com 关注 作业 存储 result
这是oo课的第三个单元，也就是关于JML的学习。在这一个单元中，我感到和前几个单元有着很大的不同。因为在前几个单元中，我们要实现的功能必须通过阅读指导书，理解自然语言的含义才能理解，这样一来容易出现理解偏差，二来也很容易漏掉关键信息。但是，在这一单元中，我们只需要阅读相应的JML规格就可以很清晰地了解我们要做什么事。在之前几个单元中，整体的设计结构是很重要的，但是在本单元中，我们不需要过于关心整体的结构，只需要选择好的算法实现各个函数的JML即可。总的来说，我感觉这一单元从难度方面而言，不如之前两个单元，但其中也蕴含了很多程序设计的理念。
首先介绍一下JML。所谓JML，就是Java Modeling Language。它是一种类似于javadoc的，通过注释的方式对java代码规格进行规范的一种形式化语言。例如对类中的成员变量的规范描述，对类的功能的特征的规范描述，以及对类中各种方法的使用条件、正确执行结果、副作用等的一系列规范化的描述。
我在一开始接触JML的时候，感到非常摸不着头脑：本来写代码已经很累了，为什么还要在写代码的前面还要写一串伪代码？难不成是怕自己写着写着忘记这个函数要干啥不成？但是后来我逐渐意识到了它的重要意义。我认为JML这种抽象的形式化语言，可以最大程度上分离设计和实现。也就是说，我在一开始思考构架的时候，可以先把注意力全部集中到设计上，搞清楚每个函数都要实现什么功能、处理怎样的边界数据、如何处理异常行为等等。在此基础上，我们编好了JML，然后再根据JML实现具体的算法。这样一来，可以很大程度上避免我们在设计的时候被诸多细节困扰，另一方面也便于形式化验证程序。
下面是对JML的简要介绍：
\not_assigned(x,y,...)表达式：用来表示括号中的变量是否在方法执行过程中被赋值。
\not_modified(x,y,...)表达式：与上面的\not_assigned表达式类似，该表达式限制括号中的变量在方法执行期间的取值未发生变化。
\forall表达式：全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。
\exists表达式：存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束。
\sum表达式：返回给定范围内的表达式的和。
\product表达式：返回给定范围内的表达式的连乘结果。
\max表达式：返回给定范围内的表达式的最大值。
\min表达式：返回给定范围内的表达式的最小值。
\num_of表达式：返回指定变量中满足相应条件的取值个数。
前置条件(pre-condition)：
openJML：对JML注释的完整性进行检查。
SMT Solver：检查代码规格，生成测试。
JMLUnitNG：针对类自动生成测试样例并进行测试。（下面简要介绍一下本人的使用经历）
在看了博客和讨论区诸位大佬的介绍后，我心底有点发凉，感觉不是很好搞的样子。然后，我只能硬着试一试（果然体验非常差）。在尝试了非常久，找到了非常多报错的原因之后，我终于成功地得到了如下结果：
为什么fail呢？有的是因为方法没有实现或者规格没有实现。但是还有一些，说实话没搞懂......
生成的到底是什么样例呢？主要是一些边界数据，用来测试程序的鲁棒性，比如传入null啥的。
使用体验：莫名其妙的BUG非常多；不支持高版本JDK；自动生成的数据过于关注一些边界，比较没用。总的来说，体验并不好。
这次作业没有复杂度特别高的操作，最复杂的一个就是isCircle，其他的函数主要复杂度都是o（1）。而在具体实现isCircle的时候，我采用了并查集的方法。因为考虑到记忆化的问题，对反复的询问不应该每次都BFS或者DFS去计算。这样一来，isCircle就变成了o（1）操作，但是addPerson和addRelation的复杂度略有上升。
这次作业的复杂程度总体来说不高，功能也都比较基础。但是，由于一开始接触JML不太熟悉，所以我没有注意到islinked函数，如果是自己对自己，应该返回true。因此出现了巨大的BUG，强测错了很多点。但是，幸好我在实现的时候，不同的方法采用了不同的具体实现方式。就比如isCircle中，我采用了并查集的方法，压根就没有调用isLinked函数，所以也不至于失分过多。
第二次作业主要增加了Group这一个对象，然后增加了一大串相关的方法。这些方法，都可以用一个办法进行优化，就是预先计算。比如getConflictSum，可以在group中维护一个变量conflict并初始化为0。然后每一次添加成员的时候，就通过conflict = conflict.xor(newPerson.getCharacter())进行更新。其它的方法，如求均值、方差等都可以用完全类似的方法进行优化。这样一来，这些函数就都变成了o（1）复杂度，但是相应的，addtoGroup的复杂度就会上升。
这次作业的复杂程度总体有所提升。但是我无论在强测还是互测，都没有出现任何的BUG，也没有找到别人的BUG。
第三次作业主要支持了从群组中删除人。这个对于之前我采用的记忆化方法来说，存在一定的挑战性，尤其是conflict。我一开始以为必须重新遍历计算新的conflict，但是写道一半转念一想，并不需要从头开始，因为a xor b xor c = a xor (b xor c) 且 a xor b = b xor a 且 a xor 0 = a 且 a xor a = 0所以如果这个人被删掉了，只需要conflict = conflict.xor(delPerson.getCharacter())就可以了。
然后还添加了getMinpath的方法，对于这个，我采用了优先队列优化的Dijkstra算法。
至于strongLink的方法，我先用优化过的DFS搜索出一条路径，然后逐个删除这条路径上的点。然后判断是否这两点还联通，如果全部联通，则证明这二者是双联通的；否则只要有一次不连通，就判定为不连通。
这次作业的复杂程度总体进一步提升了。我在强测中没有出现错误，但是在互测中，被逮到了一个问题，主要是因为有一段代码忘记放到if里面去了。在本次作业中，我也没有发现别人的BUG。
在本单元的三次作业中，我们主要的学习内容是JML的语义，而没有像之前一样一直关注程序的结构，在这一点与之前的两个单元有着很大不同。在这一单元中，基本实现的框架已经差不多了，但是具体的细节和实现还是需要我们仔细才能完成。在这一单元，我更加深刻地体会到了设计和实现的区别。在写作业的时候，我越来越明白光有正确的规格是不行的（感谢助教和老师们），实现也很重要！
总之，这一单元让我学到了很多，我也将全力以赴学习下一单元的内容。
标签：实现 数据 link 复杂度 com 关注 作业 存储 result
原文地址：https://www.cnblogs.com/kzxzvbk/p/12941187.html
