标签：不同的   page   font   类型   学习   nbsp   指令   作业   exp   

一、JML介绍

JML(Java Modelling Language)是一种用于描述Java程序方法的行为的语言。JML规格对方法的执行效果、执行条件和副作用等作出了明确的规定。

JML的相关工具链包括OpenJML、JMLUnit等，OpenJML可以对JML的正确性进行静态检验，以及对方法的正确性进行验证；JMLUnit可以生成简单的、针对边界条件的测试样例来对方法进行检测。

实际上，JML所描述的方法实现往往没有实用性。如果照搬JML规格所描述的方法实现函数，一定能够正确实现，但性能往往是很差的。实现JML所规定的功能，应对数据结构和算法都进行深入的分析。

二、程序架构

本次作业共需要实现三个类：Network、Person、Group。其中，Network代表一个社交网络，其本质是以Person为节点的无向图。Person也可能属于某些Group，一个Group内的Person可能相关或不相关，这一概念类似于“老龄人口”或者“残障人士”这种分类，抑或是群聊。

本次作业看上去好像很简单，容易实现，但实际上在算法的性能上，若不加考量，会出很大的问题。其中，比较容易产生问题的方法包括以下几个：

public int queryNameRank(int id)
public int queryAgeSum(int l, int r)
public boolean isCircle(int id1, int id2)
public int queryBlockSum()
public int queryGroupAgeVar(int id)
public boolean queryStrongLinked(int id1, int id2)

1. queryNameRank和queryAgeSum

   这两个函数分别是求一个Person在整体中名字的字典序排名和在年龄在[l,r]之间的Person个数。这两个函数都不怎么容易优化，但好在本次作业中并没有卡这两个函数的打算，即使每次以O(n)的复杂度遍历也不会出问题。实际上，这两个函数都可以通过手动建树来优化，但需要的时间和精力实在不值得，不如去做一做OS作业。

2. isCircle和queryBlockSum

   这两个函数分别是询问两个Person之间是否连通，以及整个图中的连通分量的个数。

   很显然，isCircle可以通过BFS或DFS的方法解决。第一次作业由于没有对时间作出较高的要求，使用这两种复杂度为O(n+e)的方法问题不算太大。

   但是真正的噩梦从第二次作业开始。第二次作业要求在6.66s之内运行完成100000条指令，所以时间压力变得非常大。(实际上光是调用函数的过程就得耗费1秒)使用BFS和DFS都变得危险起来。因此，需要使用新的轮子算法：并查集。通过并查集算法可以方便地查询两个点是否位于同一连通分量，而且如果在每次查询的同时对并查集结构进行展平，平均复杂度最好可以达到O(1)。同样地，连通分量的个数也可以使用并查集进行管理。

3. queryGroupAgeVar

   这个函数实际上并不难处理，使用方差的定义式即可发现方差满足下面的式子：

    

   然而，在第三次作业中年龄的上限是2000，人数的上限是800，这就意味着如果用int存储年龄的平方和，将会导致溢出。然而，由于方差的最大值是1000000，方差最大值乘以800为800000000，并没有溢出，实际上可以证明使用int并不会对最终的结果造成影响。这是因为<I, +, -, ×>构成了一个代数系统，而I中的元素和它的模4294967296同余类的映射构成一个到同余类的代数系统的同态映射。令φ表示该映射，φ^-1则表示同余类到其位于[-2147483648, 2147483647]的元素的映射，则根据同态映射的性质，满足下式：

    

   因此，使用int并不会导致最后的结果出现问题，long使用不慎反而会出问题，比如光记得用long存平方和了，结果式子后面没转换成long。

4. queryStrongLinked

   这个函数是第三次作业中最难处理的函数。它在询问是否在两点之间存在两条途经点完全不同的路径。如果使用两次BFS或两次DFS的方法那就上当了。很容易构造一个图G=<{a,b,c,d},{(a,b),(a,d),(b,c),(b,d),(c,d)}>以及一条路径(a,b,d,c)，使得当去除该路径上的所有点(除端点)后a和c不再连通，但实际上a和c确实存在两条完全不同的路径。

   这个问题实际上是点双连通分量的问题，也就是在一个图中，去掉任意一个点，是否仍然能够保证任意两个点之间是连通的。这个问题的暴力做法是，寻找一条路径，再对该路径上的所有点依次进行屏蔽，依次寻找是否仍然有两点间的路径。这种方法较为简单粗暴，实际上也不会使性能差到无法接受，因为第三次作业的queryStrongLinked最多只有10条。

   如果追求完美，可以采用Tarjan算法。Tarjan算法实际上不止有一个，包括求有向图强连通分量和点双连通分量、边双连通分量。我在查找资料的时候曾在这一问题上疑惑良久。

三、bug修复

更换JRE8，更换Eclipse，使用OpenJML对工程进行ESC，发现OpenJML报如下错误：

实际上，我尝试了各种方法，发现OpenJML有时会报NullPointerError，有时会报“Object类型不支持++运算”，但我通过解包发现并没有相关的代码。如果有人帮我配置成功，我可能会临表涕零不知所言。

我对bug的测试，实际上主要采用的是和其他人的jar包比对输出的方法。通过随机生成的数据的大量轰炸，可以用鸟枪法筛出不少bug。然而最后没有测出来方差的溢出bug，但强测没有专门卡这个bug，算是幸运max了。

四、总结

本次作业学习了JML规格这种无二义性的方法功能表述方式，同时对大量的算法进行了复习。这次作业也告诉我算法是多么重要，复杂度的差距可以造成巨大的性能差异。

第三单元总结

标签：不同的   page   font   类型   学习   nbsp   指令   作业   exp   

原文地址：https://www.cnblogs.com/SyntaxError/p/12941048.html