标签：部分 规格 实现 推理 思想 Requires 目的 细节 launch
JML是一种形式化的、面向JAVA的行为接口规格语言（behavioral interface specification language）
JML允许在规格中混合使用Java语法成分和JML引入的语法成分
JML使用Javadoc的注释方式
JML已经拥有了相应的工具链，可以自动识别和分析处理JML规格（如OpenJML，JML UnitNG等）
JML基本组成：前置条件、后置条件、会改变的元素和属性、不会改变的元素和属性、不正常的行为发生时抛出异常
\old(expr) 表达式用来表示一个表达式 expr 在相应方法执行前的取值；\result 表达式表示方法的执行返回结果；\forall 表达式是全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束；\exists 表达式是存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束；\sum 表达式表示返回给定范围内的表达式的和；\product 表达式表示返回给定范围内的表达式的连乘结果；\max \min 表达式分别表示返回给定范围内的表达式的最大值和最小值；<==> <=!=> 等价关系操作符： b_expr1<==>b_expr2 或者b_expr1<=!=>b_expr2 分别表示表达式相等或不等；==> <== 推理操作符： b_expr1 ==> b_expr2 或者 b_expr2 <== b_expr1 。requires ：requires P 表示要求调用者确保 P 为真；ensure ：ensures P 表示方法实现者确保方法执 行返回结果一定满足谓词P的要求，即确保 P 为真；assignable 表示可赋值，modifiable 表示可修改；pure ：表示方法是纯粹的访问方法，不会对对象进行任何修改；缺省参数检查：
静态检查：
动态检查：
呵
下载包
运行
错误分析：
addrela与delPerson上addrela是按照我自己逻辑写的，并没有jml规约，限制都在MyNetwork里完善了，于是保证输入是合理的。delPerson同理，在官方包中并没有写规约。jmlng就不懂。一个方法写出来或许就要保证它的完善性吧，如果别人在更改的时候调用了该方法没有做到自己实现的逻辑闭环，还是有很大隐患的，鲁棒性怕是还是要的，对不同输入（非法或不非法）的处理，或许需要进一步完善。鉴于三次架构差的不多，仅放上第三次作业图
第一次作业
基本架构课程组已经给出，总体难度不高，只是摸了dfs写把自己作死了
第二次作业
新增Group接口，基本架构我并没有在课程组的基础上修改。
因为上次作业因为性能被搞了，所以这次根据规格的实现尤其注意性能的把握。首先当然是把dfs扬了，改成路径压缩的并查集。其次是对Group内部方法的实现。缓存的思想对数据进行预处理，要注意处理时对于自身数据的把握。在person中增加自身所在group的存储也是你懂我懂大家都懂的事。
其实本来这次作业还想要设置标志位，以避免每次加人都循环的不必要，而改成响应查询时再从上次循环结束的地方继续进行，但事实证明这种实现过于不现实，遂放弃。
第三次作业
只怕我就是让老师失望的本人（，除了要求的My三件套，为了Djs而构造的Egde，并没有其他类出现在我的目录树中。
tarjan解决stronglink，堆优化djs解决minpath，并查集解决blocksum+iscircle，完美（个鬼
其实三次作业看下来，并没有理解上的难度，更像是前几次作业的最后步骤：实现。课程组已经为我们解决了前两次作业的架构设计问题，把框已经框的差不多了，填就完事了。JML也只是第一步而已。
三次作业对于JML的理解上倒没有出现什么问题，死就死在tle上了。
第一次作业中鉴于时间较为宽松，也就并无考虑性能相关事宜，但万万没有想到，随手写的DFS摆了我一道。当然这不是说DFS不适用于本次作业，而是说，我用错DFS了，鉴于上学期数据结构全还给了老师（可能也本身就没有接收到吧）测试数据不够针对性，使得我把生成全排列的DFS随手套用上了，即递归回来后又把标记位抹去了，于是，我不死谁死。强测20分让我直接自闭，删掉一行全部修复之后更自闭。但反省下还是算法不熟练的问题。
注释掉一行结束
第二次在强测中倒是没出什么叉子，只是在对拍的时候发现数据集一大，就会出错。在我看了两遍之后终于发现问题处在不大于1111上，一个"="搞死我，另一个就是因为在找这个bug的时候随手改了点东西....git版本控制用的不好啊...
第三次用了tarjan、堆优化的djs、并查集，自以为万无一失来着（。互测时发现同屋有明显bug就觉得不太对了，果然强测出来tle了一个，检查后发现还是出在djs的标志位上（叹气），加了三行修了之后感叹下，算法用的不熟练果然会死人的。
queryBlockSum上体现的尤为明显。很多人不理解有一个人的时候为什么返回1，质疑规格的正确性，但回顾离散数学之后就吃鲸了。其次是该规格的描述其实很令人摸不着头脑，按照自然语言说，其实就是返回“块”数。起初我也不理解什么意思，于是自己动手试了试，发现虽然规格说的很玄乎，但实践下来还是挺明确的。当然，也可能是因为离散数学没学好所以理解不了（getconfilctSum的规格里，为了表达建立了数组，但事实上实现的时候并不需要建立数组再循环计算。我自己第一遍写的时候也是无脑照抄规格，但是写完之后发觉不对（，对规格的实现是要建立在规格的充分理解之上的。JML显然在团队作业中能够发挥极大的作用。但本单元与其说是JML的学习，不如说是数据结构的复习，其中肯定绝大部分是我自己的原因，但着实本单元下来体验不佳。到了最后甚至不知道是在学算法还是学JML，当然这两者分不开，可能是因为我显然没有一个合格的代码撰写者的能力吧。
仍然感谢群里各位讨论的大佬以及一直跟我讨论的ljh小姐姐和帮助我的其他小朋友。
希望菜鸡继续努力。
标签：部分 规格 实现 推理 思想 Requires 目的 细节 launch
原文地址：https://www.cnblogs.com/weilan1201/p/12922681.html
