标签：work 简单 应该 提示 hat unit ber 过程 语法
JML主要由方法规格和类型规格组成。
方法规格包括前置条件、后置条件和副作用范围的限定。前置条件可以用来区分该方法不同的行为（正常或异常），后置条件就是这个方法执行完后的结果，副作用范围限定规定了这个方法运行的过程中哪些元素可以被改变。
类型规格分为不变式和状态变化约束。不变式是要求程序在一切可见状态下都要满足的特性，而状态变化约束是一项数据在发生变化是前后关系应该满足什么条件。
方法规格是对具体方法的实现做出规定，而类型规格是对于整个类进行贯穿式的规定，便于理解整个类的实现。
第一次刚拿到JML规格的时候，并没有先把整个社交系统的结构先通读一遍，只看到需要定义一个集合并可以实现添加和删除指定元素，因此当场ArrayList干上去了。用ArrayList不能说不行，甚至在很多地方能避免奇奇怪怪的BUG，但是随着对整个系统的逐渐了解，尤其是在发现需要大量的根据id查找指定对象的操作之后，我将所有的ArrayList改成了Hashmap，以每个people、message等的id为key，以要查找的内容为value，如Acquaintance，以其中person的id为key，对应不同的关系值。
在开始用BFS实现的isCircle函数中，最开始我使用的是ArrayList存储已经遍历过的person，这样就导致每次在一个acquaintance中找到一个人后，都得遍历一次这个ArrayList，看看这个person是否被找到过。因此将这个ArrayList改成了Hashset，这样找到一个person后直接加入其中即可，因为Hashset中不允许出现相同的元素。
在后面第三次作业的rank，emojiHeatList等数组中，使用Hashset也要方便许多避免了手写大量循环。
三次作业做下来，发现只要超过o(n2)的算法都会出现CTLE，而isCircle如果不用并查集的话互测会被hack。
首先就是queryBlockSum，这个函数如果按照JML直接写的话，会是一个超过o(n3)的算法，这还是在isCircle效率较高的情况下。
而isCircle在使用BFS或者是DFS时，这个函数的改动比较困难，只有在isCircle使用并查集的时候，利用节点之间的父子关系，可以通过直接查找根节点的数目来确定queryBlockSum值。
然后是person的messages需要头插，而直接实现头插会产生两次循环，效率较低。因此我直接使用了尾插即.add()，然后在读取message时改为从后向前读即可。
最后是getValueSum函数，这个函数直接写也是o(n3)的函数。
因此我在刚输入一个人到一个group时，就将value加入到group中设好的一个变量valueSum中，查找时直接返回这个valueSum即可。
在尝试了DFS和BFS都被hack之后，基于并查集进行了图模型的构建。首先新增两个Hashmap parent和rank，parent存储一个节点对应的父节点，rank存储以一个节点为根节点的树的层数。
随后在添加关系时，找到两个id对应的人的根节点，将层数少的根节点加到层数高的根节点的下面。并将该节点对应的rank加一。
这样在添加完所有的关系之后，两个人之间如果是连通的，那么他们必然会有相同的根节点。如下图所示：
在查找函数findroot()中，建立了一个递归，既将通过一个id找到的根节点不断设为这个点的父节点，这样下一次查找就会变得更快。
通过rank加一和递归设置父节点，实现了该模型的维护。
因为第一次接触JML，所以事实上我的设计过程并非正确，在此我只是将做完三个单元作业后得出的较好的设计过程做一个总结：
（1）通篇粗略阅读整个JML规格，不用细究函数的实现，但起码要知道每个函数要干什么。
（2）详细阅读每一个类，通过（1）中对要进行的操作的理解，确定其中的成员要使用怎样的数据结构。
（3）对于其中比较复杂的方法，添加新的方法和新的成员。
（4）具体实现所有的方法，并对每一个方法进行覆盖测试
（5）对整体进行测试。
Junit的使用整体来说比较简单，如我想要对Network类进行测试，我们只需要按照课程提供的链接教程新建一个MyNetworkTest类，并选择要进行测试的函数。
其中setUp()函数含有@before关键字，运行于每个函数的test之前。
tearDown()函数含有@after关键字，运行于每个函数的test之后。
然后就是具体函数测试代码的编写
首先将自己设计的数据写入其中，然后运行响应的函数，用assert对运行结果进行断言检查。
其中assertThat是一个很好用的断言检查方式。
如assertThat(mapObject,hasEntry(“key”,”value”))可以直接查Hashmap里的东西对不对，还有hasKey(“key”)、has(“value”)等等;
也有assertThat( testedNumber, allOf( greaterThan(8), lessThan(16) ) )
assertThat( testedNumber,allOf(greaterThan(8),lessThan(16) ) )，比较直观。感觉如果异常类复杂起来的话这个会比较有用。
JML的括号问题确实有些坑，因为是以注释的形式出现，所以只能肉眼判断括号匹配，而粗心如我自然是掉到了坑里。在isLink()函数中将id等于本人id的情况写到了for循坏里面导致判断不出来，还是在之后的Junit测试中碰巧找到了。
JML只是规格，是针对输入输出的一种提示，不可以对JML照抄照搬，JML中给出的可能是最麻烦的那一种实现。当然也不能一味地追求性能，忽略了整个系统的层次性和可读性。
Junit测试是一个很方便的工具，通过将自己设计的数据放到test程序中配合断言检查即可进行覆盖性测试。可以分为每一个方法、每一个类、以及整体进行测试。
从JML到代码的转换很容易，但把一个实现目标转换成JML就很难了，甚至感觉比自己实现花的时间更长，这也许是对JML语法不熟悉的原因吧。
标签：work 简单 应该 提示 hat unit ber 过程 语法
原文地址：https://www.cnblogs.com/phm19231049/p/14823725.html
