BUAA_OO_2020_Unit3 Summary
Posted weilan1201
tags:
篇首语:本文由小常识网(cha138.com)小编为大家整理,主要介绍了BUAA_OO_2020_Unit3 Summary相关的知识,希望对你有一定的参考价值。
梳理JML语言的理论基础、应用工具链情况
JML(Java Modeling Language)
-
JML是一种形式化的、面向JAVA的行为接口规格语言(behavioral interface specification language)
-
JML允许在规格中混合使用Java语法成分和JML引入的语法成分
-
JML使用Javadoc的注释方式
-
JML已经拥有了相应的工具链,可以自动识别和分析处理JML规格(如
OpenJML
,JML UnitNG
等) -
JML基本组成:前置条件、后置条件、会改变的元素和属性、不会改变的元素和属性、不正常的行为发生时抛出异常
- JML 中常用的表达式:
old(expr)
表达式用来表示一个表达式expr
在相应方法执行前的取值;esult
表达式表示方法的执行返回结果;forall
表达式是全称量词修饰的表达式,表示对于给定范围内的元素,每个元素都满足相应的约束;exists
表达式是存在量词修饰的表达式,表示对于给定范围内的元素,存在某个元素满足相应的约束;sum
表达式表示返回给定范围内的表达式的和;product
表达式表示返回给定范围内的表达式的连乘结果;max
min
表达式分别表示返回给定范围内的表达式的最大值和最小值;<==>
<=!=>
等价关系操作符:b_expr1<==>b_expr2
或者b_expr1<=!=>b_expr2
分别表示表达式相等或不等;==>
<==
推理操作符:b_expr1 ==> b_expr2
或者b_expr2 <== b_expr1
。
- JML 中常用方法规格:
- 前置条件
requires
:requires P
表示要求调用者确保 P 为真; - 后置条件
ensure
:ensures P
表示方法实现者确保方法执 行返回结果一定满足谓词P的要求,即确保 P 为真; - 副作用范围限定:关键词
assignable
表示可赋值,modifiable
表示可修改; pure
:表示方法是纯粹的访问方法,不会对对象进行任何修改;
- 前置条件
- JML 中常用的表达式:
-
- jml-launcher (the launcher for the graphical user interface tools).
- jml and jml-gui (the checker).
- jmlc and jmlc-gui (compile for runtime assertion checking).
- jmldoc and jmldoc-gui (a version of javadoc that includes JML specification information).
- jmle (compile for executing or prototyping specifications).
- jmlrac (a version of java, the VM, that includes the bin/jmlruntime.jar file in the CLASSPATH, for running files compiled with jmlc).
- jmlre (a version of java, the VM, that includes the runtime support needed for executing specifications, for running files compiled with jmle).
- jmlspec and jmlspec-gui (generate skeleton specification files from Java source files).
- jmlunit and jmlunit-gui (produce unit testing code stubs for use with JUnit).
- jtest (combines the work of jmlc and jmlunit)
- jml-junit (a version of JUnit‘s swing user interface that includes the bin/jmlruntime.jar and bin/jmljunitruntime.jar files in the CLASSPATH, for running JML and JUnit based tests on files compiled with jmlc and test cases generated by jmlunit).
- 来源官网(年久失修)
SMT solver
缺省参数检查:
静态检查:
动态检查:
呵
JMLNG:
-
下载包
-
运行
- java -jar jmlunitng.jar MyGroup.java
javac -cp jmlunitng.jar *.java
java -jar openjml.jar -cp H11.jar -rac MyGroup.java
javac -cp jmlunitng.jar MyGroup_JML_Test.java
java -cp jmlunitng.jar MyGroup_JML_Test
- java -jar jmlunitng.jar MyGroup.java
-
错误分析:
- 出现错的集中在我自己写的
addrela
与delPerson
上 - 其中
addrela
是按照我自己逻辑写的,并没有jml规约,限制都在MyNetwork里完善了,于是保证输入是合理的。 delPerson
同理,在官方包中并没有写规约。- 但想想所谓的万无一失是架构在自己的逻辑上的,看自己代码的人是否能懂呢,显然
jmlng
就不懂。一个方法写出来或许就要保证它的完善性吧,如果别人在更改的时候调用了该方法没有做到自己实现的逻辑闭环,还是有很大隐患的,鲁棒性怕是还是要的,对不同输入(非法或不非法)的处理,或许需要进一步完善。
- 出现错的集中在我自己写的
架构设计分析
鉴于三次架构差的不多,仅放上第三次作业图
第一次作业
基本架构课程组已经给出,总体难度不高,只是摸了dfs写把自己作死了
第二次作业
新增Group接口,基本架构我并没有在课程组的基础上修改。
因为上次作业因为性能被搞了,所以这次根据规格的实现尤其注意性能的把握。首先当然是把dfs扬了,改成路径压缩的并查集。其次是对Group内部方法的实现。缓存的思想对数据进行预处理,要注意处理时对于自身数据的把握。在person中增加自身所在group的存储也是你懂我懂大家都懂的事。
其实本来这次作业还想要设置标志位,以避免每次加人都循环的不必要,而改成响应查询时再从上次循环结束的地方继续进行,但事实证明这种实现过于不现实,遂放弃。
第三次作业
只怕我就是让老师失望的本人(,除了要求的My三件套,为了Djs而构造的Egde,并没有其他类出现在我的目录树中。
tarjan解决stronglink,堆优化djs解决minpath,并查集解决blocksum+iscircle,完美(个鬼
其实三次作业看下来,并没有理解上的难度,更像是前几次作业的最后步骤:实现。课程组已经为我们解决了前两次作业的架构设计问题,把框已经框的差不多了,填就完事了。JML也只是第一步而已。
BUG分析:
-
三次作业对于JML的理解上倒没有出现什么问题,死就死在tle上了。
-
第一次作业中鉴于时间较为宽松,也就并无考虑性能相关事宜,但万万没有想到,随手写的
DFS
摆了我一道。当然这不是说DFS
不适用于本次作业,而是说,我用错DFS了,鉴于上学期数据结构全还给了老师(可能也本身就没有接收到吧)测试数据不够针对性,使得我把生成全排列的DFS
随手套用上了,即递归回来后又把标记位抹去了,于是,我不死谁死。强测20分让我直接自闭,删掉一行全部修复之后更自闭。但反省下还是算法不熟练的问题。
注释掉一行结束 -
第二次在强测中倒是没出什么叉子,只是在对拍的时候发现数据集一大,就会出错。在我看了两遍之后终于发现问题处在不大于1111上,一个
"="
搞死我,另一个就是因为在找这个bug
的时候随手改了点东西....git
版本控制用的不好啊... -
第三次用了
tarjan
、堆优化的djs
、并查集
,自以为万无一失来着(。互测时发现同屋有明显bug就觉得不太对了,果然强测出来tle
了一个,检查后发现还是出在djs
的标志位
上(叹气),加了三行修了之后感叹下,算法用的不熟练果然会死人的。- 第三次互测中发现了一个孩子的tarjan有问题,奈何数据非法呢,互测放弃。
- 在帮别人对拍时发现了其除0错误
添加三行结束
规格撰写和理解上的心得体会 :
- 首先要理解规格(离散数学没学好是种什么体验),这一点在
queryBlockSum
上体现的尤为明显。很多人不理解有一个人的时候为什么返回1,质疑规格的正确性,但回顾离散数学之后就吃鲸了。其次是该规格的描述其实很令人摸不着头脑,按照自然语言说,其实就是返回“块”数。起初我也不理解什么意思,于是自己动手试了试,发现虽然规格说的很玄乎,但实践下来还是挺明确的。当然,也可能是因为离散数学没学好所以理解不了( - 规格不等于实现。规格只是给出了我理解为“要求”的东西,具体实现要根据题目的要求与自己的思维。第三单元刚开始时我一直以为只要按规格写了就可以,事实上,后来慢慢的理解到,规格只是必要条件,而不是实现的充分条件。而如何在规格之上,实现出具有“高性能”、“令人满意”的代码,是该代码撰写者思考的事情。
- 不要把规格理解为限制。对于该规格的表达不意味着就要“照搬照抄”、“不能修改”。譬如在
getconfilctSum
的规格里,为了表达建立了数组,但事实上实现的时候并不需要建立数组再循环计算。我自己第一遍写的时候也是无脑照抄规格,但是写完之后发觉不对(,对规格的实现是要建立在规格的充分理解之上的。 - 最后说说规格的撰写(前面仿佛跑题了),结合老师的讲解,按照我自己的理解,规格起到对模块接口进行规约的作用,但不是对模块内部细节设计进行规约。同时要注意撰写的“全面性”,要对“做成什么”有清楚的理解,关注结果,不管是方法规约还是类的规约,都要注意按照WARRANTY方法,即按照五步走,设计出合理的“问题”。在撰写时不必关心实现,而是按照严谨的语法写出无异议的约束(离散数学万岁。
写在最后
JML显然在团队作业中能够发挥极大的作用。但本单元与其说是JML的学习,不如说是数据结构的复习,其中肯定绝大部分是我自己的原因,但着实本单元下来体验不佳。到了最后甚至不知道是在学算法还是学JML,当然这两者分不开,可能是因为我显然没有一个合格的代码撰写者的能力吧。
仍然感谢群里各位讨论的大佬以及一直跟我讨论的ljh小姐姐和帮助我的其他小朋友。
希望菜鸡继续努力。
以上是关于BUAA_OO_2020_Unit3 Summary的主要内容,如果未能解决你的问题,请参考以下文章