标签:避免 优先 assert 它的 body 比较 pen 架构 res
JML是Java模块的行为接口规范语言。JML提供了语义来正式描述Java模块的行为,从而避免了有关模块设计者意图的歧义。JML的目标是提供严格的形式语义,同时仍然可供任何Java程序员访问。可以利用JML的行为规范的各种工具。因为规范可以作为注释写在Java程序文件中,或者存储在单独的规范文件中,所以具有JML规范的Java模块可以使用任何Java编译器进行编译。【摘自维基百科】
JML的关键字:requires、ensures、signals、signals_only、assignable、pure、invariant、loop_invariant、also、assert、spec_public
JML的表达式:\result、\old(
JMLUnitNG根据规格产生大量的自动测试
JUnit进行单元测试
openJML检查JML语法
在分析之前请先允许我吐槽一下配置的工作真的非常的麻烦,而且还要重新配置JDK的环境(我原本用的是JDK13结果发现这两个包只能在JDK8里面使用 )忙活了一通结果却不怎么尽如人意,从测试的结果上来看,其对于我们本次作业的帮助不是很大。这两个工具也不是很好用。
输出的警告是一些不影响结果的警告,因此没什么影响。只是在代码的风格上可能会有一些影响。
因为自动生成的样例中有大量的null,然而这些数据在实际情况下不会产生。其对于正常数据来说的测试帮助不大【花了这么大功夫你就给我看这】。我觉得如果单单要对正确性来进行测试的话,甚至用JMLUnitNG测试还不如自己手写一些数据,操作既简单而且测试覆盖的也比较全面。如果想要对整体的效率进行测试的话,可能对拍比用这些数据来判断要好得多。
? 第一次作业我主要是原封不动的讲JML翻译成JAVA的代码,在iscircle方法中,我盲目的使用了DFS的方法,且没有设置一个记录已经走过结点的栈,导致每个环可能会被重复走上还的个数的阶乘次,导致时间大大超出了要求,最终使我没有进入互测阶段。
? 吸取了第一次作业的教训,我将第一次作业所用的DFS方法来判断iscircle改为了用并查集的方法,这样的时间复杂度在iscircle中只需要判断其在那个集合中,时间复杂度从阶乘级别下降到了o(n),其他的地方变化不大。加之我在group中很多的参数使用了每次addperson或addrelation时直接增加的方法,使我在求ageSum,relationSum,conflictSum之类的方法的复杂度不高。但是,由于在前两次作业中我都大量使用了arraylist容器存储数据,导致在调用contains方法时的速度过慢,导致我在强测中前16个点均爆出了CPU_TLE,而后四个点又因为我在判断条件时没有仔细阅读JML,导致我在某个需要elseif判断的地方直接用else一笔带过,使我在本该没有输出的地方输出了异常信号,最终我又一次遗憾的没有进入互测。
? 充分吸取了前两次作业的经验和教训,我对我对代码进行了重构。我用HashMap和HashSet替换了原来使用ArrayList的地方,并进一步将我的并查集优化,把MyPerson加入属性RelationNum,使得iscircle的时间复杂度从o(n)降到了o(1),代价是在合并并查集的时候时间会略有上升,但由于每个集合的元素大部分时间的数量较少,因此效率还是有所提高。在实现qmp中,我使用了优先队列优化的迪杰斯特拉算法,而在实现qsl中,我使用了塔尖算法,在这次完善过后,我的代码的所有方法的复杂度都不超过o(nlogn),此外,这一次作业我也做了更加充足的测试,最终我通过了强测中所有的点。
? 在三次作业中,我的所有bug都是关于性能的,因此我的bug修复也是集中在提高性能上。在第一次的bug修复中,为了减少修复的代码的行数,我没有将dfs换成bfs或并查集算法,而是建立起了一个栈,在加入某个结点时自动入栈,其他的路径不会走已经入栈的结点,这一处修改让我通过了强测剩余的19个点。第二次作业我的bug是由于contains的使用不当造成的,当时我的qnr的时间复杂度达到了o(n^2),我在修改的时候也没有像第三次作业一样整体重构,而是将对应处的contains操作省去,用判断返回值是否为null的方法了间接判断是否contains。当然,这只是为了降低代码修改量的权衡之计。在这三次作业中,我找bug的方法主要包括对拍,对某个方法进行单元测试,输出计算时间较长的语句。
? 这单元的作业对我来说是血和泪的教训,由于在前一单元的发挥不错,加上jml的规格较为简练,使我一开始对它的重视程度不够,导致我第一次作业完全没有考虑复杂度,测试也极不充分,没有涉及时间的测试。在第二次作业中,我诚然进行了大量的测试,但殊不知我的自动测评机的代码的结构和强测代码的结构有所不同,极大的放大了我在对拍时的时间差。通过这两次的实验我深刻的认识到了特朗普的那句名言“也许这就是人生吧”,我想在后面加上一句,“当你以为你从一个坑里爬出来时,你不会发现,其实你在另一个更大的坑里面”。
标签:避免 优先 assert 它的 body 比较 pen 架构 res
原文地址:https://www.cnblogs.com/vincentxie/p/12942739.html