标签：OO LIFE NO 复杂度 作业 规格 JML 第二次 方法
目录
JML初步
JML引导
JML是一种形式化的、面向JAVA的行为接口规格语言。简而言之，即是一份老板给下属员工的任务表，告诉你什么情况应该得到什么的结果，你能使用什么工具，不能使用什么工具。而显然的是，我们就是这样的员工，读懂了老板分配的任务，就开始干活。至于怎么干，老板并不关心，关心的只是能否在固定时间内得到符合预期的结果。
由此可见，JML在应对工程任务时，有着极大的遍历。一是便于规格的统一；二是便于测试的展开，根据JML对得到程序进行格式化验证，甚至能够达到100%的准确率。
JML使用
-
JML使用的是Javadoc的注释方式。形式常为：//@ …… 或*/* …… / 。
-
方法规格：
- \requires P：前置条件。要求调用者保证P为真，方法规格中可以含有多个require语句。
- \ensures P：后置条件。要求方法执行完成之后，P为真。
- \assignable ：副作用。方法执行时，会改变某些对象的属性，这些对象需在副作用中明确。
- \signals：异常。当满足条件时，方法抛出异常。
-
类型规格：
- invariant：不变式。要求在所有可见状态下都必须满足的表达式。
- constraint：状态变化约束。对于变量改变做出的限制。
-
常见表达式：
- \result：对于方法执行所得到的返回值做出一定限制。
- \old(expr)：表示expr在该方法执行前所指向的对象。
- \forall：表示全称量词。
- \exists：表示存在量词。
- \sum：表示求和。
（
想起被离散支配的日子
JML工具链
* Openjml：通过与SMT Solver等共同使用，实现对JML规格的检测。
* JML UnitNG：自动生成测试检测代码正确性。
Openjml与Solver
写博客的这几天，基本上都在捣鼓这玩意，报的错也是各种都有，乱七八糟，心态爆炸。其中最容易碰到的就是找不到Person类。
经过多天尝试，还是没有进展的情况下，我打算采取了暴力方法。直接将Person类塞进Group文件里（拒绝checkstyle），结果真成了。
经过信息验证，我们会发现是不支持三目运算符的。经过修改之后，即可成功跑通（采用normal_behavior）。
JMLUnitNg
由于对Group的测试出现了一些状况之外的报错，例如编译器版本不对，环境异常等等，实在找不到解决办法，遂放弃。
作业架构分析
第一次作业
第一次的架构比较简单，一步步按着JML写即可。容器采用的均为ArrayList。
其中，isCircle是较为困难的地方。本次作业笔者采用的是BFS做法，通过标记点和队列实现方法。
由图可见，第一次作业的复杂度并不高。
第二次作业
第二次作业在第一次作业的基础上引入了新类Group。
考虑到第二次作业的数据量级是以万为单位，我更改了第一次作业中的数据存储结构，对于所有存储数据替换为ArrayList和HashMap的双存储结构；前者用来遍历，后者用来查找。典型的空间换时间做法。
其中，复杂度较高的是针对Group的几个函数：relationSum、valueSum、ageVar……显然，在这么高的数据强度下，双循环的复杂度会爆炸，所以采取了缓存的方式进行优化：即将复杂度转移到了addRelation和addToGroup方法之上，有效地减少了运行时间。
MyGroup类的复杂度。
MyNetwork类的复杂度
由复杂度可见，方法的复杂度主要堆积在了上述所提及的方法之上。
第三次作业
第三次作业在第二次作业的基础上并未引入新的类，而是增加了group以及network中的方法。
笔者继续延用了第二次作业的双存储结构。以及改变了isCircle的判别方法，引入了并查集的属性进行连通性的判断。新引入方法的处理也有着不小的难度。
queryMinPath，即求两点的最短路径，不话没说，直接上迪杰斯特拉（结果可想而知）。
queryStrongLinked，采取的是判断两点之间是否存在两条完全不重复的路径方法（结果可想而知）。
queryBlockSum，即判断连通块的数量，并打算用并查集辅助完全，但是考虑到时间性能，引入缓存机制。即每当调用addPerson方法时，使得数量加一；当调用addRelation方法时，根据情况减去一。
MyGroup类的复杂度
MyNetwork类的复杂度
由上图可知，qsl以及qmp的复杂度太恐怖了，并且由于过度使用缓存机制，导致addRelation方法的复杂度也是极高的。
作业BUG分析
第一次作业
第一次作业的情况极其惨烈。当时刚看到作业的时候兴奋不已，单纯地以为照着JML写写就没什么大事，却在细节的处理上被搞得心态爆炸。isCircle方法中，id1与id2相等的情况并未处理完全，导致强测爆炸。
修复：直接采取特判返回。
第二次作业
第二次作业由于课下进行了大量的对拍，Junit验证，并未发现bug。
第三次作业
第三次作业由于queryMinPath方法采用了最朴素的迪杰斯特拉算法，导致ctle。
修复：采用了堆优化的迪杰斯特拉算法。
心得体会
由于本单元的作业大部分都是根据JML写代码，只有在实验课上按葫芦画瓢地写了一点点JML，对JML撰写的理解并不是很深入。
对于JML的练习，我觉得是一个很不错的选择，或者说更像是一种职场化的提前预习？给我的感觉就是更加工程化，每个人各司其职，写规格的就写规格，写代码的就写代码，不仅使得项目管理更加方便，也避免了不少各自的冲突。但是，通过对JML工具链的使用，感觉JML的”生态环境“确实一言难尽。。。
标签：OO,LIFE,NO,复杂度,作业,规格,JML,第二次,方法 来源： https://www.cnblogs.com/Sakoo794/p/12942274.html
本站声明： 1. iCode9 技术分享网（下文简称本站）提供的所有内容，仅供技术学习、探讨和分享； 2. 关于本站的所有留言、评论、转载及引用，纯属内容发起人的个人观点，与本站观点和立场无关； 3. 关于本站的所有言论和文字，纯属内容发起人的个人观点，与本站观点和立场无关； 4. 本站文章均是网友提供，不完全保证技术分享内容的完整性、准确性、时效性、风险性和版权归属；如您发现该文章侵犯了您的权益，可联系我们第一时间进行删除； 5. 本站为非盈利性的个人网站，所有内容不会用来进行牟利，也不会利用任何形式的广告来间接获益，纯粹是为了广大技术爱好者提供技术内容和技术思想的分享性交流网站。