标签：OO 代码 作业 规格 单元 JML JMLUnitNG 小结 表达式
一、 梳理JML语言的理论基础、应用工具链情况
JML是一种行为接口规格语言（Behavior Interface Specification Language，BISL），基于Larch方法构建。
一般而言，JML有两种主要的用法：
（1）开展规格化设计。这样交给代码实现人员的将不是可能带有内在模糊性的自然语言描述，而是逻辑严格的规格。
（2）针对已有的代码实现，书写其对应的规格，从而提高代码的可维护性。这在遗留代码的维护方面具有特别重要的意义。
JML以javadoc注释的方式来表示规格，每行都以@起头。有两种注释方式，行注释和块注释。其中行注释的表示方式为//@annotation ，块注释的方式为/* @ annotation @*/ 。
JML的表达式是对Java表达式的扩展，新增了一些操作符和原子表达式。
原子表达式：
\result表达式、\old(expr)表达式、\not_assigned(x,y,...)表达式、\not_modified(x,y,...)表达式、\nonnullelements( container )表达式。
量化表达式：
\forall表达式、\exists表达式、\sum表达式、\product表达式、\max表达式、\min表达式、\num_of表达式
集合表达式以及操作符等等。
方法规格
前置条件通过requires子句来表示： requires P; 。
后置条件通过ensures子句来表示： ensures P; 。
副作用指方法在执行过程中会修改对象的属性数据或者类的静态成员数据，从而给后续方法的执行带来影响。从方法规格的角度，必须要明确给出副作用范围。JML提供了副作用约束子句，使用关键词assignable 或者modifiable 。
类型规格
指针对Java程序中定义的数据类型所设计的限制规则，一般而言，就是指针对类或接口所设计的约束规则。
不变式（invariant）是要求在所有可见状态下都必须满足的特性。
状态变化约束constraint 用来对前序可见状态和当前可见状态的关系进行约束。
JML的应用工具链
使用JML编译器编译含有JML标记的代码，若程序未实现规格中的要求，JML运行期断言检查编译器会抛出一个uncheckedException来说明程序违背了哪一条规格。JMLdoc工具与Javadoc工具类似，可在生成的HTML格式文档中包含JML规范。还有工具JMLUnitNG可以根据规格的实现自动生成TestNG测试样例。JMLUnit工具生成Java类文件测试的框架。SMT Solver工具以静态方式检查代码实现对规格的满足程度。
二、 部署JMLUnitNG / JMLUnit，针对Graph接口的实现自动生成测试用例，并结合规格对生成的测试用例和数据进行简要分析
首先是jmlUnitNG的经典用法(摘自博客)：
通过java -jar jmlunitng.jar使用适当的命令行选项运行JMLUnitNG()来生成测试类。
（可选）修改测试数据生成策略以添加自定义测试数据（有关生成的文件本身的信息，请参阅下文）。如果不更改测试数据生成策略，它们将使用默认数据。基本类型数据默认值与JMLUnit相同（例如，-1 / 0/1 int）;
使用常规Java编译器编译生成的类，使用适当的JML运行时Jar和JMLUnitNG Jar CLASSPATH。如果使用的是OpenJML RAC，则只需要JMLUnitNG Jar CLASSPATH，因为JMLUnitNG Jar包含OpenJML。
运行测试。这可以通过编写一个 testng.xml文件来运行所有测试，通过从命令行单独运行测试类（每个测试类都有一个main方法），或者从命令行运行TestNG并将其指向测试类来完成。
针对Openjml写了一个测试程序Test.java，其内容是两个整型相乘，得到一个整型。代码及Openjml运行结果如下：
出现了整型溢出的问题，需要对传入参数进行范围限制。JMLUnitNG在Openjml的基础之上进行了自动化样例测试。由于本人电脑不知道什么地方抽风了，JMLUnitNG无法正常运行，只得以其他同学的运行结果代替。
[TestNG] Running:
Command line suite
Failed: racEnabled()
Passed: constructor Test()
Passed: static main(null)
Passed: static main({})
Passed: static mult(-2147483648, -2147483648)
Passed: static mult(2147483648, -2147483648)
Passed: static mult(0, -2147483648)
……
===============================================
Command line suite
Total tests run: 13, Failures: 1, Skips: 0
根据测试结果可见，JMLUnitNG主要针对临界值进行测试。
三、按照作业梳理自己的架构设计，并特别分析迭代中对架构的重构
第九次作业
第九次作业要求实现一个PathContainer类，该类可以对Path类对象进行存储和处理。我创建了一个Arraylist存储Path对象的ID，而存储Path对象自身时，我一开始用的也是Arraylist，但是在获取不重复的节点个数时，使用Arraylist的时间复杂度是o(n^2)，这导致我的强测部分惨不忍睹，于是我改成了Hashmap容器存储节点，格式为 节点 : 出现次数
第十次作业
这次作业在第九次作业的基础之上进一步实现一个Graph类的图，通过该图可以找到最短路径以及两个节点之间的连通性。我依旧使用了Hashmap实现了图，在Hashmap中每个节点存储着其相邻节点，在查找最短路径的方法中我使用的是dijkstra算法，时间复杂度是o(n^2)，这次并没有爆时间复杂度，强测非常顺利地通过了。
第十一次作业
这次作业要在第十次作业的基础之上实现一个RailwaySystem类的图，在方法方面有三个：其一是查找最短路径，其二是不满意度最低，其三是花费最少。由于我未能够很好地理解规格，导致忘记了代码复用的思想、代码量过于庞大臃肿，几乎无法复现bug所在。中测倒数第二个点一直没能够过去，最后也导致强测一塌糊涂。由于地铁的线路图随时会增减，所以我的思路是建立一个存储边的Hashmap，同时还有一个存储节点所在地铁线路的Hashmap，在使用dijkstra算法时访问这两个Hashmap寻找符合条件的最短路径。我没能够使用其他人主流的拆点方法，导致这次作业的复杂度剧增，简直是一塌糊涂，我需要反省一下是什么原因造成了这次作业的失手。
四、按照作业分析代码实现的bug和修复情况
第九次作业
问题出在两点，其一是上文提到的时间复杂度为o(n^2)的问题，换了一种容器使时间复杂度变成o(n)后解决了该问题；第二点是对字典序的理解有误。
第十次作业
没找到bug，顺利通过。
第十一次作业
代码过于混乱，需要重构，bug出现在CPU超时上面，需警戒。
五、阐述对规格撰写和理解上的心得体会
我觉得根据我们指导书发布、大家撰写的课程形式来看，直接给规格让我们去写有些舍本逐末。很多时候（尤其是第十一次作业）的规格看得让人头大，甚至不如指导书上直接的阐述让人更清楚明白。我觉得为了理解规格，还是我们自己写来得更加透彻一些。jml虽然是一种非常规范化的语言，但是私以为不如自然语言。毕竟在今后的程序设计中大家是一个团队，相比于枯燥的jml语言，自然语言的交流会更加的快捷高效。当然了，jml的功能还是聊胜于无的，对jml的学习也让我明白了在面向对象编程的时候一个好的架构设计有多么的重要。
标签：OO,代码,作业,规格,单元,JML,JMLUnitNG,小结,表达式 来源： https://www.cnblogs.com/17231073oo/p/10901273.html
本站声明： 1. iCode9 技术分享网（下文简称本站）提供的所有内容，仅供技术学习、探讨和分享； 2. 关于本站的所有留言、评论、转载及引用，纯属内容发起人的个人观点，与本站观点和立场无关； 3. 关于本站的所有言论和文字，纯属内容发起人的个人观点，与本站观点和立场无关； 4. 本站文章均是网友提供，不完全保证技术分享内容的完整性、准确性、时效性、风险性和版权归属；如您发现该文章侵犯了您的权益，可联系我们第一时间进行删除； 5. 本站为非盈利性的个人网站，所有内容不会用来进行牟利，也不会利用任何形式的广告来间接获益，纯粹是为了广大技术爱好者提供技术内容和技术思想的分享性交流网站。