OO第三单元JML规格设计学习总结与分析
OO-Unit3-总结·
1.JML规格设计策略·
由于JML的规格描述较复杂,本单元的JML规格设计我往往采用由简入难的迭代开发策略。
即一开始不着急开发出最为复杂,性能最好的代码,先严格按照JML描述写一遍代码,实现基本功能。比如类似public instance model non_null Person[] acquaintance;
这样的规格,第9次作业开始时先直接按照ArrayList
处理,这样各个函数中实际的代码和JML描述近乎一致,方便检查。之后在完成了基本功能后,在已经理解了基本功能描述后,对各个容器和方法算法性能进行优化设计迭代。
同时,一般简单的方法和容器设计虽然性能较差,但正确性一般较好,因此个人认为也可以作为之后的迭代优化版本的正确性测试参考的标程(不过实际开发过程中也不可能先开发一版低性能保证正确性,所以还是直接全盘考虑好再写高效一点)。
对于每个方法而言。先确定normal_behavior
和exceptional_behavior
。确定进入函数后不同参数对应的分支条件。并把条件判断语句写好,搭好基本框架。之后再看assignable
会涉及到的变量。再根据ensures
确定结果返回值和应该如何改动变量。对于异常处理里的分支逻辑也是类似的编写方式。此外,每个方法编写时也可以通过函数名字推敲涵义,从而提高正确性。
同时对于迭代增量开发,每次都要重新阅读之前实现过的方法内的JML规格,因为可能会发生变化,比如第二次到第三次作业中的sendMessage
方法。此外要特别注意JML没写出,但是你需要实现的代码,比如MyGroup内的delPerson方法
,如果输入的person
是个null
需要直接返回;MyPerson
类内需要加一个addAcquaitance
方法以及getAcquaitance
方法等。
2.JML测试方法和策略·
本单元的JML规格设计由于JML细节较多,很难保证某一份代码是完全正确的,因此测试上最方便最简单的当然就是多人对拍找少数派(即多人运动)的方式了。这个方法在第一单元中也用到过,总结来说,对于这种输入一样,输出结果就应该一样的代码,这种方式测试效率还是很高的。此外,还有Junit单元测试,以及openJML等其他JML工具。
Junit单元测试·
Junit测试简单,可以进行对类内每个方法编写自己的测试逻辑。IDEA里最简单的使用方式就是右键点击代码里的类名-->点击Go to-->点击Test
,选择需要测试的函数和选项,就生成了测试文件。
本单元中主要针对一些比较容易出现错误的方法比如isCircle
和queryBlockSum
进行了测试,以这两个函数为例。
1 | import com.oocourse.spec3.exceptions.PersonIdNotFoundException; |
运行后就会出现令人舒适的评测信息,这样的单元测试,怎能不爱😍。
一般来说就在BeforeEach
和AfterEach
里分别编写数据构造和初始化以及其他的评测信息。但是注意到这样的测试方式是对于每个@Test
处的函数都分别调用了一次测试,即每个这样的函数对应一个点。这样有时体现不出一个类整体连续性,比如某几个方法之间的联系。参考官网写出了连续的测试方式,相当于所有方法在一次程序执行内跑完。
同时,Junit实在太强大,几乎可以测试所有的情况,比如空指针,异常抛出等,用以下代码举例。
1 |
|
Python对拍评测·
与第一单元类似,主要分为双人对拍和多人运动。本次作业单独写了两个文件。relation_testdata
产生测试数据。relationTest
进行对拍测试。
测试数据产生主要分为随机生成用例和生成复杂的卡时间的用例。具体的生成的方式都封装在getOneTestPoint()
方法中。根据作业次数和数据特点变量生成相应用例。其中随机生成用例要保证一定的强度,比如每个测试点都是5000条指令,保证每个测试点覆盖了所有的指令(对每个指令的个数进行计数)。
1 | datas_src = "test_data/" |
对拍测试中先进行多人团建。挨个检查所有每个文件对测试点的CPU使用时间测试性能。之后再通过比对所有人的答案检验正确性。如果大家答案均一样且没有人超时,则认为所有人正确。这里使用的是test
函数,对输入的一个jar
文件名字列表进行处理。
1 | if __name__ == "__main__": |
效果如下
在一波多人运动后,一般会发现团队中有个别成员(比如自己的代码)存在一定的问题,这时就可以选择1-2
个优秀的成员作为标程和其他代码进行对拍。使用beatTest
函数进行重点爆破,提高寻找bug
的效率。
1 | beatTest('homework11.jar', 'Berserker.jar') |
总的来说,1、3单元对多人的代码进行测试的方式比较可取的就是每个人单独跑数据看时间,使用多人对拍评价正确性。
openJML工具使用·
代码静态检查命令如下,感觉输出好奇怪,调了半天也没调好,只好放弃了。
1 | java -jar .\openjml.jar -exec (SMT Solvers的路径) .\Solvers-windows\z3-4.7.1.exe -esc -dir (项目目录) |
JMLUnitNG·
1 | java -jar jmlunitng.jar test/MyGroup.java |
这种方式只检查了边界数据,因此只是简单了解了一下,没有怎么使用。
3.容器选择与使用·
由于本单元作业需要对容器内元素进行高频率增删改查的操作,选用普通数组实现JML效率非常低下,因此大部分容器都采用HashMap
进行设计。
homework9·
本次作业由于性能要求较低,除了为了isCircle
函数的广度优先搜索算法编写的visit
数组使用了HashMap<MyPerson,Boolean>
外其余的容器均使用ArrayList
,即acquaintance/value/people
。使用时基本和JML
描述写法一致。
homework10/homework11·
在这两次作业中由于指令数量增多,性能要求提升,将第9次作业中所有的ArrayList
全部替换成了HashMap
。包括MyNetwork
类中的people/id2group/id2message/id2bossid
以及MyPerson
中的acquaintance
。同时新增的方法和变量也尽量使用了HashMap
保证性能要求。
4.bug分析·
本单元的bug主要集中在两方面,即:
- 因为JML阅读不细致导致的程序正确性问题。
- 因为算法/容器设计不合理导致的CPU时间问题。
homework9·
自己的bug·
这一次作业性能要求不高,但由于没有仔细思考,采用了dfs
算法进行isCircle
函数设计,同时在qbs
函数中直接采用二层循环进行遍历查找,导致非常慢,出现了性能问题。强测被hack一个点,互测被hack7个点,全部是CTLE
。修复bug
时将isCircle
采用bfs
实现qbs
和isCircle
函数。
他人的bug·
测试时由于这一单元正确性较简单,主要针对多人的复杂网络进行了数据构造,至少增加200人以及200条关系之后在最后的几百条指令全部用qbs
和qci
进行轰炸。效果还可,很快就刀到了两个同样使用dfs
的难兄难弟,之后基本就收手了,看了房间里被hack的代码都是这两个的性能问题导致。
homework10·
本次作业个人测试时主要注重性能,没有很关注正确性,导致代码里有大量正确性问题,导致第一次没进互测,心态崩溃的同时,也对各个写错的地方认真进行了审视。
自己的bug·
MyGroup
类内删除人的时候没有把总年龄和减去删除的人的年龄导致错误。MyNetwork
类addToGroup
方法内不存在新加的人且group
内人数大于等于1111时没有直接返回而是进入了异常。异常里存在这个人时。addMessage
内当加入的邮件里两个人id相同时抛出异常使用的id是messageId
。sendMeesage
方法内当类型为0时没有把person1
加入person2
的关系数组里。getReceivedMessages
方法内误以为只返回一个小于等于3的Message
数组,实际上是返回一个小于等于4的Message
数组。
这次作业的bug主要都是因为在阅读JML代码时过于草率,很多地方都是漏看了一句话导致了问题的出现,且测试不够充分。这启发我在以后的JML规格编写时要认真细致地阅读每一行说明,编写后要进行充分细致的单元测试和黑箱测试。此外,本次作业在自己构造数据时往往关注时间,构造了和第一次差不多的数据,对第二次作业涉及的指令覆盖很有限,这也导致了问题的出现。同时之后也发现自己的测试脚本中也是有问题的,很多时候可能测试数据里只有第一次的指令,因此问题也很难找出来。所以以后对自己的测试数据生成脚本不能过于自信,要仔细审查。
正确性虽然被hack
惨了,但是时间性能上由于使用了并查集进行搜索,没有出现问题。并查集对每个新进入的人先设置他的bossid
为他自己的id
,之后新增的关系中,如果他们的bossid不一样,则把一个人的最高级的bossid
(p.bossid==p.id
)设置为另一个人的最高级bossid
即可。
homework11·
自己的bug·
本次强测互测均未被hack。
有了上一次的惨痛教训,本次在测试时非常细致,结合了ch大佬的数据和自己的数据进行了多轮校验。这次自测时仍然找出来了与上次作业中类似的正确性的错误,对于各个类中的方法进行了多次修改,值得一提的是很多错误都是由于想当然以为上次的方法这次不变导致的,这一点以后也需要注意。同时重点设计了最短路径查找算法,使用了堆优化的Dijistra
算法,新增一个Node节点类保存了距离和id,使用优先队列模拟堆,避免了每一轮循环都进行全部的遍历查找,保证了时间性能。此外在MyGroup
类中加入了valueSum
变量,每次有人员变动时就修改valueSum
。从而保证了qgvs
指令的性能。
他人的bug·
本次由于限制了5000条指令,且上限为6s,从时间上hack是极难,尝试构造了很多复杂的数据都未成功。最后通过大量随机生成用例hack了一人。阅读代码发现是经典的问题:isCircle
函数输入相同的id
时没有返回true
5.作业架构设计·
本单元作业架构相对固定且是官方给出的,每个基本类相对固定,活动空间主要是对于图模型的管理维护。由于代码量并不大,本单元我直接将全部的图相关算法和主要数据、方法都写在了MyNetwork
类内,同时将具体算法函数与功能函数分开。在isCircle
内调用不同的find
方法从而方便优化性能,有过dfsFind(id1,id2) bfsFind(id1,id2) unionFind(id1,id2)
共三个查找的算法函数。同时在sendIndirectMessage
函数中也是调用Dijistra
函数进行操作,且调动了一个外部类Node
进行堆优化操作。同时,使用一个HashMap
保存每个PersonId对应的bossId
进行并查集数据管理。
同时,各个类内最终都基本使用了HashMap
作为数组的实现容器,且这些都采用id
作为key
值进行查找。
本次的异常类采用static
类count
对异常数据进行管理,确定了统一接口进行查询和存储异常次数。每次新增时只需要新增新的HashMap
的key
值即可。
6.感想与体会·
- 本单元是圣杯战争最后一战了,回想参加的8次互测,整体来说体验还是很好的,在这个过程中学到了不少和测试相关的知识,也加深了对java和python这两门语言的理解。非常感谢课程组给我们设置的这种课程体制,让我们对测试这门艺术有所理解和掌握
- JML对代码的限制还是很强的,之后在开发之前不妨先写上JML再进行后续的开发,这样正确性能够有大幅提升。同时,JML也确实太复杂了,感谢为我们的作业献出那么多力量的助教和老师们,真的辛苦你们了!