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规格(如OpenJMLJML 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 中常用方法规格:
      • 前置条件 requiresrequires P 表示要求调用者确保 P 为真;
      • 后置条件 ensureensures P 表示方法实现者确保方法执 行返回结果一定满足谓词P的要求,即确保 P 为真;
      • 副作用范围限定:关键词 assignable 表示可赋值,modifiable 表示可修改;
      • pure :表示方法是纯粹的访问方法,不会对对象进行任何修改;
    • 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
  • 技术图片

  • 技术图片

  • 错误分析:

    • 出现错的集中在我自己写的addreladelPerson
    • 其中addrela是按照我自己逻辑写的,并没有jml规约,限制都在MyNetwork里完善了,于是保证输入是合理的。
    • delPerson同理,在官方包中并没有写规约。
    • 但想想所谓的万无一失是架构在自己的逻辑上的,看自己代码的人是否能懂呢,显然jmlng就不懂。一个方法写出来或许就要保证它的完善性吧,如果别人在更改的时候调用了该方法没有做到自己实现的逻辑闭环,还是有很大隐患的,鲁棒性怕是还是要的,对不同输入(非法或不非法)的处理,或许需要进一步完善。

架构设计分析

鉴于三次架构差的不多,仅放上第三次作业图
技术图片
技术图片

第一次作业

基本架构课程组已经给出,总体难度不高,只是摸了dfs写把自己作死了

第二次作业

新增Group接口,基本架构我并没有在课程组的基础上修改。

因为上次作业因为性能被搞了,所以这次根据规格的实现尤其注意性能的把握。首先当然是把dfs扬了,改成路径压缩的并查集。其次是对Group内部方法的实现。缓存的思想对数据进行预处理,要注意处理时对于自身数据的把握。在person中增加自身所在group的存储也是你懂我懂大家都懂的事。

其实本来这次作业还想要设置标志位,以避免每次加人都循环的不必要,而改成响应查询时再从上次循环结束的地方继续进行,但事实证明这种实现过于不现实,遂放弃。

第三次作业

只怕我就是让老师失望的本人(,除了要求的My三件套,为了Djs而构造的Egde,并没有其他类出现在我的目录树中。

tarjan解决stronglink,堆优化djs解决minpath,并查集解决blocksum+iscircle,完美(个鬼

其实三次作业看下来,并没有理解上的难度,更像是前几次作业的最后步骤:实现。课程组已经为我们解决了前两次作业的架构设计问题,把框已经框的差不多了,填就完事了。JML也只是第一步而已。


BUG分析:

  1. 三次作业对于JML的理解上倒没有出现什么问题,死就死在tle上了。

  2. 第一次作业中鉴于时间较为宽松,也就并无考虑性能相关事宜,但万万没有想到,随手写的DFS摆了我一道。当然这不是说DFS不适用于本次作业,而是说,我用错DFS了,鉴于上学期数据结构全还给了老师(可能也本身就没有接收到吧)测试数据不够针对性,使得我把生成全排列的DFS随手套用上了,即递归回来后又把标记位抹去了,于是,我不死谁死。强测20分让我直接自闭,删掉一行全部修复之后更自闭。但反省下还是算法不熟练的问题。
    技术图片
    注释掉一行结束

  3. 第二次在强测中倒是没出什么叉子,只是在对拍的时候发现数据集一大,就会出错。在我看了两遍之后终于发现问题处在不大于1111上,一个"="搞死我,另一个就是因为在找这个bug的时候随手改了点东西....git版本控制用的不好啊...

  4. 第三次用了tarjan、堆优化的djs并查集,自以为万无一失来着(。互测时发现同屋有明显bug就觉得不太对了,果然强测出来tle了一个,检查后发现还是出在djs标志位上(叹气),加了三行修了之后感叹下,算法用的不熟练果然会死人的。

    1. 第三次互测中发现了一个孩子的tarjan有问题,奈何数据非法呢,互测放弃。
    2. 在帮别人对拍时发现了其除0错误
      技术图片
      添加三行结束

规格撰写和理解上的心得体会 :

  1. 首先要理解规格(离散数学没学好是种什么体验),这一点在queryBlockSum上体现的尤为明显。很多人不理解有一个人的时候为什么返回1,质疑规格的正确性,但回顾离散数学之后就吃鲸了。其次是该规格的描述其实很令人摸不着头脑,按照自然语言说,其实就是返回“块”数。起初我也不理解什么意思,于是自己动手试了试,发现虽然规格说的很玄乎,但实践下来还是挺明确的。当然,也可能是因为离散数学没学好所以理解不了(
  2. 规格不等于实现。规格只是给出了我理解为“要求”的东西,具体实现要根据题目的要求与自己的思维。第三单元刚开始时我一直以为只要按规格写了就可以,事实上,后来慢慢的理解到,规格只是必要条件,而不是实现的充分条件。而如何在规格之上,实现出具有“高性能”、“令人满意”的代码,是该代码撰写者思考的事情。
  3. 不要把规格理解为限制。对于该规格的表达不意味着就要“照搬照抄”、“不能修改”。譬如在getconfilctSum的规格里,为了表达建立了数组,但事实上实现的时候并不需要建立数组再循环计算。我自己第一遍写的时候也是无脑照抄规格,但是写完之后发觉不对(,对规格的实现是要建立在规格的充分理解之上的。
  4. 最后说说规格的撰写(前面仿佛跑题了),结合老师的讲解,按照我自己的理解,规格起到对模块接口进行规约的作用,但不是对模块内部细节设计进行规约。同时要注意撰写的“全面性”,要对“做成什么”有清楚的理解,关注结果,不管是方法规约还是类的规约,都要注意按照WARRANTY方法,即按照五步走,设计出合理的“问题”。在撰写时不必关心实现,而是按照严谨的语法写出无异议的约束(离散数学万岁。

写在最后

JML显然在团队作业中能够发挥极大的作用。但本单元与其说是JML的学习,不如说是数据结构的复习,其中肯定绝大部分是我自己的原因,但着实本单元下来体验不佳。到了最后甚至不知道是在学算法还是学JML,当然这两者分不开,可能是因为我显然没有一个合格的代码撰写者的能力吧。

仍然感谢群里各位讨论的大佬以及一直跟我讨论的ljh小姐姐和帮助我的其他小朋友。

希望菜鸡继续努力。

以上是关于BUAA_OO_2020_Unit3 Summary的主要内容,如果未能解决你的问题,请参考以下文章

BUAA_OO_2020_Unit3_Summary

BUAA_OO_2020_Unit3_Overview

BUAA_OO_2021_Unit3_Summary

BUAA_OO_2020_Unit2_Summary

OO_2020_Unit3总结

BUAA_OO_第三单元作业总结