码迷,mamicode.com
首页 > 其他好文 > 详细

JML规格 -- OO Unit 3

时间:2020-05-23 13:28:33      阅读:54      评论:0      收藏:0      [点我收藏+]

标签:rac   esc   sig   完成   person   http   pre   exp   补充   

JML 规格设计


JML语法


  1. 一些语法的细节:
  • jml断言中,不能使用++,--,+=等操作符
  • \old(expr) 仅表示一个java对象expr的引用是否在操作前后变化,而不能查看成员变量是否改变
  • \not_assigned(x, y) 表达式,用来表示变量是否被赋值,而\not_modified(x, y) 表示变量取值是否变化。
  • \nonnullelenment(cont) 表示容器内不会有null
  • \type(cls) 返回cls的类型
  • \typeod(expr) 返回expr的准确类型
  • \sum (expr) 求和;\product(expr) 连乘;\num_of 求个数
  1. 方法规格:
    方法规格的核心包括三个方面:前置条件,后之条件和副作用条件。
    如果不满足前置条件,方法执行结果不可预测;如果满足后之条件, 则表示方法执行正确.
    前置条件用requires修饰, 可以有多个;后之条件用ensure修饰;副作用常常用assignable和modified。
    纯粹访问性的方法用/@pure@/修饰。
    正常行为用public normal_behavior; 异常用public excptional_behavior, 二者之间用also链接,并且二者的前置条件交集为空。
    此外,当父类定义了规格,子类重现方法后,需要补充规格也可以用also。
    当发出一个异常后,用signals语句强调异常类型,signals_only仅抛出相应异常。
    此外异常中也可以使用ensures

  2. 类型规格:

  • 不变式 要求在所有可见状态下都必须满足。但,凡是会修改成员变量的方法执行期间,对象的状态都是不可见的。
    不变式可以直接应用pure修饰的方法。
    constraint对前序可见状态和当前可见状态的关系进行约束。

Openjml使用

在此目录树下:
技术图片

通过输入命令

java -jar ./openjml.jar -exec /home/brandonmoo/OORepo/home12/Solvers/z3-4.7.1 -esc /home/brandonmoo/OORepo/home12/src/*.java

在目录下测试时,会出现类似于很多错误,比如不可比较的类型,未找到符号,不兼容的类型。其原因是jml的规格语法不符合openjml。此外,openjml
不允许变量名的重复使用。
技术图片
于是只好放弃通过openjml测试规格,还是通过手动构造样例进行JUnit单元测试。

部署JMLUnitNG

运行以下命令:

                 java -jar jmlunitng.jar src/Person.java

                 javac -cp jmlunitng.jar src/*.java

                 java -jar openjml.jar -rac src/Person.java

                 java -cp jmlunitng.jar src.Person_JML_Test

果不其然还是出现了一堆报错

技术图片

由于参考了jyc同学的博客,发现其实jmlunitng存在局限性,其数据并非随机,测试范围覆盖不够。于是,最终还是使用JUnit来手动构造测试集。

第一次作业UML&复杂度分析

技术图片

技术图片

这里主要的复杂度在于addrelation和dfs,由于add要更新并查集,压缩路径,导致复杂度变高

第二次作业UML&复杂度分析

技术图片

技术图片

第三次作业UML&复杂度分析

技术图片

技术图片

技术图片

由于使用了n^2的算法,导致qmp方法复杂度飙升,也使得强测tle,这是我在代码bug修复中最痛苦的一部分。

Bug修复

  1. 第一次作业,由于课下测试不充分,我没有进入强测。
    关键问题是dfs设计的问题导致爆栈。

  2. 第二次作业, 由于采用了并查集,更改了很多方法,导致隐藏bug未能发现,尽管使用了Junit仍然不能发现一些随机性强的bug,果断又没有进强测,之后改bug时发现,仅仅将并查集换乘dfs就能修复大多数bug。。。这个故事告诉我们新方法更要多加测试。

  3. 第三次作业,终于能进强测,结果却大量TLE,问题是没有优化设计,提升算法。

心得体会

在基于规格设计代码时,首先要灵活,不一定非要用规格定义的模式去完成代码,可以采用多种容器,多种方法,多种数据结构。只要能保证规格的要求,在实现上一各个方法中性能好,实现难度低,数据管理清晰的优先。

JML规格 -- OO Unit 3

标签:rac   esc   sig   完成   person   http   pre   exp   补充   

原文地址:https://www.cnblogs.com/brandonmoo/p/12941985.html

(0)
(0)
   
举报
评论 一句话评论(0
登录后才能评论!
© 2014 mamicode.com 版权所有  联系我们:gaon5@hotmail.com
迷上了代码!