标签：OO 总结 java jar 规格 表达式 JML Group 单元
OO第三单元总结
一、 梳理JML语言的理论基础、应用工具链情况
1、JML语言的理论基础
JML语言确实是个好东西，JML是一种规格化的语言，JML采用了一种信任机制，通过JML语言，实现者信赖使用者一定是按照规格规定的条件来使用的，而使用者则确信方法实现了自己想要的功能而不会出现其它改变。无论是对使用者还是实现者来说，JML都简化了自己的职责，让自己的任务变得更明确也更简单。
一般而言，JML有两种主要的用法：
（1）开展规格化设计。这样交给代码实现人员的将不是可能带有内在模糊性的自然语言描述，而是逻辑严格的规格。
（2）针对已有的代码实现，书写其对应的规格，从而提高代码的可维护性。这在遗留代码的维护方面具有特别重要的意义。
JML语言的基础知识，通过资料的学习大家都很熟悉，就不再赘述，此处主要写写自己对JML语法的一些认识和看法。
首先是结构，JML语法中主要包括三个部分：前置条件，副作用和后置条件。requires是前置条件的关键字，assignable是副作用的关键字，ensure定义后置条件。我们阅读JML的顺序也是这三个部分依次阅读，首先阅读前置条件确定输入范围，然后看assignable了解需要改变的有哪些，最后看需要满足的后置条件。
JML的核心内容则是表达式，表达式主要出现在前置条件和后置条件中，构成约束。表达式又可以分为原子表达式、量化表达式和集合表达式。值得注意的是JML在描述复杂行为的时候往往会采取复合的表达式，在阅读这种表达式的时候我们要分层次阅读，同时也要尽可能读懂每一个小表达式的意思，再融入到整个表达式的理解中去。
2、应用工具链
JML的应用工具链还挺多，如OpenJML，SMT Solver，JMLUnitNG，Junit4等。
OpenJML与SMT Solver：
SMT Solver就是可满足性理论求解器【不是很理解，大致上就是判断公式是否可满足之类的，同时还可以进行等价验证】，这里我们对SMT Solver的使用主要就是使用OpenJML对规格进行检查，从github上下载的OpenJML包附带了三个求解器【OpenJML官网上的直接下载链接无法打开，但是官网上附了一个github链接，可以从github上下载OpenJML包】，使用java -jar openjml.jar -exec Solvers-windows\z3-4.7.1.exe -esc test\Group.java这样的指令就可以进行规格检查，我本人尝试对person检查不会出现什么错误，但对group检查会提示找不到person类的反馈，可能是无法找到关联类的原因。
JMLUnitNG
JMLUnitNG可以自动生成测试用例进行测试，听起来是个不错的东西，但实际操作起来确实不太友好。首先下载了JMLUnitNG，然后相要完成验证，主要有4条指令：
java -jar jmlunitng.jar test/Group.java
javac -cp jmlunitng.jar test/*.java
java -jar openjml.jar -rac test/Group.java test/Person.java
java -cp jmlunitng.jar test.Group_JML_Tes
第一条指令主要是生成测试用例，第二条则是对生成的java文件进行编译。在处理第一条指令的时候，我就遇到了很多问题，主要的问题就是在Group种无法找到Person类，然后报出看不懂的异常：
本人是用Person类执行成功第一条指令才发现这个问题，想通过那个异常找出问题很难。解决办法就是把Person和Group放在同一个package下，另外就是在使用容器初始化的时候，如ArrayList<Person> people = new Arraylist<>()会报错，需要在<>内加入Person才能通过。
在执行第三条指令的时候我又遇到了错误，错误如下：
分析可知大概是Collections出了问题，但我并不知道问题出在哪里，我猜测可能是OpenJML不支持Collections导致的，所以我删去了Group类中用到的关于collection的地方，果然没有再报错。
在第四步的时候我遇到了这样的错误：
按图中的说法应该是版本的问题，我去查了一下，jdk1.8（即jdk8）的class version应该是52来着，但我不知道为啥我的就成了56，无奈我再次安装了一遍jdk1.8，成功将版本该会52，终于黄天不负有心人，最终结果如下：
总的来说，能得到结果已经很不错，据众多同学反应，该方法无法获得边界值，而且应该不止Collection这一种问题，其它同学都遇到了其它很多问题，这是由于Jmlunitng和openjml实在是很古老了，缺乏更新，新版java的很多内容无法支持和检验，体验效果不好。
本人上诉总结了一些jmlunitng错误，如果后续的学弟学妹们还需要做这部分的内容，有机会看到我的博客，希望能有所帮助。
Junit4：
最后一种就是Junit4了，相对前几种方式，我个人还是比较推崇Junit4来验证代码，Junit4是根据规格来构造样例对实现进行验证，同时还可以查看覆盖率，是比较完善的验证方法，在工程中也有很大的应用。对于Junit4来说，最主要的就是好的测试用例，一个工程项目的完成会产生大量的测试用例，这就对后续的再验证有了很好支持。
二、 架构设计和模型构建策略
JML规格对于实现来说确实有很大的便利，可能是由于前两个单元需要自己设计复杂的架构，初拿到代码，发现这单元好像并不需要自己设计架构，只要按照规格进行实现就好了，于是一股脑的根据规格来实现代码，并没有太多关于架构的设计，但第三单元做完，经过老师提点才发现其实可以设计很好的架构来提高代码的效率，比如加入并查集，把money交给person管理等都是很好的架构。
由于三次作业架构相似，下面仅给出第三次作业的UML图和分析：
可以看出，整个架构其实很简单。
由于结构设计的原因，MyNetwork的方法过多，复杂度高。
三、 代码实现的bug和修复情况
本次代码的实现的bug主要是方法中存在的一些bug，其实社交网络的本质是一张图，然后各种操作就是对图的运算。本人在第一次作业中没有出现bug，第二次实验出现了两个bug，一个是规格读得不仔细，没有排除异常情况，另一个是group内方法查询的复杂度的问题导致的超时，通过二叉查找，我降低了查找的效率，成功修复。第三次作业的bug主要出现在图的双连通运算上，我采用的两次dfs的算法，显然这种方法是有缺陷的，另一个则是没有使用并查集来实现qbs，这也降低了效率。
四、 心得体会
JML规格确实是一种难得的模式，给设计者、实现者、使用者三方都带来了不同的便利，同时通过JML规格可以很好的对代码进行验证，这在工程中也有广泛的应用，这让我们可以提前了解到工程中的情况，对未来有很大的帮助。·
标签：OO,总结,java,jar,规格,表达式,JML,Group,单元 来源： https://www.cnblogs.com/RiverTan/p/12944359.html
本站声明： 1. iCode9 技术分享网（下文简称本站）提供的所有内容，仅供技术学习、探讨和分享； 2. 关于本站的所有留言、评论、转载及引用，纯属内容发起人的个人观点，与本站观点和立场无关； 3. 关于本站的所有言论和文字，纯属内容发起人的个人观点，与本站观点和立场无关； 4. 本站文章均是网友提供，不完全保证技术分享内容的完整性、准确性、时效性、风险性和版权归属；如您发现该文章侵犯了您的权益，可联系我们第一时间进行删除； 5. 本站为非盈利性的个人网站，所有内容不会用来进行牟利，也不会利用任何形式的广告来间接获益，纯粹是为了广大技术爱好者提供技术内容和技术思想的分享性交流网站。